27.2. The mole reduces to dimension one — R13 at its sharpest🔗

ISO 80000-9 is built on the mole. In the scale-spanning reading (R13), the mole is not a base dimension but a human-selected dimensionless count: N_A entities. So amount of substance is dimension one, and the /mol in every molar quantity is invisible to the dimension functor. Molar mass (kg/mol) carries the dimension of mass; molar volume (m³/mol) the dimension of volume; the amount-of-substance concentration (mol/m³) the dimension of a number density L⁻³ — the very same dimension as a particle concentration; molality (mol/kg) the dimension of an inverse mass.

And amount of substance itself joins the dimensionless family, distinct in kind from the number of entities it counts (N = n·N_A) — both dimension one, two kinds. This is requirement R13 in the place that makes it unavoidable: a mol is no more a base unit than a cd (ISO 80000-7) or a Sh (IEC 80000-13).

Theorem27.2.1

group

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

EffortsmallTagscapstoneproved

Molar mass is a mass — the mole reduces (item 9-4). With the mole dimension one, kg/mol carries the dimension of mass, M. The companion facts record the rest of the reduction: the amount-of-substance concentration is a number density (equal to the particle concentration), molality is an inverse mass, and amount of substance is itself dimension one. This is the scale-spanning reduction (R13) at the place the mole lives. Uses the dimension map and the scale-spanning units.

Lean code for Theorem27.2.1●1 theorem

theoremdefined in PropertyKindCalculus/Iso80000/Part9.lean

complete

theorem PropertyKindCalculus.Iso80000.Part9.molarMass_dim_eq_mass :
  PropertyKindCalculus.Iso80000.Part9.molarMass.dim LTMCTDimensionBase =
    PropertyKindCalculus.Dim.mass

theorem PropertyKindCalculus.Iso80000.Part9.molarMass_dim_eq_mass :
  PropertyKindCalculus.Iso80000.Part9.molarMass.dim
      LTMCTDimensionBase =
    PropertyKindCalculus.Dim.mass

**Molar mass is a mass.** With the mole dimension one, `kg/mol` carries the dimension
of mass, `M` (item 9-4).

Proof for Theorem 27.2.1

uses 0

molarMass_dim_eq_mass : molarMass.dim = Dim.mass, by reflexivity (the kind is declared at Dim.mass). The companions amountOfSubstance_dim_eq_one, amountConcentration_dim_eq_particleConcentration, and molality_dim_eq_inverseMass record the rest; the defining-relation versions (molarMass_dim_from_mass_amount, amountConcentration_dim_from_amount_volume) derive the reduction from M = m/n and c = n/V with dim n = 1. Axiom-free.

Theorem27.2.2

groupuses 1used by 0✓L∃∀N

EffortsmallTagsproved

The dimension-1 disambiguation, on the standard — with the mole inside it. There exist distinct ISO 80000-9 kinds with the same dimension one — amount of substance (the mole, reduced by R13) and the number of entities witness it, alongside the fractions, the activities, and the partition functions. Dimension cannot separate them; the kind layer does. Uses the dimension map.

Lean code for Theorem27.2.2●1 theorem

theoremdefined in PropertyKindCalculus/Iso80000/Part9.lean

complete

theorem PropertyKindCalculus.Iso80000.Part9.iso80000_9_dim_one_collision :
  ∃ a b,
    a.kind LTMCTDimensionBase ≠ b.kind LTMCTDimensionBase ∧
      a.dim LTMCTDimensionBase = b.dim LTMCTDimensionBase ∧
        a.dim LTMCTDimensionBase = 1

theorem PropertyKindCalculus.Iso80000.Part9.iso80000_9_dim_one_collision :
  ∃ a b,
    a.kind LTMCTDimensionBase ≠
        b.kind LTMCTDimensionBase ∧
      a.dim LTMCTDimensionBase =
          b.dim LTMCTDimensionBase ∧
        a.dim LTMCTDimensionBase = 1

**The dimension-one disambiguation, on the standard — with the mole inside it.** There
exist distinct ISO 80000-9 kinds with the same dimension one — amount of substance (the
mole, reduced by R13) and the number of entities witness it, alongside the fractions, the
activities, and the partition functions. Dimension cannot separate them; the kind layer
does.

Proof for Theorem 27.2.2

uses 0

iso80000_9_dim_one_collision, witnessed by ⟨amountOfSubstance, numberOfEntities, …⟩ with the kind distinction a decide and reflexivity. Axiom-free.