25.2. The radiant / luminous / photon trios
ISO 80000-7 lists most measurands three times — a radiant (energetic, subscript e)
version, a luminous (photopic, subscript v) version, and a photon (count, subscript p)
version — and pairs them explicitly ("the corresponding photometric quantity is …"). They
are not the same kind of quantity: radiant flux is the total radiant power, luminous flux
its V(λ)-weighted response in the human eye, photon flux a count rate. A dimension-only
model sees one type, "a real number of watts", for radiant and luminous flux, and cannot
say why a count rate is a different thing again.
This is requirement R2 once more — the pattern Part 3 set on the length family, Part 4
on the force family, Part 5 on the thermodynamic potentials, Part 6 on the AC power
quantities — now on the radiation trios. Each member is a distinct kind individuated
not by fiat but by a radiation mode (Dybkær's examination principle, §7.5). And the
trios split two ways: the luminous mode is a dimensionless reweighting (luminous flux ≡
radiant flux in dimension), while the photon mode is a genuine re-dimensioning (photon
flux is T⁻¹, not M·L²·T⁻³).
A radiation-mode kind is a ratio-scale quantity-kind carrying an
examination principle — this work's terse descriptor of which
aspect of the radiation it isolates: the total energetics (subscript e), the
V(λ)-weighted photopic response (subscript v), or a photon count (subscript p). The
radiant, luminous, and photon members of each measurand's trio differ in this principle.
Lean code for Definition25.2.1●1 definition
Associated Lean declarations
-
defdefined in PropertyKindCalculus/Iso80000/Part7.leancomplete
def PropertyKindCalculus.Iso80000.Part7.modeKind (id : String) (m : PropertyKindCalculus.ExaminationPrinciple) (dim : Dimension LTMCTDimensionBase) : PropertyKindCalculus.DimensionedKind LTMCTDimensionBase
def PropertyKindCalculus.Iso80000.Part7.modeKind (id : String) (m : PropertyKindCalculus.ExaminationPrinciple) (dim : Dimension LTMCTDimensionBase) : PropertyKindCalculus.DimensionedKind LTMCTDimensionBase
A ratio-scale dimensioned kind individuated by its radiation mode (examination principle).
modeKind id m dim := { kind := { id, scale := .ratio, examPrinciple := some m.id }, dim },
with the three modes RadiationMode.energetic, .photopic, .photonic. The flux trio is
radiantFlux / luminousFlux / photonFlux, and likewise for energy, intensity,
radiance, irradiance, exitance, and exposure.
Radiant and luminous flux are distinct kinds — by radiation mode, not by fiat. They
share dimension M·L²·T⁻³ and are both "flux", yet are different kinds because one is the
total radiant power and the other its V(λ)-weighted photopic response — proved through
distinct_of_examPrinciple (§7.5). The photon member is distinct again, and even
re-dimensions (T⁻¹). This is the AC-power-family pattern of Part 6 on the radiation
trios. Uses the examination principle.
Lean code for Theorem25.2.2●1 theorem
Associated Lean declarations
-
theoremdefined in PropertyKindCalculus/Iso80000/Part7.leancomplete
theorem PropertyKindCalculus.Iso80000.Part7.radiantFlux_ne_luminousFlux : PropertyKindCalculus.Iso80000.Part7.radiantFlux.kind LTMCTDimensionBase ≠ PropertyKindCalculus.Iso80000.Part7.luminousFlux.kind LTMCTDimensionBase
theorem PropertyKindCalculus.Iso80000.Part7.radiantFlux_ne_luminousFlux : PropertyKindCalculus.Iso80000.Part7.radiantFlux.kind LTMCTDimensionBase ≠ PropertyKindCalculus.Iso80000.Part7.luminousFlux.kind LTMCTDimensionBase
**Radiant flux and luminous flux are distinct kinds — by radiation mode, not by fiat.** They share dimension `M·L²·T⁻³` and are both "flux", yet differ because one is the total radiant power and the other its `V(λ)`-weighted photopic response — proved through `distinct_of_examPrinciple`. This is the candela's scale-spanning collision (R13) realized as a kind distinction.
radiantFlux_ne_luminousFlux : radiantFlux.kind ≠ luminousFlux.kind, from
KindOfProperty.distinct_of_examPrinciple on the differing modes radiant-energetic and
luminous-photopic-Vlambda. The companions radiantFlux_ne_photonFlux (the photon mode)
and radiance_ne_luminance cover further trios; radiantFlux_examinedBy and
luminousFlux_examinedBy check the kind-to-mode links. Axiom-free.
The luminous efficacy is dimension one because it is a ratio of two fluxes (item 7-11.1).
From K = Φ_v/Φ_e, with luminous and radiant flux of equal dimension (the candela
reducing to power), the dimension cancels and the efficacy is computed to be one — the
photometric analogue of the power factor (Part 6) and the plane angle (Part 3). The scale
coefficient K_cd = 683 lm/W is the candela's scale-spanning constant (R13). Uses
the dimension map and the quotient kind-law.
Lean code for Theorem25.2.3●1 theorem
Associated Lean declarations
-
theoremdefined in PropertyKindCalculus/Iso80000/Part7/DefiningRelations.leancomplete
theorem PropertyKindCalculus.Iso80000.Part7.DefiningRelations.luminousEfficacy_dim_from_fluxes : PropertyKindCalculus.Iso80000.Part7.luminousEfficacy.dim LTMCTDimensionBase = PropertyKindCalculus.Iso80000.Part7.luminousFlux.dim LTMCTDimensionBase / PropertyKindCalculus.Iso80000.Part7.radiantFlux.dim LTMCTDimensionBase
theorem PropertyKindCalculus.Iso80000.Part7.DefiningRelations.luminousEfficacy_dim_from_fluxes : PropertyKindCalculus.Iso80000.Part7.luminousEfficacy.dim LTMCTDimensionBase = PropertyKindCalculus.Iso80000.Part7.luminousFlux.dim LTMCTDimensionBase / PropertyKindCalculus.Iso80000.Part7.radiantFlux.dim LTMCTDimensionBase
**The luminous efficacy is dimension one because it is a ratio of two fluxes of equal dimension.** Luminous and radiant flux are both `M·L²·T⁻³` (the candela reducing to power, R13), so `K = Φ_v/Φ_e` cancels the dimension — the efficacy's dimensionlessness is a *checked computation from its defining relation*, the photometric analogue of the power factor (IEC 80000-6) and the plane angle (ISO 80000-3). It nonetheless remains a distinct kind from every other dimension-one quantity (see `Part7.iso80000_7_dim_one_collision`).
luminousEfficacy_dim_from_fluxes : luminousEfficacy.dim = luminousFlux.dim /
radiantFlux.dim, by reducing the right side via div_self (a / a = 1). The kind-law
luminousEfficacy_quot_fluxes is ⟨rfl, rfl, rfl⟩; the efficacy nonetheless remains a
distinct kind from every other dimension-one quantity (the collision capstone below).