22.3. Dimension does not classify; the kind does — the torque/energy case🔗

Part 4 holds the textbook example of a dimension collision. Torque (moment of force, 4-12.1/4-12.2) and energy (work, 4-28) are both M·L²·T⁻² — yet they are distinct kinds, measured in distinct units: the newton metre is reserved for torque, the joule for energy, precisely because they are different kinds. And Part 4 is dense with such collisions: momentum and impulse (M·L·T⁻¹); angular momentum, angular impulse, and action (M·L²·T⁻¹); pressure, stress, and the three elastic moduli (M·L⁻¹·T⁻²); and a whole dimension-one family — the relative densities, the strains, the Poisson number, the friction factors, the drag coefficient, and the efficiency.

Theorem22.3.1

Group: These are the dimension-disambiguation capstone, on standard quantities: 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 22.3.2

Loading preview

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

uses 1used by 0✓L∃∀N

EffortsmallTagsproved

Torque is not energy, though both are M·L²·T⁻². There exist distinct ISO 80000-4 kinds with the same dimension — torque and energy witness it. No dimension-only type system can separate them; the kind layer does. This is the textbook case that a dimension does not classify a quantity. Uses the dimension map.

Lean code for Theorem22.3.1●1 theorem

theoremdefined in PropertyKindCalculus/Iso80000/Part4.lean

complete

theorem PropertyKindCalculus.Iso80000.Part4.iso80000_4_dim_collision :
  ∃ a b,
    a.kind LTMCTDimensionBase ≠ b.kind LTMCTDimensionBase ∧
      a.dim LTMCTDimensionBase = b.dim LTMCTDimensionBase

theorem PropertyKindCalculus.Iso80000.Part4.iso80000_4_dim_collision :
  ∃ a b,
    a.kind LTMCTDimensionBase ≠
        b.kind LTMCTDimensionBase ∧
      a.dim LTMCTDimensionBase =
        b.dim LTMCTDimensionBase

**The torque/energy collision, on standard quantities.** There exist distinct
ISO 80000-4 kinds with the same dimension `M·L²·T⁻²` — torque and energy witness it.
PhysLib's `Dimension`, and any dimension-only type system, cannot separate them; the
kind layer does. This is the textbook dimension-does-not-classify case.

Proof for Theorem 22.3.1

uses 0

iso80000_4_dim_collision : ∃ a b : DimensionedKind, a.kind ≠ b.kind ∧ a.dim = b.dim, witnessed by ⟨torque, mechanicalEnergy, …⟩ with torque_ne_energy (a decide) and reflexivity. The companion momentum_ne_impulse is the M·L·T⁻¹ case. Axiom-free.

Theorem22.3.2

Group member previews

Preview

Theorem 22.3.1

Loading preview

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

uses 1used by 0✓L∃∀N

EffortsmallTagsproved

A newton metre is not a joule, though both are M·L²·T⁻². The SI units of torque and energy are not commensurable, because their kinds differ — the unit-level form of the torque/energy collision, a type-level fact the dimension cannot see. Uses metrological units.

Lean code for Theorem22.3.2●1 theorem

theoremdefined in PropertyKindCalculus/Iso80000/Part4.lean

complete

theorem PropertyKindCalculus.Iso80000.Part4.newtonMetre_joule_not_commensurable :
  ¬PropertyKindCalculus.Iso80000.Part4.newtonMetre.Commensurable
      PropertyKindCalculus.Iso80000.Part4.joule

theorem PropertyKindCalculus.Iso80000.Part4.newtonMetre_joule_not_commensurable :
  ¬PropertyKindCalculus.Iso80000.Part4.newtonMetre.Commensurable
      PropertyKindCalculus.Iso80000.Part4.joule

**The newton metre is not a joule, though both are `M·L²·T⁻²`.** The SI units of
torque and energy are not commensurable, because their kinds differ — the textbook
case that a dimension does not determine a unit.

Proof for Theorem 22.3.2

uses 0

newtonMetre_joule_not_commensurable : ¬ newtonMetre.Commensurable joule by unfolding to the underlying kinds and decide (torque's kind differs from the energy kind).

Theorem22.3.3

Group member previews

Preview

Theorem 22.3.1

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-4 kinds with the same dimension one — efficiency and the relative mass density witness it, alongside the strains, the Poisson number, and the friction factors. Dimension cannot separate them; the kind layer does. Uses the dimension map.

Lean code for Theorem22.3.3●1 theorem

theoremdefined in PropertyKindCalculus/Iso80000/Part4.lean

complete

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

theorem PropertyKindCalculus.Iso80000.Part4.iso80000_4_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-4 kinds with the same dimension one — efficiency and the relative mass
density witness it (alongside the strains, the Poisson number, and the friction
factors). Dimension cannot separate them; the kind layer does.

Proof for Theorem 22.3.3

uses 0

iso80000_4_dim_one_collision : ∃ a b : DimensionedKind, a.kind ≠ b.kind ∧ a.dim = b.dim ∧ a.dim = 1, witnessed by ⟨efficiency, relativeMassDensity, …⟩ with efficiency_ne_relativeMassDensity (a decide) and reflexivity. Axiom-free.