A Property Kind Calculus for Measurement Metrology

29.2. The sub-suffixed homonyms — same name, distinct kind🔗

ISO 80000-11 reuses one name across its transport-phenomena clauses, distinguishing the variants only by a symbol suffix and a different defining ratio. The Froude number appears as 11-4.3 (Fr, momentum) and 11-5.4 (Fr*, heat); the Fourier, Péclet, Grashof, Nusselt, Stanton, Graetz and Biot numbers each as a heat (Fo, …) and a mass (Fo*, …) member; the Bejan number four times; and the Stokes number five times (Stk, Stk₁ … Stk₄). These are the sub-suffixed quantity kinds — and they are the sharpest form of R2 in the whole series: a member shares its name and its dimension (one) with its siblings, so neither the name nor the dimension can tell them apart. Only the measurement principle can.

Theorem29.2.1
Group: The homonym families are individuated by the examination principle alone — distinct_of_examPrinciple , not the id strings, which are equal. Every characteristic number has the same coherent unit symbol 1 , so the unit cannot tell them apart either; yet two are not commensurable, because they reference different kinds. (3)
Group member previews
Preview
Theorem 29.2.2
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N
EffortsmallTagsproved

The two Froude numbers are distinct kinds — by measurement principle, not by name. Both are named "Froude number" and both are dimension one (11-4.3, Fr, momentum transfer; 11-5.4, Fr*, heat transfer), yet they isolate different physical ratios — inertial/gravitational versus gravitational/thermodiffusion forces — so the calculus proves them distinct from their differing principles. The Fourier (11-5.1, 11-6.1) and Nusselt (11-5.5, 11-6.4) numbers recur likewise. Uses the examination principle.

Lean code for Theorem29.2.1●1 theorem
  • theoremdefined in PropertyKindCalculus/Iso80000/Part11.lean
    complete
    theorem PropertyKindCalculus.Iso80000.Part11.froudeMomentum_ne_froudeHeat :
  PropertyKindCalculus.Iso80000.Part11.froudeMomentum.kind
      LTMCTDimensionBase ≠
    PropertyKindCalculus.Iso80000.Part11.froudeHeat.kind
      LTMCTDimensionBase
    theorem PropertyKindCalculus.Iso80000.Part11.froudeMomentum_ne_froudeHeat :
  PropertyKindCalculus.Iso80000.Part11.froudeMomentum.kind
      LTMCTDimensionBase ≠
    PropertyKindCalculus.Iso80000.Part11.froudeHeat.kind
      LTMCTDimensionBase
    **The two Froude numbers are distinct kinds.** Both are named "Froude number" and both
are dimension one (11-4.3, `Fr`, momentum transfer; 11-5.4, `Fr*`, heat transfer), yet
they isolate different physical ratios — inertial/gravitational versus
gravitational/thermodiffusion forces.
Proof for Theorem 29.2.1
uses 0

froudeMomentum_ne_froudeHeat : froudeMomentum.kind ≠ froudeHeat.kind, from KindOfProperty.distinct_of_examPrinciple on the differing principles momentum-transfer: … and heat-transfer: …; froudeMomentum_id_eq_froudeHeat checks the names are equal. The companions fourierHeat_ne_fourierMass and nusseltHeat_ne_nusseltMass cover the other recurring pairs. Axiom-free.

Theorem29.2.2
Group: The homonym families are individuated by the examination principle alone — distinct_of_examPrinciple , not the id strings, which are equal. Every characteristic number has the same coherent unit symbol 1 , so the unit cannot tell them apart either; yet two are not commensurable, because they reference different kinds. (3)
Group member previews
Preview
Theorem 29.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N
EffortsmallTagsproved

The five Stokes numbers are pairwise distinct kinds. All five (11-4.32 … 11-4.36) carry the name "Stokes number" and dimension one, distinguished only by symbol suffix (Stk, Stk₁ … Stk₄) and the measurement principle each isolates — friction/inertia for particles in flow, for vibrating particles, rotameter calibration, viscous/gravity for settling particles, drag/internal-friction. Uses the examination principle.

Lean code for Theorem29.2.2●1 theorem
  • theoremdefined in PropertyKindCalculus/Iso80000/Part11.lean
    complete
    theorem PropertyKindCalculus.Iso80000.Part11.stokes_pairwise_distinct :
  PropertyKindCalculus.Iso80000.Part11.stokesPlasma.kind
        LTMCTDimensionBase ≠
      PropertyKindCalculus.Iso80000.Part11.stokesVibrating.kind
        LTMCTDimensionBase ∧
    PropertyKindCalculus.Iso80000.Part11.stokesVibrating.kind
          LTMCTDimensionBase ≠
        PropertyKindCalculus.Iso80000.Part11.stokesRotameter.kind
          LTMCTDimensionBase ∧
      PropertyKindCalculus.Iso80000.Part11.stokesRotameter.kind
            LTMCTDimensionBase ≠
          PropertyKindCalculus.Iso80000.Part11.stokesGravity.kind
            LTMCTDimensionBase ∧
        PropertyKindCalculus.Iso80000.Part11.stokesGravity.kind
              LTMCTDimensionBase ≠
            PropertyKindCalculus.Iso80000.Part11.stokesDrag.kind
              LTMCTDimensionBase ∧
          PropertyKindCalculus.Iso80000.Part11.stokesPlasma.kind
              LTMCTDimensionBase ≠
            PropertyKindCalculus.Iso80000.Part11.stokesDrag.kind
              LTMCTDimensionBase
    theorem PropertyKindCalculus.Iso80000.Part11.stokes_pairwise_distinct :
  PropertyKindCalculus.Iso80000.Part11.stokesPlasma.kind
        LTMCTDimensionBase ≠
      PropertyKindCalculus.Iso80000.Part11.stokesVibrating.kind
        LTMCTDimensionBase ∧
    PropertyKindCalculus.Iso80000.Part11.stokesVibrating.kind
          LTMCTDimensionBase ≠
        PropertyKindCalculus.Iso80000.Part11.stokesRotameter.kind
          LTMCTDimensionBase ∧
      PropertyKindCalculus.Iso80000.Part11.stokesRotameter.kind
            LTMCTDimensionBase ≠
          PropertyKindCalculus.Iso80000.Part11.stokesGravity.kind
            LTMCTDimensionBase ∧
        PropertyKindCalculus.Iso80000.Part11.stokesGravity.kind
              LTMCTDimensionBase ≠
            PropertyKindCalculus.Iso80000.Part11.stokesDrag.kind
              LTMCTDimensionBase ∧
          PropertyKindCalculus.Iso80000.Part11.stokesPlasma.kind
              LTMCTDimensionBase ≠
            PropertyKindCalculus.Iso80000.Part11.stokesDrag.kind
              LTMCTDimensionBase
    **The five Stokes numbers are pairwise distinct kinds.** All five (11-4.32 … 11-4.36)
carry the name "Stokes number" and dimension one, distinguished only by symbol suffix
(`Stk`, `Stk₁` … `Stk₄`) and the measurement principle each isolates.
Proof for Theorem 29.2.2
uses 0

stokes_pairwise_distinct, a conjunction of five distinct_of_examPrinciple applications on the differing principles. Axiom-free.

Theorem29.2.3
Group: The homonym families are individuated by the examination principle alone — distinct_of_examPrinciple , not the id strings, which are equal. Every characteristic number has the same coherent unit symbol 1 , so the unit cannot tell them apart either; yet two are not commensurable, because they reference different kinds. (3)
Group member previews
Preview
Theorem 29.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N
EffortsmallTagsproved

The four Bejan numbers are distinct kinds — even two sharing a transport context. The momentum (11-4.15), the two heat (11-5.9, 11-5.10) and the mass (11-6.16) Bejan numbers are four kinds. The two heat-transfer ones share name and context, and differ only in the measurement principle (mechanical-work/diffusion-losses versus heat-transfer efficiency by entropy generation) — the finest distinction the calculus draws in this part. Uses the examination principle.

Lean code for Theorem29.2.3●1 theorem
  • theoremdefined in PropertyKindCalculus/Iso80000/Part11.lean
    complete
    theorem PropertyKindCalculus.Iso80000.Part11.bejan_four_distinct :
  PropertyKindCalculus.Iso80000.Part11.bejanMomentum.kind
        LTMCTDimensionBase ≠
      PropertyKindCalculus.Iso80000.Part11.bejanHeat.kind
        LTMCTDimensionBase ∧
    PropertyKindCalculus.Iso80000.Part11.bejanHeat.kind
          LTMCTDimensionBase ≠
        PropertyKindCalculus.Iso80000.Part11.bejanEntropy.kind
          LTMCTDimensionBase ∧
      PropertyKindCalculus.Iso80000.Part11.bejanEntropy.kind
            LTMCTDimensionBase ≠
          PropertyKindCalculus.Iso80000.Part11.bejanMass.kind
            LTMCTDimensionBase ∧
        PropertyKindCalculus.Iso80000.Part11.bejanMomentum.kind
            LTMCTDimensionBase ≠
          PropertyKindCalculus.Iso80000.Part11.bejanMass.kind
            LTMCTDimensionBase
    theorem PropertyKindCalculus.Iso80000.Part11.bejan_four_distinct :
  PropertyKindCalculus.Iso80000.Part11.bejanMomentum.kind
        LTMCTDimensionBase ≠
      PropertyKindCalculus.Iso80000.Part11.bejanHeat.kind
        LTMCTDimensionBase ∧
    PropertyKindCalculus.Iso80000.Part11.bejanHeat.kind
          LTMCTDimensionBase ≠
        PropertyKindCalculus.Iso80000.Part11.bejanEntropy.kind
          LTMCTDimensionBase ∧
      PropertyKindCalculus.Iso80000.Part11.bejanEntropy.kind
            LTMCTDimensionBase ≠
          PropertyKindCalculus.Iso80000.Part11.bejanMass.kind
            LTMCTDimensionBase ∧
        PropertyKindCalculus.Iso80000.Part11.bejanMomentum.kind
            LTMCTDimensionBase ≠
          PropertyKindCalculus.Iso80000.Part11.bejanMass.kind
            LTMCTDimensionBase
    **The four Bejan numbers are distinct kinds.** The momentum (11-4.15), the two heat
(11-5.9, 11-5.10) and the mass (11-6.16) Bejan numbers are four kinds — even the two heat
ones, sharing name *and* transport context, differ by their measurement principle.
Proof for Theorem 29.2.3
uses 0

bejan_four_distinct, a conjunction of four distinct_of_examPrinciple applications. Axiom-free.

Theorem29.2.4
Group: The homonym families are individuated by the examination principle alone — distinct_of_examPrinciple , not the id strings, which are equal. Every characteristic number has the same coherent unit symbol 1 , so the unit cannot tell them apart either; yet two are not commensurable, because they reference different kinds. (3)
Group member previews
Preview
Theorem 29.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N
EffortsmallTagsproved

One unit symbol, many kinds. The Reynolds and Euler units are not commensurable, though both carry the coherent unit symbol 1 and dimension one. Same symbol, same dimension, different kind — so a value of one cannot be read as a value of the other. The kind layer keeps them apart where the unit symbol and the dimension cannot. Uses the metrological unit.

Lean code for Theorem29.2.4●1 theorem
  • theoremdefined in PropertyKindCalculus/Iso80000/Part11.lean
    complete
    theorem PropertyKindCalculus.Iso80000.Part11.reynolds_euler_not_commensurable :
  ¬PropertyKindCalculus.Iso80000.Part11.reynoldsUnit.Commensurable
      PropertyKindCalculus.Iso80000.Part11.eulerUnit
    theorem PropertyKindCalculus.Iso80000.Part11.reynolds_euler_not_commensurable :
  ¬PropertyKindCalculus.Iso80000.Part11.reynoldsUnit.Commensurable
      PropertyKindCalculus.Iso80000.Part11.eulerUnit
    **The Reynolds and Euler units are not commensurable, though both have unit symbol
`"1"`.** Same symbol, same dimension (one), different kind — so a value of one cannot be
read as a value of the other. The kind layer keeps them apart where the unit symbol and
the dimension cannot.
Proof for Theorem 29.2.4
uses 0

reynolds_euler_not_commensurable : ¬ reynoldsUnit.Commensurable eulerUnit, by unfolding Commensurable (equality of the referenced kinds) and decide; reynoldsUnit_wellFormed checks the unit is well-formed (a ratio-scale kind bears a unit). Axiom-free.