24.4. Dimension does not classify; the kind does — the power and impedance cases
Part 6 holds the sharpest dimension collision in the series so far. Active power (6-56),
reactive power (6-60), and apparent power (6-57) are all M·L²·T⁻³, yet they are
distinct kinds — and the collision is sharper than Part 5's joule-per-kelvin, because there
even the unit string agreed, while here the standard itself spends three strings (W,
var, VA) on the one dimension. Resistance (6-46) and reactance (6-51.4) collide the
same way at the ohm — the real and imaginary parts of an impedance — and the relative
permittivity (6-15), relative permeability (6-27), the susceptibilities, the coupling and
leakage factors, and the quality, loss, and power factors fill out the dimension-one family.
Active power is not reactive power, though both are M·L²·T⁻³. There exist distinct
IEC 80000-6 kinds with the same dimension — active and reactive power witness it, alongside
apparent, complex, and non-active power. No dimension-only type system can separate them;
the kind layer does. This is the electromagnetic case that a dimension does not classify a
quantity, sharper than Part 5's. Uses the dimension map.
Lean code for Theorem24.4.1●1 theorem
Associated Lean declarations
-
theoremdefined in PropertyKindCalculus/Iso80000/Part6.leancomplete
theorem PropertyKindCalculus.Iso80000.Part6.iec80000_6_dim_collision : ∃ a b, a.kind LTMCTDimensionBase ≠ b.kind LTMCTDimensionBase ∧ a.dim LTMCTDimensionBase = b.dim LTMCTDimensionBase
theorem PropertyKindCalculus.Iso80000.Part6.iec80000_6_dim_collision : ∃ a b, a.kind LTMCTDimensionBase ≠ b.kind LTMCTDimensionBase ∧ a.dim LTMCTDimensionBase = b.dim LTMCTDimensionBase
**The power collision, on standard quantities.** There exist distinct IEC 80000-6 kinds with the same dimension `M·L²·T⁻³` — active power and reactive power witness it (alongside apparent, complex, and non-active power). PhysLib's `Dimension`, and any dimension-only type system, cannot separate them; the kind layer does — and so do the units, which here even differ in string (`W` vs `var`). This is the electromagnetic dimension-does-not-classify case, sharper than Part 5's joule-per-kelvin.
iec80000_6_dim_collision : ∃ a b : DimensionedKind, a.kind ≠ b.kind ∧ a.dim = b.dim,
witnessed by ⟨activePower, reactivePower, …⟩ with activePower_ne_reactivePower and
reflexivity. The companion resistance_ne_reactance is the ohm case (real vs imaginary
part of an impedance). Axiom-free.
The active-power watt is not the reactive-power var. The units of active and reactive
power carry the same dimension M·L²·T⁻³, yet are not commensurable — and the standard
keeps them apart not only by kind but by string, W versus var, a sharper form of the
rule that neither a dimension nor a unit string determines a kind. Uses
metrological units.
Lean code for Theorem24.4.2●1 theorem
Associated Lean declarations
-
theoremdefined in PropertyKindCalculus/Iso80000/Part6.leancomplete
theorem PropertyKindCalculus.Iso80000.Part6.wattActive_varReactive_not_commensurable : ¬PropertyKindCalculus.Iso80000.Part6.wattActive.Commensurable PropertyKindCalculus.Iso80000.Part6.varReactive
theorem PropertyKindCalculus.Iso80000.Part6.wattActive_varReactive_not_commensurable : ¬PropertyKindCalculus.Iso80000.Part6.wattActive.Commensurable PropertyKindCalculus.Iso80000.Part6.varReactive
**The watt of active power and the var of reactive power are not commensurable, though both are `M·L²·T⁻³`.** The standard spends two different unit strings (`W`, `var`) on one dimension precisely to keep the kinds apart — a sharper form of "a dimension does not determine a kind" than Part 5's joule-per-kelvin, where even the unit string agreed.
wattActive_varReactive_not_commensurable : ¬ wattActive.Commensurable varReactive by
unfolding to the underlying kinds and decide (active power's kind differs from the
reactive-power kind; the units are written "W" and "var").
The dimension-1 disambiguation, on the standard. There exist distinct IEC 80000-6 kinds with the same dimension one — relative permittivity and relative permeability witness it, alongside the susceptibilities, the coupling and leakage factors, and the quality, loss, and power factors. Dimension cannot separate them; the kind layer does. Uses the dimension map.
Lean code for Theorem24.4.3●1 theorem
Associated Lean declarations
-
theoremdefined in PropertyKindCalculus/Iso80000/Part6.leancomplete
theorem PropertyKindCalculus.Iso80000.Part6.iec80000_6_dim_one_collision : ∃ a b, a.kind LTMCTDimensionBase ≠ b.kind LTMCTDimensionBase ∧ a.dim LTMCTDimensionBase = b.dim LTMCTDimensionBase ∧ a.dim LTMCTDimensionBase = 1
theorem PropertyKindCalculus.Iso80000.Part6.iec80000_6_dim_one_collision : ∃ a b, a.kind LTMCTDimensionBase ≠ b.kind LTMCTDimensionBase ∧ a.dim LTMCTDimensionBase = b.dim LTMCTDimensionBase ∧ a.dim LTMCTDimensionBase = 1
**The dimension-1 disambiguation, on standard quantities.** There exist distinct IEC 80000-6 kinds with the same dimension one — relative permittivity and relative permeability witness it (alongside the susceptibilities, the coupling and leakage factors, and the quality, loss, and power factors). Dimension cannot separate them; the kind layer does.
iec80000_6_dim_one_collision : ∃ a b : DimensionedKind, a.kind ≠ b.kind ∧ a.dim = b.dim ∧
a.dim = 1, witnessed by ⟨relativePermittivity, relativePermeability, …⟩ with
relativePermittivity_ne_relativePermeability (a decide) and reflexivity. Axiom-free.