30.2. Collisions everywhere — the kind classifies where the dimension cannot
ISO 80000-12 makes the catalogue's thesis the norm. Five families each collapse to one dimension:
-
Seven energies — work function, ionization energy, electron affinity, Fermi energy, gap energy, exchange integral, superconductor energy gap — all
M·L²·T⁻². -
Five temperatures — Debye, Fermi, Curie, Néel, superconduction-transition — all
Θ, and all in the kelvin. -
Thirteen lengths — lattice and position vectors, spacings, mean free paths, the penetration and coherence lengths — all
L. -
Five carrier densities and five reciprocal lengths — all
L⁻³andL⁻¹.
A dimension-only model sees one type per family; the kind layer keeps the Fermi energy from the gap energy, the Curie temperature from the Néel temperature, the lattice spacing from the Burgers vector. The five named temperatures are the sharpest case: one dimension, one unit symbol, five kinds.
Fermi energy is not gap energy, though both are J and M·L²·T⁻² (items 12-27.1,
12-27.2). There exist distinct ISO 80000-12 kinds with the same dimension — the seven
energies witness it. No dimension-only type system can separate them; the kind layer — and
the unit — does. Uses the dimension map.
Lean code for Theorem30.2.1●1 theorem
Associated Lean declarations
-
theoremdefined in PropertyKindCalculus/Iso80000/Part12.leancomplete
theorem PropertyKindCalculus.Iso80000.Part12.iso80000_12_dim_collision : ∃ a b, a.kind LTMCTDimensionBase ≠ b.kind LTMCTDimensionBase ∧ a.dim LTMCTDimensionBase = b.dim LTMCTDimensionBase
theorem PropertyKindCalculus.Iso80000.Part12.iso80000_12_dim_collision : ∃ a b, a.kind LTMCTDimensionBase ≠ b.kind LTMCTDimensionBase ∧ a.dim LTMCTDimensionBase = b.dim LTMCTDimensionBase
**The dimension-collision capstone, on the standard — collisions everywhere.** There exist distinct ISO 80000-12 kinds with the same dimension `M·L²·T⁻²` — the Fermi energy and the gap energy witness it, alongside the work function, ionization energy, electron affinity, exchange integral, and superconductor energy gap (seven energies). The {dimension functor} cannot separate them; the kind layer does.
iso80000_12_dim_collision, witnessed by ⟨fermiEnergy, gapEnergy, …⟩. The unit fact
jouleFermi_jouleGap_not_commensurable is a decide; the companions
latticePlaneSpacing_dim_eq_burgersVector_dim (the length family) and
curieTemperature_dim_eq_neelTemperature_dim (the temperature family) record the other
collisions. Axiom-free.
The kelvin of the Curie temperature and the kelvin of the Néel temperature are not
commensurable, though both are Θ (items 12-35.1, 12-35.2). Five named temperatures — the
Debye, Fermi, Curie, Néel, and superconduction-transition — share one dimension and one
unit symbol, and only the kind tells them apart. Uses the
metrological unit.
Lean code for Theorem30.2.2●1 theorem
Associated Lean declarations
-
theoremdefined in PropertyKindCalculus/Iso80000/Part12.leancomplete
theorem PropertyKindCalculus.Iso80000.Part12.kelvinCurie_kelvinNeel_not_commensurable : ¬PropertyKindCalculus.Iso80000.Part12.kelvinCurie.Commensurable PropertyKindCalculus.Iso80000.Part12.kelvinNeel
theorem PropertyKindCalculus.Iso80000.Part12.kelvinCurie_kelvinNeel_not_commensurable : ¬PropertyKindCalculus.Iso80000.Part12.kelvinCurie.Commensurable PropertyKindCalculus.Iso80000.Part12.kelvinNeel
**The kelvin of Curie temperature and the kelvin of Néel temperature are not commensurable, though both are `Θ`.** Five named temperatures, one dimension, one unit symbol — the kind layer keeps them apart.
kelvinCurie_kelvinNeel_not_commensurable, by decide after unfolding
MetrologicalUnit.Commensurable. Axiom-free.
The dimension-1 disambiguation, on the standard. There exist distinct ISO 80000-12 kinds with the same dimension one — the Bragg angle and the structure factor witness it, alongside the order parameters, the atomic scattering factor, the Debye-Waller factor, the Grüneisen parameters, and the mobility ratio. Dimension cannot separate them; the kind layer does. Uses the dimension map.
Lean code for Theorem30.2.3●1 theorem
Associated Lean declarations
-
theoremdefined in PropertyKindCalculus/Iso80000/Part12.leancomplete
theorem PropertyKindCalculus.Iso80000.Part12.iso80000_12_dim_one_collision : ∃ a b, a.kind LTMCTDimensionBase ≠ b.kind LTMCTDimensionBase ∧ a.dim LTMCTDimensionBase = b.dim LTMCTDimensionBase ∧ a.dim LTMCTDimensionBase = 1
theorem PropertyKindCalculus.Iso80000.Part12.iso80000_12_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.** There exist distinct ISO 80000-12 kinds with the same dimension one — the Bragg angle and the structure factor witness it, alongside the order parameters, the scattering factor, the Debye-Waller factor, the Grüneisen parameters, and the mobility ratio. Dimension cannot separate them; the kind layer does.
iso80000_12_dim_one_collision, witnessed by ⟨braggAngle, structureFactor, …⟩ with the
kind distinction a decide and reflexivity. Axiom-free.