27.3. The seven-fold `J/mol` collision🔗

The mole reducing to dimension one, the seven energies-per-mole — molar internal energy, molar enthalpy, molar Helmholtz and Gibbs energies (9-6.1 … 9-6.4), the chemical potential (9-17), the standard chemical potential (9-21), and the affinity of a reaction (9-30) — all carry the same dimension M·L²·T⁻² and the same unit string J/mol, yet are seven distinct kinds. A dimension-only model sees one type, "a real number of joules per mole", for all seven; the kind layer keeps the chemical potential from being read as an affinity. Likewise the molar heat capacity (9-7), molar entropy (9-8), and molar gas constant (9-37.1) all share J/(mol·K).

Theorem27.3.1

uses 1used by 0✓L∃∀N

EffortsmallTagsproved

Molar internal energy is not molar Gibbs energy, though both are J/mol and M·L²·T⁻² (items 9-6.1, 9-6.4). There exist distinct ISO 80000-9 kinds with the same dimension — seven J/mol quantities witness it. The mole reduces to dimension one, so no dimension-only type system can separate them; the kind layer — and the unit — does. Uses the dimension map.

Lean code for Theorem27.3.1●1 theorem

theoremdefined in PropertyKindCalculus/Iso80000/Part9.lean

complete

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

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

**The `J/mol` collision capstone, on the standard.** There exist distinct ISO 80000-9
kinds with the same dimension `M·L²·T⁻²` — molar internal energy and molar Gibbs energy
witness it, alongside the molar enthalpy and Helmholtz energy, the chemical potential, the
standard chemical potential, and the affinity (all `J/mol`). The mole reduces to dimension
one, so the {dimension functor} cannot separate them; the kind layer does.

Proof for Theorem 27.3.1

uses 0

iso80000_9_dim_collision, witnessed by ⟨molarInternalEnergy, molarGibbsEnergy, …⟩. The unit fact jPerMol_internalEnergy_gibbs_not_commensurable is a decide; molarHeatCapacity_dim_eq_molarEntropy_dim records the parallel J/(mol·K) collision, and molPerKg_molality_ionicStrength_not_commensurable the mol/kg one. Axiom-free.

27.3. The seven-fold J/mol collision🔗

27.3. The seven-fold `J/mol` collision🔗