A Property Kind Calculus for Measurement Metrology

24.1. Quantity-kinds and units of IEC 80000-6🔗

Definition24.1.1
Group: Each catalogued kind reuses the dimension functor dim over PhysLib's Dimension , now over the charge generator C (with electric current as C·T⁻¹ ), so the standard's dimensional facts — a capacitance is C²·M⁻¹·L⁻²·T² , a resistance M·L²·T⁻¹·C⁻² , a magnetic flux M·L²·T⁻¹·C⁻¹ — are checked computations rather than annotations. The kinds are dimensioned internally over this charge generator — so the checked facts read in C (a capacitance's charge-exponent is 2 ) — but the item-index tables cite each dimension in the ISQ base quantity current via the change of basis C = I·T , so the printed capacitance is M⁻¹·L⁻²·T⁴·I² exactly as IEC 80000-6 tabulates it. Each unit is a metrological unit of its kind; commensurability is a type-level fact, so an ampere and a volt are not interchangeable. (2)
Group member previews
Preview
Theorem 24.1.2
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N

A catalogued kind pairs a dimensioned quantity-kind with its exact source in the series — the part, the printed item designation (e.g. "6-51.1"), the principal quantity symbol, and the coherent SI unit symbol. The citation travels with the kind as data, so the source of each definition can be rendered or audited downstream rather than kept in a comment.

Lean code for Definition24.1.1●1 definition
  • structure(5 fields)defined in PropertyKindCalculus/Iso80000/Catalogue.lean
    complete
    structure PropertyKindCalculus.Iso80000.CataloguedKind : Type
    structure PropertyKindCalculus.Iso80000.CataloguedKind :
  Type
    A **catalogued quantity-kind**: a {dimensioned kind} together with its exact
source in the 80000 series — the part, the printed item designation, the principal
quantity symbol, and the coherent SI unit symbol. Every field other than `qk` is a
*citation locator*; the citation travels with the kind as data, so a downstream
model can render or audit the source of each definition. Shared by every part
module, so the structure is defined once rather than per part.

    Fields

    ref : PropertyKindCalculus.Iso80000.StandardRef
    The part of the series this kind is defined in. 
    item : String
    The item designation as printed, e.g. "3-3". 
    symbol : String
    The principal quantity symbol, e.g. "A". 
    coherentUnit : String
    The coherent SI unit symbol, e.g. "m²" (a citation locator). 
    qk : PropertyKindCalculus.DimensionedKind LTMCTDimensionBase
    The dimensioned kind itself.
Proof for Definition 24.1.1
uses 0

Realized as structure CataloguedKind over a DimensionedKind, with cite rendering e.g. IEC 80000-6, Edition 2.0, 2022-11 item 6-51.1 (the one IEC-published part of the catalogue). The catalogue lists all 85 items in item order — electric current (6-1), electric charge (6-2.1), magnetic flux (6-22.1), the impedance family (6-51.1 … 6-51.5), the AC power quantities (6-56 … 6-61), active energy (6-62), … — each paired with its coherent SI unit symbol.

Theorem24.1.2
Group: Each catalogued kind reuses the dimension functor dim over PhysLib's Dimension , now over the charge generator C (with electric current as C·T⁻¹ ), so the standard's dimensional facts — a capacitance is C²·M⁻¹·L⁻²·T² , a resistance M·L²·T⁻¹·C⁻² , a magnetic flux M·L²·T⁻¹·C⁻¹ — are checked computations rather than annotations. The kinds are dimensioned internally over this charge generator — so the checked facts read in C (a capacitance's charge-exponent is 2 ) — but the item-index tables cite each dimension in the ISQ base quantity current via the change of basis C = I·T , so the printed capacitance is M⁻¹·L⁻²·T⁴·I² exactly as IEC 80000-6 tabulates it. Each unit is a metrological unit of its kind; commensurability is a type-level fact, so an ampere and a volt are not interchangeable. (2)
Group member previews
Preview
Definition 24.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N
EffortsmallTagsproved

A capacitance carries the charge generator squared (item 6-13). The catalogued capacitance kind has charge-exponent two in PhysLib's dimension group — the farad's C²·M⁻¹·L⁻²·T² reproduced as a checked computation over the new electric-current base axis, not an annotation. Uses the dimension map.

Lean code for Theorem24.1.2●1 theorem
  • theoremdefined in PropertyKindCalculus/Iso80000/Part6.lean
    complete
    theorem PropertyKindCalculus.Iso80000.Part6.capacitance_dim_charge :
  (PropertyKindCalculus.Iso80000.Part6.capacitance.dim
        LTMCTDimensionBase).charge =
    2
    theorem PropertyKindCalculus.Iso80000.Part6.capacitance_dim_charge :
  (PropertyKindCalculus.Iso80000.Part6.capacitance.dim
        LTMCTDimensionBase).charge =
    2
    **Capacitance is `C²·M⁻¹·L⁻²·T²`: its charge-exponent is `2`** — the farad carries
the charge generator squared (item 6-13).
Proof for Theorem 24.1.2
uses 0

Proved as capacitance_dim_charge : capacitance.dim.charge = 2 in the Iso80000 library, discharged by norm_num over the PhysLib dimension lemmas for the charge generator. The companions electricCurrent_dim_charge = 1 and electricCurrent_dim_time = -1 (item 6-1, the ampere as C·T⁻¹), resistance_dim_charge = -2 (item 6-46, the ohm), and magneticFlux_dim_charge = -1 (item 6-22.1, the weber) record the rest of the electromagnetic algebra.

Theorem24.1.3
Group: Each catalogued kind reuses the dimension functor dim over PhysLib's Dimension , now over the charge generator C (with electric current as C·T⁻¹ ), so the standard's dimensional facts — a capacitance is C²·M⁻¹·L⁻²·T² , a resistance M·L²·T⁻¹·C⁻² , a magnetic flux M·L²·T⁻¹·C⁻¹ — are checked computations rather than annotations. The kinds are dimensioned internally over this charge generator — so the checked facts read in C (a capacitance's charge-exponent is 2 ) — but the item-index tables cite each dimension in the ISQ base quantity current via the change of basis C = I·T , so the printed capacitance is M⁻¹·L⁻²·T⁴·I² exactly as IEC 80000-6 tabulates it. Each unit is a metrological unit of its kind; commensurability is a type-level fact, so an ampere and a volt are not interchangeable. (2)
Group member previews
Preview
Definition 24.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N
EffortsmallTagsproved

An ampere and a volt are not commensurable. Electric current and electric potential are distinct kinds, so their units cannot be compared by ratio — a type-level fact, not a runtime check. Uses metrological units.

Lean code for Theorem24.1.3●1 theorem
  • theoremdefined in PropertyKindCalculus/Iso80000/Part6.lean
    complete
    theorem PropertyKindCalculus.Iso80000.Part6.ampere_voltPotential_not_commensurable :
  ¬PropertyKindCalculus.Iso80000.Part6.ampere.Commensurable
      PropertyKindCalculus.Iso80000.Part6.voltPotential
    theorem PropertyKindCalculus.Iso80000.Part6.ampere_voltPotential_not_commensurable :
  ¬PropertyKindCalculus.Iso80000.Part6.ampere.Commensurable
      PropertyKindCalculus.Iso80000.Part6.voltPotential
    The ampere and the volt are **not** commensurable — electric current and electric
potential are distinct kinds (a type-level fact).
Proof for Theorem 24.1.3
uses 0

Proved as ampere_voltPotential_not_commensurable : ¬ ampere.Commensurable voltPotential by unfolding Commensurable to the underlying kinds and decide. The ampere and the ohm are each WellFormed (electric current and resistance are ratio-scale).