26.2. The logarithmic levels — the acoustic face of dimension one🔗

ISO 80000-8 lists three levels: the sound pressure level (8-14), the sound power level (8-15), and the sound exposure level (8-16). Each is 10·lg(quantity / reference) — a ratio of a quantity to a stated reference, taken on a logarithmic scale, and reported in the decibel. A level is dimension one: the logarithm of a ratio of like quantities. So the dimension functor sends all three to the single point 1, and a dimension-only model sees one type, "a real number of decibels", for all of them.

What keeps them apart is which quantity each is the level of — the pressure, the power, the exposure. This is requirement R1 once more (the dimension does not classify the kind), in the form the part makes vivid: a shared unit symbol dB no more makes the sound pressure level the sound power level than the shared symbol 1 makes a Reynolds number a Froude number (ISO 80000-11).

Theorem26.2.1

groupuses 1used by 0✓L∃∀N

EffortsmallTagsproved

The decibel of sound pressure level and the decibel of sound power level are not commensurable, though both are dB and dimension one (items 8-14, 8-15). Same symbol, same dimension, different kind — the level of pressure is not the level of power. This is the ISO 80000-11 "1" pattern (Reynolds versus Euler) on the acoustic levels. Uses the metrological unit.

Lean code for Theorem26.2.1●1 theorem

theoremdefined in PropertyKindCalculus/Iso80000/Part8.lean

complete

theorem PropertyKindCalculus.Iso80000.Part8.decibelPressure_decibelPower_not_commensurable :
  ¬PropertyKindCalculus.Iso80000.Part8.decibelPressure.Commensurable
      PropertyKindCalculus.Iso80000.Part8.decibelPower

theorem PropertyKindCalculus.Iso80000.Part8.decibelPressure_decibelPower_not_commensurable :
  ¬PropertyKindCalculus.Iso80000.Part8.decibelPressure.Commensurable
      PropertyKindCalculus.Iso80000.Part8.decibelPower

**The decibel of sound pressure level and the decibel of sound power level are not
commensurable, though both have unit symbol `dB` and dimension one.** Same symbol, same
dimension, different kind — the level of pressure is not the level of power. This is the
ISO 80000-11 `"1"` pattern (Reynolds versus Euler) on the acoustic levels.

Proof for Theorem 26.2.1

uses 0

decibelPressure_decibelPower_not_commensurable, by decide after unfolding MetrologicalUnit.Commensurable on the two dimension-one kinds. The companion soundPressureLevel_ne_soundPowerLevel is the underlying kind distinction, and iso80000_8_dim_one_collision packages the dimension-one capstone. Axiom-free.

Theorem26.2.2

groupuses 1used by 0✓L∃∀N

EffortsmallTagsproved

The dimension-1 disambiguation, on the standard. There exist distinct ISO 80000-8 kinds with the same dimension one — the sound pressure level and the sound power level witness it, alongside the sound exposure level and the logarithmic frequency range. The dimension cannot separate them; the kind layer does. Uses the dimension map.

Lean code for Theorem26.2.2●1 theorem

theoremdefined in PropertyKindCalculus/Iso80000/Part8.lean

complete

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

theorem PropertyKindCalculus.Iso80000.Part8.iso80000_8_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-8 kinds with the same dimension one — the sound pressure level and the sound
power level witness it, alongside the sound exposure level and the logarithmic frequency
range. The logarithmic levels are the acoustic face of R1.

Proof for Theorem 26.2.2

uses 0

iso80000_8_dim_one_collision : ∃ a b : DimensionedKind, a.kind ≠ b.kind ∧ a.dim = b.dim ∧ a.dim = 1, witnessed by ⟨soundPressureLevel, soundPowerLevel, …⟩ with the kind distinction a decide and reflexivity. Axiom-free.