25.3. Dimension does not classify; the kind does — the widest collisions in the series🔗

ISO 80000-7 holds the widest dimension collisions of the catalogue. The candela reducing to power and the steradian to one, radiant flux, luminous flux, radiant intensity, and luminous intensity all share M·L²·T⁻³; radiance, luminance, irradiance, illuminance, and the exitances all share M·T⁻³; and over two dozen kinds — refractive index, the efficiencies and efficacies, emissivity, the absorptances, reflectances, and transmittances, the optical densities, the radiance and luminance factors, the chromaticity coordinates, the colour-matching functions, the photon number — share dimension one.

Theorem25.3.1

groupuses 1used by 0✓L∃∀N

EffortsmallTagsproved

Radiant flux is not luminous flux, though both are M·L²·T⁻³. There exist distinct ISO 80000-7 kinds with the same dimension — radiant and luminous flux witness it, alongside radiant and luminous intensity. The candela reduces to power, so no dimension-only type system can separate them; the kind layer — and the unit, W versus lm — does. This is a collision between a base-quantity unit and a derived one, the scale-spanning case (R13) on the standard. Uses the dimension map.

Lean code for Theorem25.3.1●1 theorem

theoremdefined in PropertyKindCalculus/Iso80000/Part7.lean

complete

theorem PropertyKindCalculus.Iso80000.Part7.iso80000_7_dim_collision :
  ∃ a b,
    a.kind LTMCTDimensionBase ≠ b.kind LTMCTDimensionBase ∧
      a.dim LTMCTDimensionBase = b.dim LTMCTDimensionBase

theorem PropertyKindCalculus.Iso80000.Part7.iso80000_7_dim_collision :
  ∃ a b,
    a.kind LTMCTDimensionBase ≠
        b.kind LTMCTDimensionBase ∧
      a.dim LTMCTDimensionBase =
        b.dim LTMCTDimensionBase

**The scale-spanning collision capstone, on the standard.** There exist distinct
ISO 80000-7 kinds with the same dimension `M·L²·T⁻³` — radiant flux and luminous flux
witness it (alongside radiant and luminous intensity). The candela reduces to power, so
the {dimension functor} cannot separate them; the kind layer — and the unit, `W` versus
`lm` — does. This is the dimension-does-not-classify case at its sharpest: the collision
is between a base-quantity unit (the candela) and a derived one.

Proof for Theorem 25.3.1

uses 0

iso80000_7_dim_collision : ∃ a b : DimensionedKind, a.kind ≠ b.kind ∧ a.dim = b.dim, witnessed by ⟨radiantFlux, luminousFlux, …⟩. The companion radiantFlux_dim_eq_radiantIntensity_dim is the steradian collision (flux versus intensity, the steradian being dimension one), and wattRadiant_lumen_not_commensurable / wattRadiant_wattPerSteradian_not_commensurable record the unit-level facts. Axiom-free.

Theorem25.3.2

groupuses 1used by 0✓L∃∀N

EffortsmallTagsproved

The dimension-1 disambiguation, on the standard — the widest in the series. There exist distinct ISO 80000-7 kinds with the same dimension one — refractive index and emissivity witness it, alongside the efficiencies, efficacies, absorptances, reflectances, transmittances, optical densities, the radiance and luminance factors, the reflectance factor, the chromaticity coordinates, the colour-matching functions, and the photon number. Dimension cannot separate them; the kind layer does. Uses the dimension map.

Lean code for Theorem25.3.2●1 theorem

theoremdefined in PropertyKindCalculus/Iso80000/Part7.lean

complete

theorem PropertyKindCalculus.Iso80000.Part7.iso80000_7_dim_one_collision :
  ∃ a b,
    a.kind LTMCTDimensionBase ≠ b.kind LTMCTDimensionBase ∧
      a.dim LTMCTDimensionBase = b.dim LTMCTDimensionBase ∧
        a.dim LTMCTDimensionBase = 1

theorem PropertyKindCalculus.Iso80000.Part7.iso80000_7_dim_one_collision :
  ∃ a b,
    a.kind LTMCTDimensionBase ≠
        b.kind LTMCTDimensionBase ∧
      a.dim LTMCTDimensionBase =
          b.dim LTMCTDimensionBase ∧
        a.dim LTMCTDimensionBase = 1

**The dimension-one disambiguation, on the standard — the widest in the series.**
There exist distinct ISO 80000-7 kinds with the same dimension one — refractive index
and emissivity witness it, alongside the efficiencies, efficacies, absorptances,
reflectances, transmittances, optical densities, the radiance and luminance factors, the
reflectance factor, the chromaticity coordinates, the colour-matching functions, and the
photon number. Dimension cannot separate them; the kind layer does.

Proof for Theorem 25.3.2

uses 0

iso80000_7_dim_one_collision : ∃ a b : DimensionedKind, a.kind ≠ b.kind ∧ a.dim = b.dim ∧ a.dim = 1, witnessed by ⟨refractiveIndex, emissivity, …⟩ with refractiveIndex_ne_emissivity (a decide) and reflexivity. Axiom-free.