23.4. Dimension does not classify; the kind does — the entropy/heat-capacity case🔗

Part 5 holds another textbook dimension collision. Entropy (5-18) and heat capacity (5-15) are both M·L²·T⁻²·Θ⁻¹ — the joule per kelvin — yet they are distinct kinds, and the collision is unusually sharp: their units carry not only the same dimension but the same symbol, "J/K", and are still not commensurable, because their kinds differ. The Massieu (5-22) and Planck (5-23) functions join them at J/K; specific entropy (5-19), specific heat capacity (5-16.1), and the specific gas constant (5-26) collide the same way at J/(kg·K); and the humidity ratios and fractions (5-29 … 5-35), with the ratio of specific heats and the efficiencies, fill out the dimension-one family.

Theorem23.4.1

Group: These are the dimension-disambiguation capstone, on standard quantities: the dimension map identifies the members of each pair, while the kind layer keeps them apart, both as kinds and as units — here even when the units share a symbol. (2)

Group member previews

Preview

Theorem 23.4.2

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 0✓L∃∀N

EffortsmallTagsproved

Entropy is not heat capacity, though both are M·L²·T⁻²·Θ⁻¹. There exist distinct ISO 80000-5 kinds with the same dimension — entropy and heat capacity witness it. No dimension-only type system can separate them; the kind layer does. This is the textbook thermodynamic case that a dimension does not classify a quantity. Uses the dimension map.

Lean code for Theorem23.4.1●1 theorem

theoremdefined in PropertyKindCalculus/Iso80000/Part5.lean

complete

theorem PropertyKindCalculus.Iso80000.Part5.iso80000_5_dim_collision :
  ∃ a b,
    a.kind LTMCTDimensionBase ≠ b.kind LTMCTDimensionBase ∧
      a.dim LTMCTDimensionBase = b.dim LTMCTDimensionBase

theorem PropertyKindCalculus.Iso80000.Part5.iso80000_5_dim_collision :
  ∃ a b,
    a.kind LTMCTDimensionBase ≠
        b.kind LTMCTDimensionBase ∧
      a.dim LTMCTDimensionBase =
        b.dim LTMCTDimensionBase

**The entropy/heat-capacity collision, on standard quantities.** There exist
distinct ISO 80000-5 kinds with the same dimension `M·L²·T⁻²·Θ⁻¹` — entropy and heat
capacity witness it (alongside the Massieu and Planck functions). PhysLib's
`Dimension`, and any dimension-only type system, cannot separate them; the kind layer
does. This is the thermodynamic dimension-does-not-classify case.

Proof for Theorem 23.4.1

uses 0

iso80000_5_dim_collision : ∃ a b : DimensionedKind, a.kind ≠ b.kind ∧ a.dim = b.dim, witnessed by ⟨entropy, heatCapacity, …⟩ with entropy_ne_heatCapacity (a decide) and reflexivity. The companion specificEntropy_ne_specificHeatCapacity is the J/(kg·K) case. Axiom-free.

Theorem23.4.2

Group member previews

Preview

Theorem 23.4.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 0✓L∃∀N

EffortsmallTagsproved

The entropy "J/K" is not the heat-capacity "J/K". The units of entropy and heat capacity carry the same symbol and the same dimension M·L²·T⁻²·Θ⁻¹, yet are not commensurable — the sharpest form of the rule that neither a dimension nor a unit string determines a kind. Uses metrological units.

Lean code for Theorem23.4.2●1 theorem

theoremdefined in PropertyKindCalculus/Iso80000/Part5.lean

complete

theorem PropertyKindCalculus.Iso80000.Part5.entropy_heatCapacity_unit_not_commensurable :
  ¬PropertyKindCalculus.Iso80000.Part5.joulePerKelvinEntropy.Commensurable
      PropertyKindCalculus.Iso80000.Part5.joulePerKelvinHeatCapacity

theorem PropertyKindCalculus.Iso80000.Part5.entropy_heatCapacity_unit_not_commensurable :
  ¬PropertyKindCalculus.Iso80000.Part5.joulePerKelvinEntropy.Commensurable
      PropertyKindCalculus.Iso80000.Part5.joulePerKelvinHeatCapacity

**The entropy joule-per-kelvin is not the heat-capacity joule-per-kelvin, though
both are "J/K" and both `M·L²·T⁻²·Θ⁻¹`.** The units of entropy and heat capacity carry
the same symbol and the same dimension, yet are not commensurable, because their kinds
differ — the sharpest form of "a dimension (or a unit string) does not determine a
kind".

Proof for Theorem 23.4.2

uses 0

entropy_heatCapacity_unit_not_commensurable : ¬ joulePerKelvinEntropy.Commensurable joulePerKelvinHeatCapacity by unfolding to the underlying kinds and decide (entropy's kind differs from the heat-capacity kind, although both units are written "J/K").

Theorem23.4.3

Group member previews

Preview

Theorem 23.4.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 0✓L∃∀N

EffortsmallTagsproved

The dimension-1 disambiguation, on the standard. There exist distinct ISO 80000-5 kinds with the same dimension one — the ratio of specific heat capacities and the efficiency witness it, alongside the isentropic exponent and the humidity ratios and fractions. Dimension cannot separate them; the kind layer does. Uses the dimension map.

Lean code for Theorem23.4.3●1 theorem

theoremdefined in PropertyKindCalculus/Iso80000/Part5.lean

complete

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

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

**The dimension-1 disambiguation, on standard quantities.** There exist distinct
ISO 80000-5 kinds with the same dimension one — the ratio of specific heat capacities
and the efficiency witness it (alongside the isentropic exponent and the humidity
ratios and fractions). Dimension cannot separate them; the kind layer does.

Proof for Theorem 23.4.3

uses 0

iso80000_5_dim_one_collision : ∃ a b : DimensionedKind, a.kind ≠ b.kind ∧ a.dim = b.dim ∧ a.dim = 1, witnessed by ⟨ratioOfSpecificHeatCapacities, efficiency, …⟩ with ratioOfSpecificHeatCapacities_ne_efficiency (a decide) and reflexivity. Axiom-free.