A Property Kind Calculus for Measurement Metrology

12.2. The requirement, proved🔗

Theorem12.2.1
Group: The dimension layer can detect some scale-spanning units: a unit whose dimension is mechanically reducible — expressible in mass, length, and time alone — is by that fact not dimensionally independent. The candela (power) and the mole (one) are reducible this way. The kelvin is the sharp case: this work keeps thermodynamic temperature Θ as an independent dimension (the Thermodynamics chapter needs it), so the dimension layer sees the kelvin as if it were a base — its scale-spanning character is visible only once one adopts k_B as a defining coefficient, which the dimension layer does not. So scale-spanning is carried, like a kind's identity , above the dimension. (6)
Group member previews
Preview
Definition 12.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N
EffortsmallTagsproved

The candela reduces to power — the dimension layer can see it. Luminous intensity carries the dimension of power, which is mechanically reducible; so the dimension layer correctly detects that the candela is not dimensionally independent. The mole is likewise reducible (to dimension one). Uses mechanical reducibility.

Lean code for Theorem12.2.1●1 theorem
  • theoremdefined in PropertyKindCalculus/ScaleSpanning.lean
    complete
    theorem PropertyKindCalculus.ScaleSpanning.candela_reduction_reducible :
  PropertyKindCalculus.Dimension.MechanicallyReducible
    PropertyKindCalculus.ScaleSpanning.candela.reducesTo
    theorem PropertyKindCalculus.ScaleSpanning.candela_reduction_reducible :
  PropertyKindCalculus.Dimension.MechanicallyReducible
    PropertyKindCalculus.ScaleSpanning.candela.reducesTo
    The candela's reduction is mechanically reducible — the dimension layer *can*
detect that luminous intensity is dimensionally dependent on the physical base.
Proof for Theorem 12.2.1
uses 0

candela_reduction_reducible : Dimension.MechanicallyReducible candela.reducesTo, from power_mechanicallyReducible (power.charge = 0, power.temperature = 0, checked in the PhysLib dimension group). The companion mole_reduction_reducible covers dimension one. Axiom-free.

Theorem12.2.2
Group: The dimension layer can detect some scale-spanning units: a unit whose dimension is mechanically reducible — expressible in mass, length, and time alone — is by that fact not dimensionally independent. The candela (power) and the mole (one) are reducible this way. The kelvin is the sharp case: this work keeps thermodynamic temperature Θ as an independent dimension (the Thermodynamics chapter needs it), so the dimension layer sees the kelvin as if it were a base — its scale-spanning character is visible only once one adopts k_B as a defining coefficient, which the dimension layer does not. So scale-spanning is carried, like a kind's identity , above the dimension. (6)
Group member previews
Preview
Definition 12.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 11.1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
EffortsmallTagsproved

The kelvin's scale-spanning character is invisible to the dimension layer. Its proposed reduction (energy, via k_B) is mechanically reducible, yet the dimension this work assigns thermodynamic temperature (Θ) is not — so no dimensional analysis reveals the kelvin to be scale-spanning. The fact is carried at the unit-classification layer, through the coefficient k_B, exactly as a kind carries more than its dimension. Uses mechanical reducibility.

Lean code for Theorem12.2.2●1 theorem
  • theoremdefined in PropertyKindCalculus/ScaleSpanning.lean
    complete
    theorem PropertyKindCalculus.ScaleSpanning.kelvin_reduction_invisible_to_dimension :
  PropertyKindCalculus.Dimension.MechanicallyReducible
      PropertyKindCalculus.ScaleSpanning.kelvin.reducesTo ∧
    ¬PropertyKindCalculus.Dimension.MechanicallyReducible
        PropertyKindCalculus.Dim.temperature
    theorem PropertyKindCalculus.ScaleSpanning.kelvin_reduction_invisible_to_dimension :
  PropertyKindCalculus.Dimension.MechanicallyReducible
      PropertyKindCalculus.ScaleSpanning.kelvin.reducesTo ∧
    ¬PropertyKindCalculus.Dimension.MechanicallyReducible
        PropertyKindCalculus.Dim.temperature
    **The kelvin's scale-spanning character is invisible to the dimension layer.**
Its *proposed* reduction (energy, via `k_B`) is mechanically reducible, yet the
dimension this library actually assigns thermodynamic temperature (`Θ`) is *not* — so
no amount of dimensional analysis reveals the kelvin to be scale-spanning. The fact is
carried at the unit-classification layer, through the coefficient `k_B`, not at the
dimension layer.
Proof for Theorem 12.2.2
uses 0

kelvin_reduction_invisible_to_dimension : Dimension.MechanicallyReducible kelvin.reducesTo ∧ ¬ Dimension.MechanicallyReducible Dim.temperature, the first conjunct from energy_mechanicallyReducible, the second from temperature_not_mechanicallyReducible (Dim.temperature.temperature = 1 ≠ 0). Axiom-free.

Theorem12.2.3
Group: The dimension layer can detect some scale-spanning units: a unit whose dimension is mechanically reducible — expressible in mass, length, and time alone — is by that fact not dimensionally independent. The candela (power) and the mole (one) are reducible this way. The kelvin is the sharp case: this work keeps thermodynamic temperature Θ as an independent dimension (the Thermodynamics chapter needs it), so the dimension layer sees the kelvin as if it were a base — its scale-spanning character is visible only once one adopts k_B as a defining coefficient, which the dimension layer does not. So scale-spanning is carried, like a kind's identity , above the dimension. (6)
Group member previews
Preview
Definition 12.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N
EffortsmallTagsproved

The ampere is a genuine physical base — not scale-spanning. Electric current is not mechanically reducible: it carries the electromagnetic generator, so it is dimensionally independent. This is the contrast that makes the third category non-empty and distinct from the first — the ampere (IEC 80000-6) belongs to the base set, the candela (ISO 80000-7) does not. Uses mechanical reducibility.

Lean code for Theorem12.2.3●1 theorem
  • theoremdefined in PropertyKindCalculus/ScaleSpanning.lean
    complete
    theorem PropertyKindCalculus.ScaleSpanning.ampere_is_physicalBase :
  ¬PropertyKindCalculus.Dimension.MechanicallyReducible
      PropertyKindCalculus.Dim.current
    theorem PropertyKindCalculus.ScaleSpanning.ampere_is_physicalBase :
  ¬PropertyKindCalculus.Dimension.MechanicallyReducible
      PropertyKindCalculus.Dim.current
    **The ampere is genuinely a physical base — not scale-spanning.** Electric current
is not mechanically reducible: it carries the electromagnetic generator. This is the
contrast that makes the third category non-empty *and* distinct from the first.
Proof for Theorem 12.2.3
uses 0

ampere_is_physicalBase : ¬ Dimension.MechanicallyReducible Dim.current, from Dim.current_charge = 1 ≠ 0. Axiom-free.

Theorem12.2.4
Group: The dimension layer can detect some scale-spanning units: a unit whose dimension is mechanically reducible — expressible in mass, length, and time alone — is by that fact not dimensionally independent. The candela (power) and the mole (one) are reducible this way. The kelvin is the sharp case: this work keeps thermodynamic temperature Θ as an independent dimension (the Thermodynamics chapter needs it), so the dimension layer sees the kelvin as if it were a base — its scale-spanning character is visible only once one adopts k_B as a defining coefficient, which the dimension layer does not. So scale-spanning is carried, like a kind's identity , above the dimension. (6)
Group member previews
Preview
Definition 12.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 12.1.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
EffortsmallPriorityhighTagscapstoneproved

R13 — the base/derived dichotomy is insufficient; scale-spanning is a third category, not a function of dimension. Two scale-spanning units disagree on mechanical reducibility — the candela's dimension (reducible) and the kelvin's actual dimension Θ (not reducible) — so membership in the third category cannot be decided from the dimension. The classification is a genuine extra datum, the unit-layer analogue of R1. Uses the unit categories and the scale-spanning units.

Lean code for Theorem12.2.4●1 theorem
  • theoremdefined in PropertyKindCalculus/ScaleSpanning.lean
    complete
    theorem PropertyKindCalculus.ScaleSpanning.scaleSpanning_not_determined_by_dimension :
  ∃ a b,
    PropertyKindCalculus.Dimension.MechanicallyReducible a.reducesTo ∧
      ¬PropertyKindCalculus.Dimension.MechanicallyReducible
            PropertyKindCalculus.Dim.temperature ∧
        b.unit = PropertyKindCalculus.ScaleSpanning.kelvin.unit
    theorem PropertyKindCalculus.ScaleSpanning.scaleSpanning_not_determined_by_dimension :
  ∃ a b,
    PropertyKindCalculus.Dimension.MechanicallyReducible
        a.reducesTo ∧
      ¬PropertyKindCalculus.Dimension.MechanicallyReducible
            PropertyKindCalculus.Dim.temperature ∧
        b.unit =
          PropertyKindCalculus.ScaleSpanning.kelvin.unit
    **R13 — the base/derived dichotomy is insufficient: scale-spanning is a third
category, not a function of dimension.** There exist two scale-spanning units whose
dimensions disagree on mechanical reducibility — the candela's (reducible) and the
kelvin's actual dimension `Θ` (not reducible) — so one cannot decide scale-spanning
membership from the dimension. The classification is a genuine extra datum, the
unit-layer analogue of R1 (a kind is more than its dimension).
Proof for Theorem 12.2.4
uses 0

scaleSpanning_not_determined_by_dimension : ∃ a b : ScaleSpanningUnit, Dimension.MechanicallyReducible a.reducesTo ∧ ¬ Dimension.MechanicallyReducible Dim.temperature ∧ b.unit = kelvin.unit, witnessed by ⟨candela, kelvin, …⟩. Axiom-free. This is the requirement ISO 80000-7's candela and mole, and ISO 80000-5's kelvin, exercise on the standard.