A Property Kind Calculus for Measurement Metrology

12.1. A criterion the dimension layer can apply — and one place it cannot🔗

Definition12.1.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.2
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0
Used by 3
Reverse dependency previews
Preview
Theorem 12.2.1
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

A dimension is mechanically reducible when it is expressible in mass, length, and time alone — it carries no charge and no temperature exponent. This is the Finkelstein–Whitehead test for "not dimensionally independent of the four physical base units", specialized to the mechanical generators: such a unit needs no electromagnetic, thermal, luminous, or chemical base of its own.

Lean code for Definition12.1.1●1 definition
  • defdefined in PropertyKindCalculus/ScaleSpanning.lean
    complete
    def PropertyKindCalculus.Dimension.MechanicallyReducible
  (d : Dimension LTMCTDimensionBase) : Prop
    def PropertyKindCalculus.Dimension.MechanicallyReducible
  (d : Dimension LTMCTDimensionBase) :
  Prop
    A dimension is **mechanically reducible** iff it is expressible in mass, length,
and time alone — i.e. it carries no charge and no temperature exponent. This is the
Finkelstein–Whitehead criterion for "*not* dimensionally independent of the four
physical base units `{kg, m, s, A}`" specialized to the mechanical generators: a unit
whose dimension is mechanically reducible needs neither an electromagnetic, a
thermal, a luminous, nor a chemical base of its own.
Proof for Definition 12.1.1
uses 0

Dimension.MechanicallyReducible d := d.charge = 0 ∧ d.temperature = 0. Power and energy are reducible (power_mechanicallyReducible, energy_mechanicallyReducible), as is dimension one; electric current is not (current_not_mechanicallyReducible — it carries the electromagnetic generator), and neither is thermodynamic temperature in this work's algebra (temperature_not_mechanicallyReducible).

Definition12.1.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.
uses 1used by 1✓L∃∀N

The proposed three-way classification of SI units: physical base (the four dimensionally independent units kg, m, s, A), scale-spanning (the kelvin, candela, and mole), and derived (every plain product of powers, with no special coefficient). The scale-spanning units are the new middle category the two-way base/derived split omits.

Lean code for Definition12.1.2●1 definition
  • inductive(3 constructors)defined in PropertyKindCalculus/ScaleSpanning.lean
    complete
    inductive PropertyKindCalculus.UnitCategory : Type
    inductive PropertyKindCalculus.UnitCategory : Type
    The proposed three-way classification of SI units. The base/derived dichotomy is
*insufficient*; a third category is needed.

    Constructors

    PropertyKindCalculus.UnitCategory.physicalBase :
  PropertyKindCalculus.UnitCategory
    The four dimensionally independent physical base units `{kg, m, s, A}`, each
fixed by a natural constant (`h`, `c`, `Δν_Cs`, `e`). 
    PropertyKindCalculus.UnitCategory.scaleSpanning :
  PropertyKindCalculus.UnitCategory
    The kelvin, candela, and mole: *not* dimensionally independent, yet retained as
distinct coherent units because each carries a human-selected coefficient that lets
it span vast scales. 
    PropertyKindCalculus.UnitCategory.derived :
  PropertyKindCalculus.UnitCategory
    Every other unit (the newton, joule, watt, volt, ohm, …): a plain product of
powers of the base units, with no special defining coefficient.
Proof for Definition 12.1.2
uses 0

inductive UnitCategory | physicalBase | scaleSpanning | derived. Realized as a plain enumeration; a scale-spanning unit's category is scaleSpanning by construction.

Definition12.1.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 1
Used by 4
Reverse dependency previews
Preview
Definition 12.1.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

A scale-spanning unit pairs a metrological unit with its mechanical-dimension reduction and the human-selected coefficient that defines it. The worked set is the candela (reducing to power, via K_cd = 683 lm/W), the mole (to dimension one, via N_A), and the kelvin (to energy, via k_B). The coefficient and its value are citation locators — the published constants — not reproduced normative text.

Lean code for Definition12.1.3●1 definition
  • structure(4 fields)defined in PropertyKindCalculus/ScaleSpanning.lean
    complete
    structure PropertyKindCalculus.ScaleSpanningUnit : Type
    structure PropertyKindCalculus.ScaleSpanningUnit :
  Type
    A **scale-spanning unit**: a metrological unit that is dimensionally dependent on
the physical base, yet retained for its scale-spanning role, defined through a
human-selected coefficient.

    Fields

    unit : PropertyKindCalculus.MetrologicalUnit
    The metrological unit (e.g. the candela of luminous intensity). 
    reducesTo : Dimension LTMCTDimensionBase
    The mechanical dimension the unit reduces to (power, energy, one). 
    coefficient : String
    The human-selected defining coefficient (e.g. `K_cd`, `k_B`, `N_A`). 
    coefficientValue : String
    The coefficient's published value, a citation locator (e.g. `683 lm/W`).
Proof for Definition 12.1.3
uses 0

structure ScaleSpanningUnit carries the unit, the reducesTo dimension, and the coefficient symbol and value. The three canonical instances candela, mole, kelvin are declared in the ScaleSpanning namespace (so their names do not collide with the standards parts that also declare them).