28.4. The algebraic Remarks as kind-laws: dosimetry built by the kind algebra🔗

Several Part-10 definitions state a quantity's defining relation algebraically. Dose equivalent is the product of absorbed dose with the dimensionless quality factor (10-83.1, H = D·Q); mean life is the reciprocal of the decay constant (10-25, τ = 1/λ); specific activity is activity per mass (10-28); the absorbed-dose rate is absorbed dose per time (10-84); the mass attenuation coefficient is linear attenuation per mass density (10-50). Each is specified as an R12 kind-law, several crossing to ISO 80000-3 and -4.

Theorem28.4.1

uses 1used by 0✓L∃∀N

EffortsmallTagsproved

Dose equivalent is absorbed dose × quality factor — a verified construction (item 10-83.1). A dose equivalent built as the product of an absorbed dose and the dimensionless quality factor carries its product certificate by construction, over the ℝ carrier. The companion doseEquivalent_dim_from_dose_quality shows it keeps the dimension of absorbed dose L²·T⁻² because the quality factor is dimension one — the gray/sievert collision as a checked computation. Uses the quotient kind-law.

Lean code for Theorem28.4.1●1 theorem

theoremdefined in PropertyKindCalculus/Iso80000/Part10/DefiningRelations.lean

complete

theorem PropertyKindCalculus.Iso80000.Part10.DefiningRelations.doseEquivalentOf_isProduct
  (d :
    PropertyKindCalculus.Quantity
      (PropertyKindCalculus.Iso80000.Part10.absorbedDose.kind
        LTMCTDimensionBase)
      ℝ)
  (q :
    PropertyKindCalculus.Quantity
      (PropertyKindCalculus.Iso80000.Part10.qualityFactor.kind
        LTMCTDimensionBase)
      ℝ) :
  PropertyKindCalculus.Quantity.IsProduct
    PropertyKindCalculus.Iso80000.Part10.DefiningRelations.doseEquivalent_prod_dose_quality
    (PropertyKindCalculus.Iso80000.Part10.DefiningRelations.doseEquivalentOf
      d q)
    d q

theorem PropertyKindCalculus.Iso80000.Part10.DefiningRelations.doseEquivalentOf_isProduct
  (d :
    PropertyKindCalculus.Quantity
      (PropertyKindCalculus.Iso80000.Part10.absorbedDose.kind
        LTMCTDimensionBase)
      ℝ)
  (q :
    PropertyKindCalculus.Quantity
      (PropertyKindCalculus.Iso80000.Part10.qualityFactor.kind
        LTMCTDimensionBase)
      ℝ) :
  PropertyKindCalculus.Quantity.IsProduct
    PropertyKindCalculus.Iso80000.Part10.DefiningRelations.doseEquivalent_prod_dose_quality
    (PropertyKindCalculus.Iso80000.Part10.DefiningRelations.doseEquivalentOf
      d q)
    d q

The constructed dose equivalent satisfies the product certificate by construction.

Proof for Theorem 28.4.1

uses 0

doseEquivalentOf d q := Quantity.mul doseEquivalent_prod_dose_quality d q, and doseEquivalentOf_isProduct is rfl. The same families give specificActivityOf (= A/m) and the reciprocal/quotient kind-laws meanLife_recip_decayConstant, absorbedDoseRate_quot_dose_duration, and massAttenuation_quot_linear_density, crossing to ISO 80000-3 and -4.