26.3. A dimension collision, and the boundary where the dimension does classify🔗

ISO 80000-8 shows both sides of the thesis. Sound pressure (8-2.2, Pa) and sound energy density (8-7, J/m³) carry the same dimension M·L⁻¹·T⁻² — pressure being force per area, energy density energy per volume, and the two equal — yet are different kinds: a collision the dimension cannot resolve.

But the part also marks the boundary. It lists two quantities both called an impedance: the characteristic impedance of a medium (8-12, Pa·s/m, M·L⁻²·T⁻¹) and the acoustic impedance (8-13, Pa·s/m³, M·L⁻⁴·T⁻¹). Here the dimension does tell the homonyms apart, because one is pressure over particle velocity and the other pressure over volume flow rate — the extra L² shows. Dimension is a necessary discriminator of kind, never a sufficient one; the impedances are the case where, this once, it is also sufficient, and naming them makes the limit of the dimension test explicit.

Theorem26.3.1

uses 1used by 0✓L∃∀N

EffortsmallTagsproved

Sound pressure is not sound energy density, though both are M·L⁻¹·T⁻² (items 8-2.2, 8-7). There exist distinct ISO 80000-8 kinds with the same dimension — sound pressure and sound energy density witness it. Force per area equals energy per volume, so no dimension-only type system can separate them; the kind layer — and the unit, Pa versus J/m³ — does. Uses the dimension map.

Lean code for Theorem26.3.1●1 theorem

theoremdefined in PropertyKindCalculus/Iso80000/Part8.lean

complete

theorem PropertyKindCalculus.Iso80000.Part8.iso80000_8_dim_collision :
  ∃ a b,
    a.kind LTMCTDimensionBase ≠ b.kind LTMCTDimensionBase ∧
      a.dim LTMCTDimensionBase = b.dim LTMCTDimensionBase

theorem PropertyKindCalculus.Iso80000.Part8.iso80000_8_dim_collision :
  ∃ a b,
    a.kind LTMCTDimensionBase ≠
        b.kind LTMCTDimensionBase ∧
      a.dim LTMCTDimensionBase =
        b.dim LTMCTDimensionBase

**The dimension collision capstone, on the standard.** There exist distinct
ISO 80000-8 kinds with the same dimension — sound pressure and sound energy density
witness it (`M·L⁻¹·T⁻²`), as do the three logarithmic levels at dimension one. The
{dimension functor} cannot separate them; the kind layer — and the unit, `Pa` versus
`J/m³` — does.

Proof for Theorem 26.3.1

uses 0

iso80000_8_dim_collision : ∃ a b : DimensionedKind, a.kind ≠ b.kind ∧ a.dim = b.dim, witnessed by ⟨soundPressure, soundEnergyDensity, …⟩. The dimension equality soundPressure_dim_eq_energyDensity_dim is a Dimension.ext computation (force/area = energy/volume); pascalSound_joulePerCubicMetre_not_commensurable records the unit-level fact. The contrasting acousticImpedance_dim_from_pressure_volumeFlow shows where the dimension instead discriminates. Axiom-free.