A Property Kind Calculus for Measurement Metrology

25.1. Quantity-kinds and units of ISO 80000-7🔗

Definition25.1.1
groupuses 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. "7-6.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.

Lean code for Definition25.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 25.1.1
uses 0

Realized as structure CataloguedKind over a DimensionedKind, with cite rendering e.g. ISO 80000-7, Second edition, 2019-08 item 7-6.1. The catalogue lists all 66 items in item order — the speed of light (7-1.1), radiant flux (7-4.1), luminous intensity (7-14), the photon quantities (7-19.1 … 7-25), the molar absorption coefficient (7-37), … — each paired with its coherent SI unit symbol.

Theorem25.1.2
group
Statement uses 2
Statement dependency previews
Preview
Definition 11.1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
EffortsmallTagsproved

The candela reduces to power (item 7-14). Luminous intensity carries the dimension of power, M·L²·T⁻³ — the scale-spanning reduction (R13) made a checked computation: PhysLib has no luminous-intensity generator, and none is needed, the spectral luminous efficiency V(λ) that relates the candela to the watt being dimensionless. Uses the dimension map and the scale-spanning units.

Lean code for Theorem25.1.2●1 theorem
  • theoremdefined in PropertyKindCalculus/Iso80000/Part7.lean
    complete
    theorem PropertyKindCalculus.Iso80000.Part7.luminousIntensity_dim_eq_power :
  PropertyKindCalculus.Iso80000.Part7.luminousIntensity.dim
      LTMCTDimensionBase =
    PropertyKindCalculus.Dim.power
    theorem PropertyKindCalculus.Iso80000.Part7.luminousIntensity_dim_eq_power :
  PropertyKindCalculus.Iso80000.Part7.luminousIntensity.dim
      LTMCTDimensionBase =
    PropertyKindCalculus.Dim.power
    **Luminous intensity reduces to power.** The candela carries the dimension of
power, `M·L²·T⁻³` — the scale-spanning reduction (R13).
Proof for Theorem 25.1.2
uses 0

luminousIntensity_dim_eq_power : luminousIntensity.dim = Dim.power, by reflexivity over Dim.luminousIntensity := Dim.power. The companions radiantFlux_dim_{mass,length,time} record M·L²·T⁻³ for radiant flux, radiantEnergy_dim_time = -2 the joule, photonFlux_dim_time = -1 the photon count rate, and molarAbsorptionCoefficient_dim_length = 2 the molar coefficient as an area (the mole reduced).