A Property Kind Calculus for Measurement Metrology

20.1. The references layer (citation metadata only)🔗

Definition20.1.1
groupuses 0used by 1✓L∃∀N

A standard reference StandardRef is the bibliographic identity of one part: its publishing body (ISO or IEC), the series number (80000), the part number, the edition designation as printed, the publication date, and the part's English title. It carries no normative content — only what is needed to cite the source. Its cite renders the conventional form, e.g. IEC 80000-6, Edition 2.0, 2022-11.

Lean code for Definition20.1.1●1 definition
  • structure(6 fields)defined in PropertyKindCalculus/Iso80000/References.lean
    complete
    structure PropertyKindCalculus.Iso80000.StandardRef : Type
    structure PropertyKindCalculus.Iso80000.StandardRef :
  Type
    A **bibliographic reference** to a published standard — body, number, part,
edition, and date only. No normative content is carried; this records the citable
identity so a {quantity-kind} or {unit} can name its exact source.

    Fields

    body : PropertyKindCalculus.Iso80000.StandardBody
    The publishing body (ISO or IEC). 
    number : Nat
    The series number — `80000`. 
    part : Nat
    The part number (e.g. `3` for *Space and time*). 
    edition : String
    The edition designation as printed on the cover (e.g. "Second edition",
"Edition 2.0"). 
    date : String
    Publication date, year-month (e.g. "2019-10"). 
    title : String
    The part's official English title (the subtitle after "Quantities and units —").
Proof for Definition 20.1.1
uses 0

Realized as structure StandardRef (Mathlib-free) with a StandardBody (ISO/IEC) field and the printed edition, date, and title as strings, plus designation (ISO 80000-3) and cite (the full reference). The values are read off each licensed part's cover page; nothing normative is transcribed.

Definition20.1.2
groupuses 1used by 0✓L∃∀N

The catalogue is the list of the thirteen catalogued parts in part order, each a standard reference. It is the single place this work names which editions of ISO/IEC 80000 the catalogued quantity-kinds and units are grounded against, so the grounding is auditable rather than implicit.

Lean code for Definition20.1.2●1 definition
  • defdefined in PropertyKindCalculus/Iso80000/References.lean
    complete
    def PropertyKindCalculus.Iso80000.catalogue :
  List PropertyKindCalculus.Iso80000.StandardRef
    def PropertyKindCalculus.Iso80000.catalogue :
  List
    PropertyKindCalculus.Iso80000.StandardRef
    The full catalogue of licensed parts, in part order.
Proof for Definition 20.1.2
uses 0

Realized as catalogue : List StandardRef, the thirteen definitions iso80000_1 … iec80000_13 (with iec80000_6 and iec80000_13 the IEC-published parts). The edition is "Second edition" for every part except those two, both "Edition 2.0"; the dates are the cover dates of the licensed copies.