A Property Kind Calculus for Measurement Metrology

28.2. The gray/sievert collision — the standard's own J/kg disambiguation🔗

Four quantities of ISO 80000-10 carry the dimension L²·T⁻² (energy per mass): the absorbed dose (10-81.1), the specific energy imparted (10-81.2), the kerma (10-86.1) — all in grays — and the dose equivalent (10-83.1) — in sieverts. The gray and the sievert are the same coherent unit, J/kg; the standard gives them different special names precisely because the kinds differ: the physical energy deposited per mass, versus that energy weighted for biological effect.

This is requirement R1 (the dimension does not classify the kind) confirmed by the standard's own hand. A dimension-only model sees one type, "a real number of joules per kilogram", for absorbed dose and dose equivalent — and would let a gray be silently read as a sievert, the exact error the two unit names exist to prevent. It is the entropy-versus-heat-capacity J/K collision of ISO 80000-5, made sharper: here the collision is between two named units, not two uses of one.

Theorem28.2.1
Group: The dimension-collision capstone, on standard quantities: the dimension map identifies absorbed dose with dose equivalent, while the kind layer keeps them apart, both as kinds and as units (the gray and the sievert). The becquerel collision ( T⁻¹ ) is the companion. (2)
Group member previews
Preview
Theorem 28.2.2
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N
EffortsmallTagscapstoneproved

Absorbed dose is not dose equivalent, though both are J/kg and L²·T⁻² (items 10-81.1, 10-83.1). There exist distinct ISO 80000-10 kinds with the same dimension — absorbed dose and dose equivalent witness it, alongside the specific energy imparted and the kerma. The standard assigns two unit names (gray, sievert) to one dimension; no dimension-only type system can separate them, the kind layer — and the unit — does. Uses the dimension map.

Lean code for Theorem28.2.1●1 theorem
  • theoremdefined in PropertyKindCalculus/Iso80000/Part10.lean
    complete
    theorem PropertyKindCalculus.Iso80000.Part10.iso80000_10_dim_collision :
  ∃ a b,
    a.kind LTMCTDimensionBase ≠ b.kind LTMCTDimensionBase ∧
      a.dim LTMCTDimensionBase = b.dim LTMCTDimensionBase
    theorem PropertyKindCalculus.Iso80000.Part10.iso80000_10_dim_collision :
  ∃ a b,
    a.kind LTMCTDimensionBase ≠
        b.kind LTMCTDimensionBase ∧
      a.dim LTMCTDimensionBase =
        b.dim LTMCTDimensionBase
    **The gray/sievert collision capstone, on the standard.** There exist distinct
ISO 80000-10 kinds with the same dimension `L²·T⁻²` — absorbed dose and dose equivalent
witness it, alongside the specific energy imparted and the kerma. The standard assigns two
unit names (gray, sievert) to one dimension; the {dimension functor} cannot separate them,
the kind layer — and the unit — does.
Proof for Theorem 28.2.1
uses 0

iso80000_10_dim_collision, witnessed by ⟨absorbedDose, doseEquivalent, …⟩. The unit fact gray_sievert_not_commensurable is a decide. Axiom-free.

Theorem28.2.2
Group: The dimension-collision capstone, on standard quantities: the dimension map identifies absorbed dose with dose equivalent, while the kind layer keeps them apart, both as kinds and as units (the gray and the sievert). The becquerel collision ( T⁻¹ ) is the companion. (2)
Group member previews
Preview
Theorem 28.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N
EffortsmallTagsproved

The becquerel of activity and the reciprocal second of the decay constant are not commensurable, though both are T⁻¹ (items 10-27, 10-24). The becquerel is the special name SI reserves for s⁻¹ as the unit of activity — a kind distinction the dimension cannot see, shared also with the particle emission rate and the Larmor and cyclotron frequencies. Uses the metrological unit.

Lean code for Theorem28.2.2●1 theorem
  • theoremdefined in PropertyKindCalculus/Iso80000/Part10.lean
    complete
    theorem PropertyKindCalculus.Iso80000.Part10.becquerel_perSecond_not_commensurable :
  ¬PropertyKindCalculus.Iso80000.Part10.becquerel.Commensurable
      PropertyKindCalculus.Iso80000.Part10.perSecondDecay
    theorem PropertyKindCalculus.Iso80000.Part10.becquerel_perSecond_not_commensurable :
  ¬PropertyKindCalculus.Iso80000.Part10.becquerel.Commensurable
      PropertyKindCalculus.Iso80000.Part10.perSecondDecay
    **The becquerel of activity and the reciprocal second of the decay constant are not
commensurable, though both are `T⁻¹`.** The becquerel is the special name SI reserves for
`s⁻¹` as the unit of activity — a kind distinction the dimension cannot see.
Proof for Theorem 28.2.2
uses 0

becquerel_perSecond_not_commensurable, by decide after unfolding MetrologicalUnit.Commensurable. The underlying kind distinction is activity_ne_decayConstant, and activity_dim_eq_decayConstant_dim records the shared dimension. Axiom-free.