21.7. The algebraic Remarks as kind-laws🔗

Many Part-3 remarks state a quantity's defining relation algebraically — as a quotient or a reciprocal of other quantities. Curvature is 1/ρ (item 3-2); repetency is 1/λ (3-20); frequency is 1/T (3-17.1); speed is ds/dt, path length per duration (3-10.2); a plane angle is s/r, arc length per radius (3-5). Each is formalized as an R12 kind-law over the catalogued kinds, using the quotient and reciprocal families.

Theorem21.7.1

groupuses 1used by 0✓L∃∀N

EffortsmallTagsproved

Under the SI's α = s/r, a plane angle computes to dimension one. Taking arc and radius as plain lengths, the remark α = s/r cancels the dimension — a checked computation that reproduces the current SI convention, not one that settles it. That the relation forces dimensionlessness is exactly what the metrology reform disputes: Quincey, Mohr and Phillips (Quincey, Mohr, and Phillips, 2019)Paul Quincey, Peter J. Mohr, and William D. Phillips (2019). “Angles are inherently neither length ratios nor dimensionless”. Metrologia. 56(4). argue an angle is inherently neither a length ratio nor dimensionless. PKC formalizes the standard as published and leaves the dimensional stance open — plane angle remains a distinct kind from every other dimension-one quantity (the collision capstone above), which is what keeps the radian and steradian apart whatever dimension the SI assigns. Uses the dimension map.

Lean code for Theorem21.7.1●1 theorem

theoremdefined in PropertyKindCalculus/Iso80000/Part3/DefiningRelations.lean

complete

theorem PropertyKindCalculus.Iso80000.Part3.DefiningRelations.planeAngle_dim_from_arc_over_radius :
  PropertyKindCalculus.Iso80000.Part3.planeAngle.dim
      LTMCTDimensionBase =
    PropertyKindCalculus.Iso80000.Part3.pathLength.dim
        LTMCTDimensionBase /
      PropertyKindCalculus.Iso80000.Part3.radius.dim LTMCTDimensionBase

theorem PropertyKindCalculus.Iso80000.Part3.DefiningRelations.planeAngle_dim_from_arc_over_radius :
  PropertyKindCalculus.Iso80000.Part3.planeAngle.dim
      LTMCTDimensionBase =
    PropertyKindCalculus.Iso80000.Part3.pathLength.dim
        LTMCTDimensionBase /
      PropertyKindCalculus.Iso80000.Part3.radius.dim
        LTMCTDimensionBase

**Under the SI's `α = s/r`, plane angle computes to dimension one.** With arc and
radius taken as plain lengths, `s/r` cancels the dimension — a checked computation
that reproduces the *current SI convention* rather than settling it. That the relation
*forces* dimensionlessness is exactly what the metrology reform literature disputes:
read arc and radius as carrying an angle dimension and `s/r` need not be dimensionless.
PKC formalizes the standard as published and leaves the dimensional stance open —
plane angle nonetheless stays a distinct *kind* from every other dimension-one quantity
(see `Part3.iso80000_3_dim_one_collision`), which is what keeps the radian and the
steradian non-interchangeable, whatever dimension the SI ultimately assigns.

Proof for Theorem 21.7.1

uses 0

planeAngle_dim_from_arc_over_radius : planeAngle.dim = pathLength.dim / radius.dim, by reducing both sides to Dim.length / Dim.length and the lemma length_div_length (a / a = 1, by ext and simp).

Theorem21.7.2

groupuses 1used by 0✓L∃∀N

EffortsmallTagsproved

Verified construction at the quantity level. A frequency built as the reciprocal of a period duration carries its classification certificate by construction, over the ℝ carrier — and canonicity makes that certificate determine the quantity. Uses the reciprocal kind-law.

Lean code for Theorem21.7.2●1 theorem

theoremdefined in PropertyKindCalculus/Iso80000/Part3/DefiningRelations.lean

complete

theorem PropertyKindCalculus.Iso80000.Part3.DefiningRelations.frequencyOf_isReciprocal
  (T :
    PropertyKindCalculus.Quantity
      (PropertyKindCalculus.Iso80000.Part3.periodDuration.kind
        LTMCTDimensionBase)
      ℝ) :
  PropertyKindCalculus.Quantity.IsReciprocal
    PropertyKindCalculus.Iso80000.Part3.DefiningRelations.frequency_recip_periodDuration
    (PropertyKindCalculus.Iso80000.Part3.DefiningRelations.frequencyOf
      T)
    T

theorem PropertyKindCalculus.Iso80000.Part3.DefiningRelations.frequencyOf_isReciprocal
  (T :
    PropertyKindCalculus.Quantity
      (PropertyKindCalculus.Iso80000.Part3.periodDuration.kind
        LTMCTDimensionBase)
      ℝ) :
  PropertyKindCalculus.Quantity.IsReciprocal
    PropertyKindCalculus.Iso80000.Part3.DefiningRelations.frequency_recip_periodDuration
    (PropertyKindCalculus.Iso80000.Part3.DefiningRelations.frequencyOf
      T)
    T

The constructed frequency satisfies the reciprocal certificate by construction.

Proof for Theorem 21.7.2

uses 0

frequencyOf T := Quantity.recip frequency_recip_periodDuration T, and frequencyOf_isReciprocal is rfl; frequency_certificate_canonical is eq_recip_of_isReciprocal. The kind-law frequency_recip_periodDuration is ⟨rfl, rfl⟩ (both kinds ratio-scale). The same families give speedOf (speed = path length / duration) and planeAngleOf (plane angle = arc / radius).