A Property Kind Calculus for Measurement Metrology

22.2. The force family: distinguishing kinds by measurement principle🔗

ISO 80000-4 lists weight (4-9.2), static friction force (4-9.3), kinetic friction force (4-9.4), rolling resistance (4-9.5), and drag force (4-9.6) as separate items — yet every one has dimension M·L·T⁻² and ratio scale. The standard distinguishes them only in prose: a weight acts in a gravitational field; a static friction force resists motion before a body slides; a kinetic friction force resists motion while it slides. A dimension-only or representation-only model cannot capture the difference; it sees one type, "a real number of newtons", for all of them.

This is requirement R2 again, now on the force family — the exact pattern Part 3 set on the length family. Item 4-9.1, force, is the broad genus; each later item is specified as a species of force, distinguished not by fiat but by an explicit measurement principle (Dybkær's examination principle, §7.5). The species are then provably distinct kinds while remaining mutually comparable as forces.

Definition22.2.1
Group: The force species are individuated by an examination principle and arranged as a specialization lattice over the general force kind. The sharpest case is static versus kinetic friction: physically the same dimension and both "friction forces", they are nonetheless different kinds — and the calculus proves it from their differing measurement conditions, not from a naming convention. (2)
Group member previews
Preview
Theorem 22.2.2
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 6.4.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N

A force species is a ratio-scale quantity-kind of dimension M·L·T⁻² carrying an examination principle — this work's own terse descriptor of the measurement principle that distinguishes it (gravitational-field action, pre-slip resistance, sliding resistance, …), never the standard's normative definition. Weight, the static and kinetic friction forces, the rolling resistance, and the drag force are all species of the general force kind (item 4-9.1).

Lean code for Definition22.2.1●1 definition
  • defdefined in PropertyKindCalculus/Iso80000/Part4.lean
    complete
    def PropertyKindCalculus.Iso80000.Part4.forceSpecies (id : String)
  (p : PropertyKindCalculus.ExaminationPrinciple) :
  PropertyKindCalculus.DimensionedKind LTMCTDimensionBase
    def PropertyKindCalculus.Iso80000.Part4.forceSpecies
  (id : String)
  (p :
    PropertyKindCalculus.ExaminationPrinciple) :
  PropertyKindCalculus.DimensionedKind
    LTMCTDimensionBase
    A force species: dimension `M·L·T⁻²`, ratio-scale, individuated by its measurement
(examination) principle.
Proof for Definition 22.2.1
uses 0

forceSpecies id p := { kind := { id, scale := .ratio, examPrinciple := some p.id }, dim := MDim.force }. The general force carries no examination principle; the direct-parent edges of the family are collected in an Edge relation, each species an edge to force (mirroring the standard's "force (item 4-9.1) … acting/resisting …").

Theorem22.2.2
Group: The force species are individuated by an examination principle and arranged as a specialization lattice over the general force kind. The sharpest case is static versus kinetic friction: physically the same dimension and both "friction forces", they are nonetheless different kinds — and the calculus proves it from their differing measurement conditions, not from a naming convention. (2)
Group member previews
Preview
Definition 22.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N
EffortsmallTagsproved

Static and kinetic friction forces are distinct kinds — by measurement principle, not by fiat. They share dimension M·L·T⁻² and are both "friction forces", yet are different kinds because they are examined under different conditions (resistance before sliding vs during sliding), proved through distinct_of_examPrinciple (§7.5). This is the force-family analogue of width ≠ distance. Uses the examination principle.

Lean code for Theorem22.2.2●1 theorem
  • theoremdefined in PropertyKindCalculus/Iso80000/Part4.lean
    complete
    theorem PropertyKindCalculus.Iso80000.Part4.staticFriction_ne_kineticFriction :
  PropertyKindCalculus.Iso80000.Part4.staticFrictionForce.kind
      LTMCTDimensionBase ≠
    PropertyKindCalculus.Iso80000.Part4.kineticFrictionForce.kind
      LTMCTDimensionBase
    theorem PropertyKindCalculus.Iso80000.Part4.staticFriction_ne_kineticFriction :
  PropertyKindCalculus.Iso80000.Part4.staticFrictionForce.kind
      LTMCTDimensionBase ≠
    PropertyKindCalculus.Iso80000.Part4.kineticFrictionForce.kind
      LTMCTDimensionBase
    **Static and kinetic friction forces are distinct kinds — by measurement
principle, not by fiat.** They have the same dimension `M·L·T⁻²` and are both
"friction forces", yet they are different kinds *because they are examined under
different conditions* (resistance before sliding vs during sliding), proved through
`distinct_of_examPrinciple` (§7.5) rather than by appealing to their `id` strings.
This is the force-family analogue of width ≠ distance.
Proof for Theorem 22.2.2
uses 0

staticFriction_ne_kineticFriction : staticFrictionForce.kind ≠ kineticFrictionForce.kind, from KindOfProperty.distinct_of_examPrinciple applied to the differing principles pre-slip-resistance and sliding-resistance (a decide on the Option String links). The companions weight_ne_dragForce and weight_ne_force separate the other species, and weight_examinedBy checks the kind-to-principle link. Axiom-free.

Theorem22.2.3
Group: The force species are individuated by an examination principle and arranged as a specialization lattice over the general force kind. The sharpest case is static versus kinetic friction: physically the same dimension and both "friction forces", they are nonetheless different kinds — and the calculus proves it from their differing measurement conditions, not from a naming convention. (2)
Group member previews
Preview
Definition 22.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N
EffortsmallTagsproved

Comparability is preserved. Weight and the drag force, though distinct kinds, remain mutually comparable — they share the super-kind force, so combining them is possible but only via an explicit up-cast, never silently. The companion weight_specializes_force records that a weight specializes force. Uses specialization.

Lean code for Theorem22.2.3●1 theorem
  • theoremdefined in PropertyKindCalculus/Iso80000/Part4.lean
    complete
    theorem PropertyKindCalculus.Iso80000.Part4.weight_dragForce_comparable :
  PropertyKindCalculus.MutuallyComparable
    PropertyKindCalculus.Iso80000.Part4.Edge
    (PropertyKindCalculus.Iso80000.Part4.weight.kind LTMCTDimensionBase)
    (PropertyKindCalculus.Iso80000.Part4.dragForce.kind
      LTMCTDimensionBase)
    theorem PropertyKindCalculus.Iso80000.Part4.weight_dragForce_comparable :
  PropertyKindCalculus.MutuallyComparable
    PropertyKindCalculus.Iso80000.Part4.Edge
    (PropertyKindCalculus.Iso80000.Part4.weight.kind
      LTMCTDimensionBase)
    (PropertyKindCalculus.Iso80000.Part4.dragForce.kind
      LTMCTDimensionBase)
    **Mutual comparability is preserved.** Weight and the drag force, though distinct
kinds, remain *mutually comparable* — they share the super-kind force, so combining
them is possible but only via an explicit up-cast, never silently.
Proof for Theorem 22.2.3
uses 0

weight_dragForce_comparable : MutuallyComparable Edge weight.kind dragForce.kind, with witness force.kind, each species reaching it by one edge. Axiom-free.