26.4. The algebraic Remarks as kind-laws: linear acoustics built by the kind algebra🔗

Several Part-8 definitions state a quantity's defining relation algebraically — the constitutive laws of linear acoustics. Sound particle velocity is the time-derivative of displacement (8-4), acceleration of velocity (8-5); sound intensity is the product of sound pressure and particle velocity (8-10, I = p·u); the two impedances are quotients of sound pressure (8-12, 8-13). Each is specified as an R12 kind-law, the kinematics crossing to ISO 80000-3 for time.

Theorem26.4.1

uses 1used by 0✓L∃∀N

EffortsmallTagsproved

Sound intensity is sound pressure × particle velocity — a verified construction (item 8-10). A sound intensity built as the product of a sound pressure and a particle velocity carries its product certificate by construction, over the ℝ carrier. The companion soundIntensity_dim_from_pressure_velocity shows the intensity is M·T⁻³ because the length in pressure and velocity cancels — the acoustic intensity law as a checked computation. Uses the quotient kind-law.

Lean code for Theorem26.4.1●1 theorem

theoremdefined in PropertyKindCalculus/Iso80000/Part8/DefiningRelations.lean

complete

theorem PropertyKindCalculus.Iso80000.Part8.DefiningRelations.soundIntensityOf_isProduct
  (p :
    PropertyKindCalculus.Quantity
      (PropertyKindCalculus.Iso80000.Part8.soundPressure.kind
        LTMCTDimensionBase)
      ℝ)
  (u :
    PropertyKindCalculus.Quantity
      (PropertyKindCalculus.Iso80000.Part8.particleVelocity.kind
        LTMCTDimensionBase)
      ℝ) :
  PropertyKindCalculus.Quantity.IsProduct
    PropertyKindCalculus.Iso80000.Part8.DefiningRelations.soundIntensity_prod_pressure_velocity
    (PropertyKindCalculus.Iso80000.Part8.DefiningRelations.soundIntensityOf
      p u)
    p u

theorem PropertyKindCalculus.Iso80000.Part8.DefiningRelations.soundIntensityOf_isProduct
  (p :
    PropertyKindCalculus.Quantity
      (PropertyKindCalculus.Iso80000.Part8.soundPressure.kind
        LTMCTDimensionBase)
      ℝ)
  (u :
    PropertyKindCalculus.Quantity
      (PropertyKindCalculus.Iso80000.Part8.particleVelocity.kind
        LTMCTDimensionBase)
      ℝ) :
  PropertyKindCalculus.Quantity.IsProduct
    PropertyKindCalculus.Iso80000.Part8.DefiningRelations.soundIntensity_prod_pressure_velocity
    (PropertyKindCalculus.Iso80000.Part8.DefiningRelations.soundIntensityOf
      p u)
    p u

The constructed sound intensity satisfies the product certificate by construction.

Proof for Theorem 26.4.1

uses 0

soundIntensityOf p u := Quantity.mul soundIntensity_prod_pressure_velocity p u, and soundIntensityOf_isProduct is rfl. The same family gives the quotient constructors characteristicImpedanceOf (= p/u) and the cross-part kinematic laws particleVelocity_quot_displacement_duration (= displacement / time), the time crossing to ISO 80000-3.