21.2. The length family: distinguishing kinds by measurement principle
ISO 80000-3 lists width (3-1.2), height (3-1.3), thickness (3-1.4), diameter (3-1.5),
radius (3-1.6), path length (3-1.7), distance (3-1.8), and more as separate items —
yet every one of them has dimension L and ratio scale. The standard distinguishes
them only in prose: a width is a transverse extent, a distance is a shortest path,
and so on. A dimension-only or representation-only model cannot capture the
difference at all; it sees one type, "a real number of metres", for all of them.
This is exactly requirement R2, and Part 3 is where it earns its keep on the real standard. Item 3-1.1, length, is the broad genus. Each later item is specified as a species of length, distinguished not by fiat (not merely by a different name) but by an explicit measurement principle — Dybkær's examination principle (§7.5), a genuine defining aspect. The species are then provably distinct kinds, while remaining mutually comparable as lengths; and the specialization edges mirror the standard's own "defined in terms of" links (a diameter is a width of a circle, a radius is half a diameter, a distance is a shortest path length).
A length species is a ratio-scale quantity-kind of dimension
L carrying an examination principle — this work's own terse
descriptor of the measurement principle that distinguishes it (transverse extent,
shortest path, centre-to-rim, …), never the standard's normative definition. Width,
height, thickness, diameter, radius, path length, distance, radial distance, the
position and displacement vectors, the radius of curvature, and the wavelength are all
species of the general length kind (item 3-1.1).
Lean code for Definition21.2.1●1 definition
Associated Lean declarations
-
defdefined in PropertyKindCalculus/Iso80000/Part3.leancomplete
def PropertyKindCalculus.Iso80000.Part3.lengthSpecies (id : String) (p : PropertyKindCalculus.ExaminationPrinciple) : PropertyKindCalculus.DimensionedKind LTMCTDimensionBase
def PropertyKindCalculus.Iso80000.Part3.lengthSpecies (id : String) (p : PropertyKindCalculus.ExaminationPrinciple) : PropertyKindCalculus.DimensionedKind LTMCTDimensionBase
A length species: dimension `L`, ratio-scale, individuated by its measurement (examination) principle.
lengthSpecies id p := { kind := { id, scale := .ratio, examPrinciple := some p.id },
dim := Dim.length }. The general length carries no examination principle; the
direct-parent edges of the family are collected in an Edge relation mirroring the
standard's definitional links (thickness and diameter via width, radius via diameter,
distance via path length, …).
Width and distance are distinct kinds — by measurement principle, not by fiat. A
width (transverse extent) and a distance (shortest path) are different kinds because
they are examined by different principles, proved through distinct_of_examPrinciple
(§7.5) rather than by appealing to their id strings. Same dimension L, same scale,
different kind. Uses the examination principle.
Lean code for Theorem21.2.2●1 theorem
Associated Lean declarations
-
theoremdefined in PropertyKindCalculus/Iso80000/Part3.leancomplete
theorem PropertyKindCalculus.Iso80000.Part3.width_ne_distance : PropertyKindCalculus.Iso80000.Part3.width.kind LTMCTDimensionBase ≠ PropertyKindCalculus.Iso80000.Part3.distance.kind LTMCTDimensionBase
theorem PropertyKindCalculus.Iso80000.Part3.width_ne_distance : PropertyKindCalculus.Iso80000.Part3.width.kind LTMCTDimensionBase ≠ PropertyKindCalculus.Iso80000.Part3.distance.kind LTMCTDimensionBase
**Distinction not by fiat but by measurement principle.** Width and distance are distinct kinds *because they are examined by different principles* (transverse extent vs shortest path), not merely because their `id` strings differ — this is the user-facing point of `distinct_of_examPrinciple` applied to the standard.
width_ne_distance : width.kind ≠ distance.kind, from
KindOfProperty.distinct_of_examPrinciple applied to the differing examination
principles transverse-extent and shortest-path (a decide on the Option String
links). The companion width_examinedBy checks the kind-to-principle link. Axiom-free.
A radius specializes length — transitively. Through the chain radius ⊑ diameter ⊑ width ⊑ length, a radius is a length: specialization is the reflexive-transitive closure of the family's edges, a genuine preorder (a lattice, not just direct edges). Uses specialization.
Lean code for Theorem21.2.3●1 theorem
Associated Lean declarations
-
theoremdefined in PropertyKindCalculus/Iso80000/Part3.leancomplete
theorem PropertyKindCalculus.Iso80000.Part3.radius_specializes_length : PropertyKindCalculus.Specializes PropertyKindCalculus.Iso80000.Part3.Edge (PropertyKindCalculus.Iso80000.Part3.radius.kind LTMCTDimensionBase) (PropertyKindCalculus.Iso80000.Part3.length.kind LTMCTDimensionBase)
theorem PropertyKindCalculus.Iso80000.Part3.radius_specializes_length : PropertyKindCalculus.Specializes PropertyKindCalculus.Iso80000.Part3.Edge (PropertyKindCalculus.Iso80000.Part3.radius.kind LTMCTDimensionBase) (PropertyKindCalculus.Iso80000.Part3.length.kind LTMCTDimensionBase)
A **radius specializes length transitively** (radius ⊑ diameter ⊑ width ⊑ length) — specialization is a preorder, not just the direct edges.
radius_specializes_length, built from Specializes.of_edge on
radius_diameter, diameter_width, width_length composed by Specializes.trans.
Axiom-free.
Comparability is preserved. Width and distance, though distinct kinds, remain mutually comparable — they share the super-kind length, so combining them is possible but only via an explicit up-cast, never silently. Uses specialization.
Lean code for Theorem21.2.4●1 theorem
Associated Lean declarations
-
theoremdefined in PropertyKindCalculus/Iso80000/Part3.leancomplete
theorem PropertyKindCalculus.Iso80000.Part3.width_distance_comparable : PropertyKindCalculus.MutuallyComparable PropertyKindCalculus.Iso80000.Part3.Edge (PropertyKindCalculus.Iso80000.Part3.width.kind LTMCTDimensionBase) (PropertyKindCalculus.Iso80000.Part3.distance.kind LTMCTDimensionBase)
theorem PropertyKindCalculus.Iso80000.Part3.width_distance_comparable : PropertyKindCalculus.MutuallyComparable PropertyKindCalculus.Iso80000.Part3.Edge (PropertyKindCalculus.Iso80000.Part3.width.kind LTMCTDimensionBase) (PropertyKindCalculus.Iso80000.Part3.distance.kind LTMCTDimensionBase)
**Mutual comparability is preserved.** Width and distance, though distinct kinds, remain *mutually comparable* — they share the super-kind length, so combining them is possible but only via an explicit up-cast, never silently.
width_distance_comparable : MutuallyComparable Edge width.kind distance.kind, with
witness length.kind, width reaching it by one edge and distance by two
(distance ⊑ path length ⊑ length). Axiom-free.