22.4. The algebraic Remarks as kind-laws: mechanics built from space and time🔗

Many Part-4 remarks state a quantity's defining relation algebraically — and, in mechanics, the other quantities are often space-and-time quantities from Part 3. Momentum is mass × velocity (4-8); pressure is force / area (4-14.1); mass density is mass / volume (4-2); specific volume is 1/ρ (4-3); kinematic viscosity is η/ρ (4-25); efficiency is output power / input power (4-29); a modulus of elasticity is stress / strain (4-19.1). Each is formalized as an R12 kind-law over the catalogued kinds, several composing a Part-4 kind out of Part-3 kinds.

Theorem22.4.1

groupuses 1used by 0✓L∃∀N

EffortsmallTagsproved

Momentum is mass × velocity — a verified, cross-part construction. A momentum built as the product of a mass (Part 4) and a velocity (Part 3) carries its product certificate by construction, over the ℝ carrier, and canonicity makes the certificate determine the quantity. Uses the product kind-law.

Lean code for Theorem22.4.1●1 theorem

theoremdefined in PropertyKindCalculus/Iso80000/Part4/DefiningRelations.lean

complete

theorem PropertyKindCalculus.Iso80000.Part4.DefiningRelations.momentumOf_isProduct
  (m :
    PropertyKindCalculus.Quantity
      (PropertyKindCalculus.Iso80000.Part4.mass.kind LTMCTDimensionBase)
      ℝ)
  (v :
    PropertyKindCalculus.Quantity
      (PropertyKindCalculus.Iso80000.Part3.velocity.kind
        LTMCTDimensionBase)
      ℝ) :
  PropertyKindCalculus.Quantity.IsProduct
    PropertyKindCalculus.Iso80000.Part4.DefiningRelations.momentum_prod_mass_velocity
    (PropertyKindCalculus.Iso80000.Part4.DefiningRelations.momentumOf m
      v)
    m v

theorem PropertyKindCalculus.Iso80000.Part4.DefiningRelations.momentumOf_isProduct
  (m :
    PropertyKindCalculus.Quantity
      (PropertyKindCalculus.Iso80000.Part4.mass.kind
        LTMCTDimensionBase)
      ℝ)
  (v :
    PropertyKindCalculus.Quantity
      (PropertyKindCalculus.Iso80000.Part3.velocity.kind
        LTMCTDimensionBase)
      ℝ) :
  PropertyKindCalculus.Quantity.IsProduct
    PropertyKindCalculus.Iso80000.Part4.DefiningRelations.momentum_prod_mass_velocity
    (PropertyKindCalculus.Iso80000.Part4.DefiningRelations.momentumOf
      m v)
    m v

The constructed momentum satisfies the product certificate by construction.

Proof for Theorem 22.4.1

uses 0

momentumOf m v := Quantity.mul momentum_prod_mass_velocity m v, and momentumOf_isProduct is rfl; momentum_certificate_canonical is eq_mul_of_isProduct. The kind-law momentum_prod_mass_velocity : ProductKind mass.kind Part3.velocity.kind momentum.kind is ⟨rfl, rfl, rfl⟩, and momentum_dim_from_mass_velocity checks M·L·T⁻¹ follows from the relation. The same families give pressureOf (pressure = force / area) and efficiencyOf.

Theorem22.4.2

groupuses 1used by 0✓L∃∀N

EffortsmallTagsproved

Efficiency is dimension one because it is a ratio of two powers. From the remark η = P_out/P_in, the powers cancel and the dimension is computed to be one — not stipulated, the mechanics analogue of the plane angle being a ratio of two lengths. Yet efficiency remains a distinct kind from every other dimension-one quantity (the collision capstone above). Uses the dimension map.

Lean code for Theorem22.4.2●1 theorem

theoremdefined in PropertyKindCalculus/Iso80000/Part4/DefiningRelations.lean

complete

theorem PropertyKindCalculus.Iso80000.Part4.DefiningRelations.efficiency_dim_from_power_ratio :
  PropertyKindCalculus.Iso80000.Part4.efficiency.dim
      LTMCTDimensionBase =
    PropertyKindCalculus.Iso80000.Part4.power.dim LTMCTDimensionBase /
      PropertyKindCalculus.Iso80000.Part4.power.dim LTMCTDimensionBase

theorem PropertyKindCalculus.Iso80000.Part4.DefiningRelations.efficiency_dim_from_power_ratio :
  PropertyKindCalculus.Iso80000.Part4.efficiency.dim
      LTMCTDimensionBase =
    PropertyKindCalculus.Iso80000.Part4.power.dim
        LTMCTDimensionBase /
      PropertyKindCalculus.Iso80000.Part4.power.dim
        LTMCTDimensionBase

**Efficiency is dimension one because it is a ratio of two powers.** Output and
input power are both `M·L²·T⁻³`, so `η = P_out/P_in` cancels the dimension — the
efficiency's dimensionlessness is a *checked computation from its defining relation*,
not a stipulation. (It nonetheless remains a distinct kind from every other
dimension-one quantity; see `Part4.iso80000_4_dim_one_collision`.) This is the
mechanics analogue of the plane angle being a ratio of two lengths.

Proof for Theorem 22.4.2

uses 0

efficiency_dim_from_power_ratio : efficiency.dim = power.dim / power.dim, by reducing both sides via div_self' (a / a = 1). The kind-law efficiency_quot_power_power is ⟨rfl, rfl, rfl⟩ and efficiencyOf builds a certified efficiency from two powers.