21.3. Dimension does not classify; the kind does🔗

Part 3 alone is dense with dimension collisions — distinct kinds that the dimension functor cannot tell apart. Plane angle, rotational displacement, phase angle, solid angle, rotation, and the logarithmic decrement are all dimension one. Frequency, rotational frequency, angular frequency, angular velocity, and the damping coefficient are all T⁻¹. Velocity and speed are both L·T⁻¹. The dimension is the same; the kind is not — and so the units differ too, a radian is not a steradian and a hertz is not a radian-per-second, though each pair shares a dimension.

Theorem21.3.1

Group: These are the dimension-1 disambiguation capstone, now on standard quantities rather than a constructed example: the dimension map identifies the members of each pair, while the kind layer keeps them apart, both as kinds and as units . (2)

Group member previews

Preview

Theorem 21.3.2

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 0✓L∃∀N

EffortsmallTagsproved

The dimension-1 disambiguation, on the standard. There exist distinct ISO 80000-3 kinds with the same dimension one — plane angle and solid angle witness it. No dimension-only type system can separate them; the kind layer does. This generalizes the calculus's dim_not_injective capstone to the published standard. Uses the dimension map.

Lean code for Theorem21.3.1●1 theorem

theoremdefined in PropertyKindCalculus/Iso80000/Part3.lean

complete

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

theorem PropertyKindCalculus.Iso80000.Part3.iso80000_3_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
ISO 80000-3 kinds with the same dimension one — plane angle and solid angle witness
it. PhysLib's `Dimension`, and any dimension-only type system, cannot separate them;
the kind layer does. (Generalizes `Dimension.dim_not_injective` to the standard.)

Proof for Theorem 21.3.1

uses 0

iso80000_3_dim_one_collision : ∃ a b : DimensionedKind, a.kind ≠ b.kind ∧ a.dim = b.dim ∧ a.dim = 1, witnessed by ⟨planeAngle, solidAngle, …⟩ with planeAngle_ne_solidAngle (a decide) and reflexivity. Axiom-free.

Theorem21.3.2

Group member previews

Preview

Theorem 21.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 0✓L∃∀N

EffortsmallTagsproved

A radian is not a steradian, though both are dimension one. The SI units of plane and solid angle are not commensurable, because their kinds differ — a type-level fact the dimension cannot see. This is exactly the separation the angle-reform literature seeks to install in the dimension layer — Leonard (Leonard, 2021)B. P. Leonard (2021). “Proposal for the dimensionally consistent treatment of angle and solid angle by the International System of Units (SI)”. Metrologia. 58(5). would give angle its own dimension and make solid angle its square. PKC secures it at the kind layer — so it holds whether or not the SI ever assigns angle a dimension — and, having made PhysLib's Dimension parametric in its basis, now realizes the reform itself in an angle-augmented basis where plane angle is a base dimension and solid angle its square. The hertz and the radian-per-second are separated the same way (both T⁻¹). Uses metrological units.

Lean code for Theorem21.3.2●1 theorem

theoremdefined in PropertyKindCalculus/Iso80000/Part3.lean

complete

theorem PropertyKindCalculus.Iso80000.Part3.radian_steradian_not_commensurable :
  ¬PropertyKindCalculus.Iso80000.Part3.radian.Commensurable
      PropertyKindCalculus.Iso80000.Part3.steradian

theorem PropertyKindCalculus.Iso80000.Part3.radian_steradian_not_commensurable :
  ¬PropertyKindCalculus.Iso80000.Part3.radian.Commensurable
      PropertyKindCalculus.Iso80000.Part3.steradian

The radian and the steradian are **not** commensurable — plane angle and solid
angle are distinct kinds, *though both are dimension one*. The kind separates units
the dimension cannot.

Proof for Theorem 21.3.2

uses 0

radian_steradian_not_commensurable : ¬ radian.Commensurable steradian by unfolding to the underlying kinds and decide; hertz_radianPerSecond_not_commensurable is the T⁻¹ companion.

Theorem21.3.3

Group member previews

Preview

Theorem 21.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 0✓L∃∀N

EffortsmallTagsproved

Dimension is not a classifier even away from dimension one. Distinct ISO 80000-3 kinds also share dimensionful dimensions — frequency and angular frequency are both T⁻¹, velocity and speed both L·T⁻¹. Uses the dimension map.

Lean code for Theorem21.3.3●1 theorem

theoremdefined in PropertyKindCalculus/Iso80000/Part3.lean

complete

theorem PropertyKindCalculus.Iso80000.Part3.iso80000_3_dim_collision :
  ∃ a b,
    a.kind LTMCTDimensionBase ≠ b.kind LTMCTDimensionBase ∧
      a.dim LTMCTDimensionBase = b.dim LTMCTDimensionBase

theorem PropertyKindCalculus.Iso80000.Part3.iso80000_3_dim_collision :
  ∃ a b,
    a.kind LTMCTDimensionBase ≠
        b.kind LTMCTDimensionBase ∧
      a.dim LTMCTDimensionBase =
        b.dim LTMCTDimensionBase

**A dimensionful collision.** Distinct ISO 80000-3 kinds also share *dimensionful*
dimensions — frequency and angular frequency are both `T⁻¹`. Dimension is not a
classifier even away from dimension one.

Proof for Theorem 21.3.3

uses 0

iso80000_3_dim_collision, witnessed by ⟨frequency, angularFrequency, …⟩ with frequency_ne_angularFrequency (a decide) and reflexivity; velocity_ne_speed is the L·T⁻¹ companion. Axiom-free.