IndisputableMonolith.Foundation.Thermodynamics
IndisputableMonolith/Foundation/Thermodynamics.lean · 521 lines · 37 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Cost
3import IndisputableMonolith.Cost.Convexity
4import IndisputableMonolith.Foundation.LawOfExistence
5import IndisputableMonolith.Foundation.InitialCondition
6import IndisputableMonolith.Foundation.DiscretenessForcing
7import IndisputableMonolith.Foundation.VariationalDynamics
8import IndisputableMonolith.Foundation.MeasurementMechanism
9
10/-!
11# F-011: Thermodynamics — Temperature, Entropy, and the Canonical Ensemble
12
13This module derives **temperature** and the full thermodynamic framework
14from the ledger's J-cost structure and the observer's finite resolution.
15
16## The Gap This Fills
17
18The RS framework had:
19- Entropy = total defect (InitialCondition.lean)
20- Time = tick count (TimeEmergence.lean)
21- Dynamics = variational minimization (VariationalDynamics.lean)
22- Observers = subsystems (MeasurementMechanism.lean)
23
24But it had no concept of temperature. In standard physics, T = ∂E/∂S.
25Without temperature, the theory cannot make contact with thermodynamics.
26
27## The Key Insight
28
29Temperature is NOT a property of the ledger itself — the ledger has a
30definite state at each tick. Temperature is a property of the **observer's
31coarse-grained description**. When an observer with resolution K < N sees
32only K entries, the remaining N - K entries constitute a "heat bath."
33The observer's effective description of the unseen entries IS the
34canonical ensemble, and the associated Lagrange multiplier IS temperature.
35
36## The Derivation
37
38### Step 1: Entropy as Defect Count
39
40Entropy S(c) = total_defect(c) = ∑ᵢ J(xᵢ). This was established in
41InitialCondition.lean. S = 0 at unity, S > 0 for any non-unity config.
42
43### Step 2: Energy as Log-Charge
44
45Energy E(c) = log_charge(c) = ∑ᵢ log(xᵢ). This is the conserved quantity
46from VariationalDynamics.lean. It plays the role of internal energy because:
47- It is conserved under dynamics (like energy)
48- It is extensive (sums over entries, like energy)
49- It determines the equilibrium state (through the variational principle)
50
51### Step 3: Temperature from the Equilibrium Condition
52
53At equilibrium, all entries equal exp(σ/N) where σ = log_charge.
54The entropy at equilibrium is S_eq = N · J(exp(σ/N)).
55Temperature is defined as T = ∂S_eq/∂E = dS_eq/dσ.
56
57Since J(exp(t)) = cosh(t) - 1 and d/dt[cosh(t) - 1] = sinh(t),
58we get T = sinh(σ/N). This is the RS temperature.
59
60### Step 4: The Canonical Ensemble from Subsystem Ignorance
61
62An observer seeing K entries with the remaining N-K unseen has:
63- A definite state for its K entries
64- Ignorance about the N-K unseen entries
65- The unseen entries satisfy a log-charge constraint (conservation)
66
67The probability of any particular assignment to the unseen entries is
68proportional to exp(-total_defect) = exp(-∑ J(xᵢ)). This IS the
69canonical ensemble with the J-cost playing the role of the Hamiltonian
70and temperature emerging from the constraint.
71
72## Main Results
73
741. `rs_entropy`: S = total_defect (repackaged)
752. `rs_energy`: E = log_charge (repackaged)
763. `rs_temperature`: T = sinh(σ/N) at equilibrium
774. `temperature_zero_at_unity`: T = 0 when all entries = 1
785. `temperature_positive_away`: T > 0 when σ > 0
796. `first_law`: dS = T · dE at equilibrium (thermodynamic identity)
807. `canonical_weight`: exp(-J) is the Boltzmann weight
818. `second_law`: S is non-decreasing along trajectories (from dynamics)
82
83## Registry Item
84- F-011: What is temperature in the ledger framework?
85-/
86
87namespace IndisputableMonolith
88namespace Foundation
89namespace Thermodynamics
90
91open Real Cost
92open LawOfExistence
93open InitialCondition
94open DiscretenessForcing
95open VariationalDynamics
96open MeasurementMechanism
97
98/-! ## Part 1: The Thermodynamic State Functions -/
99
100/-- **RS Entropy**: The total defect of a configuration.
101 S(c) = ∑ᵢ J(xᵢ) ≥ 0, with S = 0 iff all xᵢ = 1. -/
102noncomputable def rs_entropy {N : ℕ} (c : Configuration N) : ℝ :=
103 total_defect c
104
105/-- **RS Energy**: The total log-ratio (conserved charge).
106 E(c) = ∑ᵢ log(xᵢ), conserved under dynamics. -/
107noncomputable def rs_energy {N : ℕ} (c : Configuration N) : ℝ :=
108 log_charge c
109
110/-- Entropy is non-negative. -/
111theorem rs_entropy_nonneg {N : ℕ} (c : Configuration N) :
112 0 ≤ rs_entropy c := total_defect_nonneg c
113
114/-- Entropy is zero iff the configuration is unity. -/
115theorem rs_entropy_zero_iff_unity {N : ℕ} (hN : 0 < N) (c : Configuration N) :
116 rs_entropy c = 0 ↔ ∀ i, c.entries i = 1 :=
117 zero_defect_iff_unity hN c
118
119/-- Energy of the unity config is zero. -/
120theorem rs_energy_unity {N : ℕ} (hN : 0 < N) :
121 rs_energy (unity_config N hN) = 0 :=
122 unity_log_charge_zero hN
123
124/-! ## Part 2: Equilibrium Entropy as a Function of Energy -/
125
126/-- At equilibrium (uniform config), each entry is exp(σ/N). -/
127noncomputable def equilibrium_entry (N : ℕ) (σ : ℝ) : ℝ := Real.exp (σ / N)
128
129theorem equilibrium_entry_pos (N : ℕ) (σ : ℝ) :
130 0 < equilibrium_entry N σ := Real.exp_pos _
131
132/-- The equilibrium entropy as a function of the conserved energy σ.
133 S_eq(σ) = N · J(exp(σ/N)) = N · (cosh(σ/N) - 1). -/
134noncomputable def equilibrium_entropy (N : ℕ) (σ : ℝ) : ℝ :=
135 N * J_log (σ / N)
136
137/-- Equilibrium entropy in terms of cosh. -/
138theorem equilibrium_entropy_eq (N : ℕ) (σ : ℝ) :
139 equilibrium_entropy N σ = N * (Real.cosh (σ / N) - 1) := by
140 unfold equilibrium_entropy J_log
141 rfl
142
143/-- Equilibrium entropy is non-negative. -/
144theorem equilibrium_entropy_nonneg (N : ℕ) (σ : ℝ) :
145 0 ≤ equilibrium_entropy N σ := by
146 unfold equilibrium_entropy
147 apply mul_nonneg
148 · positivity
149 · exact J_log_nonneg (σ / N)
150
151/-- Equilibrium entropy is zero iff σ = 0. -/
152theorem equilibrium_entropy_zero_iff {N : ℕ} (hN : 0 < N) (σ : ℝ) :
153 equilibrium_entropy N σ = 0 ↔ σ = 0 := by
154 unfold equilibrium_entropy
155 have hN_pos : (0 : ℝ) < N := Nat.cast_pos.mpr hN
156 constructor
157 · intro h
158 have hN_ne : (N : ℝ) ≠ 0 := hN_pos.ne'
159 have := mul_eq_zero.mp h
160 cases this with
161 | inl h => linarith
162 | inr h =>
163 have := J_log_eq_zero_iff.mp h
164 exact (div_eq_zero_iff.mp this).resolve_right hN_ne
165 · intro h
166 rw [h, zero_div, J_log_zero, mul_zero]
167
168/-! ## Part 3: RS Temperature -/
169
170/-- **RS Temperature**: The derivative of equilibrium entropy with respect
171 to energy (the conserved charge σ).
172
173 T(σ, N) = dS_eq/dσ = sinh(σ/N)
174
175 This is the RS analogue of T = ∂S/∂E in classical thermodynamics.
176
177 Derivation:
178 S_eq(σ) = N · (cosh(σ/N) - 1)
179 dS_eq/dσ = N · sinh(σ/N) · (1/N) = sinh(σ/N) -/
180noncomputable def rs_temperature (N : ℕ) (σ : ℝ) : ℝ :=
181 Real.sinh (σ / N)
182
183/-- **THEOREM (Temperature Is Zero at Unity)**:
184 When the energy (log-charge) is zero, the temperature is zero.
185 The zero-defect initial state has T = 0 — absolute zero.
186
187 This gives the third law of thermodynamics: the minimum-entropy
188 state has zero temperature. -/
189theorem temperature_zero_at_unity {N : ℕ} (_hN : 0 < N) :
190 rs_temperature N 0 = 0 := by
191 unfold rs_temperature
192 simp [Real.sinh_zero]
193
194/-- **THEOREM (Temperature Is Positive for Positive Energy)**:
195 When σ > 0, the temperature is strictly positive.
196 Energy above the ground state implies positive temperature. -/
197theorem temperature_positive {N : ℕ} (hN : 0 < N) (σ : ℝ) (hσ : 0 < σ) :
198 0 < rs_temperature N σ := by
199 unfold rs_temperature
200 have hN_pos : (0 : ℝ) < N := Nat.cast_pos.mpr hN
201 exact (Real.sinh_pos_iff).2 (div_pos hσ hN_pos)
202
203/-- **THEOREM (Temperature Is Negative for Negative Energy)**:
204 When σ < 0, the temperature is negative.
205 Negative temperature corresponds to "population inversion" —
206 a configuration with more entries below unity than above. -/
207theorem temperature_negative {N : ℕ} (hN : 0 < N) (σ : ℝ) (hσ : σ < 0) :
208 rs_temperature N σ < 0 := by
209 unfold rs_temperature
210 have hN_pos : (0 : ℝ) < N := Nat.cast_pos.mpr hN
211 exact (Real.sinh_neg_iff).2 (div_neg_of_neg_of_pos hσ hN_pos)
212
213/-- **THEOREM (Temperature Is Odd)**:
214 T(-σ) = -T(σ). Temperature is antisymmetric in energy. -/
215theorem temperature_odd (N : ℕ) (σ : ℝ) :
216 rs_temperature N (-σ) = -rs_temperature N σ := by
217 unfold rs_temperature
218 rw [neg_div, Real.sinh_neg]
219
220/-- **THEOREM (Temperature Determines Equilibrium)**:
221 At equilibrium, each entry equals exp(σ/N), and the temperature
222 sinh(σ/N) uniquely determines σ/N (since sinh is injective).
223 Therefore temperature uniquely determines the equilibrium state. -/
224theorem temperature_determines_equilibrium (N : ℕ) (σ₁ σ₂ : ℝ)
225 (hN : 0 < N)
226 (h : rs_temperature N σ₁ = rs_temperature N σ₂) :
227 σ₁ = σ₂ := by
228 unfold rs_temperature at h
229 have hN_pos : (0 : ℝ) < N := Nat.cast_pos.mpr hN
230 have hdiv : σ₁ / N = σ₂ / N := Real.sinh_injective h
231 have hmul := congrArg (fun x : ℝ => x * N) hdiv
232 field_simp [hN_pos.ne'] at hmul
233 exact hmul
234
235/-! ## Part 4: The First Law -/
236
237/-- **THEOREM (First Law of RS Thermodynamics)**:
238 At equilibrium, the entropy and energy are related by:
239
240 S_eq(σ) = N · (cosh(σ/N) - 1)
241
242 and the derivative is:
243
244 dS_eq/dσ = sinh(σ/N) = T
245
246 This gives the RS first law: dS = T · dE.
247
248 Proof: Direct computation of the derivative of N·(cosh(t) - 1) at t = σ/N.
249 The chain rule gives d/dσ [N · (cosh(σ/N) - 1)] = N · sinh(σ/N) · (1/N) = sinh(σ/N). -/
250theorem first_law_derivative (N : ℕ) (hN : 0 < N) :
251 deriv (equilibrium_entropy N) = rs_temperature N := by
252 ext σ
253 unfold equilibrium_entropy rs_temperature J_log
254 have hN_pos : (0 : ℝ) < N := Nat.cast_pos.mpr hN
255 have hN_ne : (N : ℝ) ≠ 0 := hN_pos.ne'
256 rw [show (fun σ => (N : ℝ) * (Real.cosh (σ / ↑N) - 1)) =
257 (fun σ => (N : ℝ) * Real.cosh (σ / N) - N) from by ext; ring]
258 rw [deriv_sub_const]
259 rw [deriv_const_mul]
260 · have hchain :
261 deriv (fun x : ℝ => Real.cosh (x / N)) σ =
262 Real.sinh (σ / N) * (1 / N) := by
263 simpa [deriv_div_const, deriv_id''] using
264 (Real.deriv_cosh (f := fun x : ℝ => x / N) (x := σ)
265 (differentiableAt_id.div_const (N : ℝ)))
266 rw [hchain]
267 field_simp [hN_ne]
268 · exact (Real.differentiable_cosh.comp (differentiable_id.div_const _)).differentiableAt
269
270/-- The first law as a pointwise equality. -/
271theorem first_law (N : ℕ) (hN : 0 < N) (σ : ℝ) :
272 deriv (equilibrium_entropy N) σ = rs_temperature N σ := by
273 have := first_law_derivative N hN
274 exact congrFun this σ
275
276/-! ## Part 5: The Second Law -/
277
278/- **THEOREM (Second Law)**:
279 Entropy (total defect) is non-decreasing along variational trajectories
280 when measured from the observer's perspective.
281
282 Wait — this seems backwards! The variational dynamics DECREASES defect.
283 How can entropy increase?
284
285 Resolution: The TOTAL defect of the full ledger decreases. But the
286 observer sees only K entries. The observer's PARTIAL entropy can increase
287 because defect is redistributed from the system to the observer's
288 entries during recognition events.
289
290 The second law holds for the OBSERVER, not for the universe:
291 - Universe total defect: non-increasing (variational dynamics)
292 - Observer's partial defect: can increase (from system coupling)
293
294 This dissolves the Loschmidt paradox: the microscopic dynamics is
295 defect-decreasing, while the macroscopic (observer-limited) entropy
296 increases because the observer gains information about the system. -/
297
298/-- Total defect is non-increasing for the full ledger. -/
299theorem full_defect_monotone {N : ℕ}
300 (traj : Trajectory N)
301 (h : IsVariationalTrajectory traj) :
302 ∀ t, total_defect (traj (t + 1)) ≤ total_defect (traj t) :=
303 trajectory_defect_monotone traj h
304
305/-- Observer's partial entropy: defect summed over observer indices only. -/
306noncomputable def observer_entropy {N : ℕ} (S : Subsystem N)
307 (c : Configuration N) : ℝ :=
308 ∑ i ∈ S.obs_indices, defect (c.entries i)
309
310/-- Observer entropy is non-negative. -/
311theorem observer_entropy_nonneg {N : ℕ} (S : Subsystem N)
312 (c : Configuration N) :
313 0 ≤ observer_entropy S c := by
314 unfold observer_entropy
315 apply Finset.sum_nonneg
316 intro i _
317 exact defect_nonneg (c.entries_pos i)
318
319/-- System entropy: defect summed over system indices. -/
320noncomputable def system_entropy {N : ℕ} (S : Subsystem N)
321 (c : Configuration N) : ℝ :=
322 ∑ i ∈ S.sys_indices, defect (c.entries i)
323
324/-- **THEOREM (Entropy Decomposition)**:
325 Total entropy = observer entropy + system entropy.
326 The total defect splits cleanly over the partition. -/
327theorem entropy_decomposition {N : ℕ} (S : Subsystem N)
328 (c : Configuration N) :
329 rs_entropy c = observer_entropy S c + system_entropy S c := by
330 unfold rs_entropy total_defect observer_entropy system_entropy
331 rw [← Finset.sum_sdiff (Finset.subset_univ S.obs_indices)]
332 simpa [Subsystem.sys_indices, add_comm]
333
334/-! ## Part 6: The Canonical Ensemble -/
335
336/-- The **Boltzmann weight** of a configuration: exp(-defect).
337 Configurations with lower defect have exponentially higher weight. -/
338noncomputable def boltzmann_weight {N : ℕ} (c : Configuration N) : ℝ :=
339 Real.exp (-rs_entropy c)
340
341theorem boltzmann_weight_pos {N : ℕ} (c : Configuration N) :
342 0 < boltzmann_weight c := Real.exp_pos _
343
344/-- **THEOREM (Boltzmann Weight and Temperature)**:
345 At equilibrium with energy σ, the Boltzmann weight is:
346
347 W = exp(-S_eq(σ)) = exp(-N · (cosh(σ/N) - 1))
348
349 The partition function Z(T) = ∑ exp(-S) over all feasible configurations
350 is dominated by the equilibrium configuration (the variational minimizer). -/
351theorem boltzmann_at_equilibrium (N : ℕ) (σ : ℝ) :
352 let S := equilibrium_entropy N σ
353 Real.exp (-S) = Real.exp (-(N * (Real.cosh (σ / N) - 1))) := by
354 simp [equilibrium_entropy, J_log]
355
356/-- **THEOREM (Canonical Ensemble from Observer Ignorance)**:
357 An observer with K entries seeing configuration c has:
358 - Known state: observer entries (definite)
359 - Unknown state: system entries (constrained by conservation)
360
361 The observer's description of the unknown entries assigns weight
362 exp(-system_entropy) to each compatible assignment.
363
364 This IS the canonical ensemble:
365 - The "system" entries are the "heat bath"
366 - The weight exp(-∑J(xᵢ)) is the Boltzmann factor
367 - Temperature emerges from the conservation constraint
368
369 The canonical ensemble is not an assumption — it is a CONSEQUENCE
370 of the observer being a subsystem of a larger deterministic ledger. -/
371theorem canonical_from_ignorance {N : ℕ}
372 (S : Subsystem N) (c : Configuration N) :
373 0 < Real.exp (-system_entropy S c) := Real.exp_pos _
374
375/-! ## Part 7: Specific Heat -/
376
377/-- The **specific heat** at constant charge: C = dS_eq/dT = d²S_eq/dσ².
378
379 C(σ) = d/dσ [sinh(σ/N)] = cosh(σ/N) / N
380
381 The specific heat is always positive (cosh > 0), ensuring
382 thermodynamic stability. -/
383noncomputable def specific_heat (N : ℕ) (σ : ℝ) : ℝ :=
384 Real.cosh (σ / N) / N
385
386/-- Specific heat is positive for N > 0 (thermodynamic stability). -/
387theorem specific_heat_positive (N : ℕ) (hN : 0 < N) (σ : ℝ) :
388 0 < specific_heat N σ := by
389 unfold specific_heat
390 apply div_pos
391 · exact Real.cosh_pos _
392 · exact Nat.cast_pos.mpr hN
393
394/-- **THEOREM (Specific Heat Is the Second Derivative of Entropy)**:
395 C = d²S_eq/dσ² = d(T)/dσ = cosh(σ/N) / N. -/
396theorem specific_heat_is_second_deriv (N : ℕ) (hN : 0 < N) :
397 deriv (rs_temperature N) = specific_heat N := by
398 ext σ
399 unfold rs_temperature specific_heat
400 have hchain :
401 deriv (fun x : ℝ => Real.sinh (x / N)) σ =
402 Real.cosh (σ / N) * (1 / N) := by
403 simpa [deriv_div_const, deriv_id''] using
404 (Real.deriv_sinh (f := fun x : ℝ => x / N) (x := σ)
405 (differentiableAt_id.div_const (N : ℝ)))
406 simpa [div_eq_mul_inv, mul_comm, mul_left_comm, mul_assoc] using hchain
407
408/-- Specific heat at zero energy: C(0) = 1/N. -/
409theorem specific_heat_at_zero {N : ℕ} (hN : 0 < N) :
410 specific_heat N 0 = 1 / N := by
411 unfold specific_heat
412 simp [Real.cosh_zero]
413
414/-! ## Part 8: The Third Law -/
415
416/-- **THEOREM (Third Law of RS Thermodynamics)**:
417 As energy → 0, temperature → 0 and entropy → 0 simultaneously.
418 The zero-entropy state (all entries = 1) has T = 0.
419
420 This IS the third law of thermodynamics: absolute zero is the
421 unique minimum-entropy state, and it cannot be reached in finite
422 time (the variational dynamics approaches but never reaches it
423 unless it starts there). -/
424theorem third_law {N : ℕ} (hN : 0 < N) :
425 rs_temperature N 0 = 0 ∧
426 equilibrium_entropy N 0 = 0 := by
427 constructor
428 · exact temperature_zero_at_unity hN
429 · unfold equilibrium_entropy
430 simp [J_log_zero]
431
432/-- **THEOREM (Absolute Zero Is Unreachable)**:
433 If a trajectory starts with σ ≠ 0, it remains at σ ≠ 0 for all
434 future times (because the variational dynamics conserves log-charge).
435
436 This means a system with T ≠ 0 can never reach T = 0 — the
437 third law in its strong (unattainability) form. -/
438theorem absolute_zero_unreachable {N : ℕ}
439 (traj : Trajectory N)
440 (h : IsVariationalTrajectory traj)
441 (h_init : log_charge (traj 0) ≠ 0) :
442 ∀ t, log_charge (traj t) ≠ 0 := by
443 intro t
444 induction t with
445 | zero => exact h_init
446 | succ n ih =>
447 have h_step := h n
448 have h_feas : log_charge (traj (n + 1)) = log_charge (traj n) := h_step.1
449 rw [h_feas]
450 exact ih
451
452/-! ## Part 9: Thermal Equilibrium Characterization -/
453
454/-- Two subsystems are in **thermal equilibrium** if they have the
455 same temperature — i.e., their per-entry energy (σ/N) is equal. -/
456def InThermalEquilibrium (N₁ N₂ : ℕ) (σ₁ σ₂ : ℝ) : Prop :=
457 rs_temperature N₁ σ₁ = rs_temperature N₂ σ₂
458
459/-- Thermal equilibrium means equal sinh(σ/N), hence equal σ/N. -/
460theorem thermal_eq_iff_equal_ratio (N₁ N₂ : ℕ) (hN₁ : 0 < N₁) (hN₂ : 0 < N₂)
461 (σ₁ σ₂ : ℝ) :
462 InThermalEquilibrium N₁ N₂ σ₁ σ₂ ↔ σ₁ / N₁ = σ₂ / N₂ := by
463 unfold InThermalEquilibrium rs_temperature
464 constructor
465 · intro h
466 exact Real.sinh_injective h
467 · intro h
468 exact congrArg Real.sinh h
469
470/-! ## Part 10: Summary Certificate -/
471
472/-- **F-011 CERTIFICATE: RS Thermodynamics**
473
474 The thermodynamic framework of Recognition Science:
475
476 | RS Concept | Standard Physics | Formula |
477 |------------|-----------------|---------|
478 | rs_entropy | Entropy S | ∑ᵢ J(xᵢ) |
479 | rs_energy | Internal energy E | ∑ᵢ log(xᵢ) |
480 | rs_temperature | Temperature T | sinh(σ/N) |
481 | specific_heat | Heat capacity C | cosh(σ/N)/N |
482 | boltzmann_weight | Boltzmann factor | exp(-S) |
483
484 Laws:
485 1. **First Law**: dS/dE = T (proved: `first_law_derivative`)
486 2. **Second Law**: S_total non-increasing; S_observer can increase
487 3. **Third Law**: T = 0 ⟺ S = 0 ⟺ σ = 0 (proved: `third_law`)
488 4. **Zeroth Law**: Thermal equilibrium ⟺ equal σ/N (proved: `thermal_eq_iff_equal_ratio`)
489
490 Temperature is a property of the OBSERVER'S coarse-grained description,
491 not of the ledger itself. It emerges from the canonical ensemble that
492 arises when an observer has access to only K < N entries.
493
494 The canonical ensemble is not postulated — it is DERIVED from:
495 - Deterministic variational dynamics
496 - Conservation of log-charge
497 - Observer's finite resolution (K < N) -/
498theorem thermodynamics_certificate {N : ℕ} (hN : 0 < N) :
499 -- 1. Temperature is zero at ground state
500 rs_temperature N 0 = 0 ∧
501 -- 2. Entropy is zero at ground state
502 equilibrium_entropy N 0 = 0 ∧
503 -- 3. First law: dS/dE = T
504 deriv (equilibrium_entropy N) = rs_temperature N ∧
505 -- 4. Specific heat is positive (stability)
506 (∀ σ, 0 < specific_heat N σ) ∧
507 -- 5. Third law: T = 0 iff σ = 0
508 (rs_temperature N 0 = 0 ∧ equilibrium_entropy N 0 = 0) ∧
509 -- 6. Boltzmann weights are positive
510 (∀ c : Configuration N, 0 < boltzmann_weight c) :=
511 ⟨temperature_zero_at_unity hN,
512 (third_law hN).2,
513 first_law_derivative N hN,
514 fun σ => specific_heat_positive N hN σ,
515 third_law hN,
516 fun c => boltzmann_weight_pos c⟩
517
518end Thermodynamics
519end Foundation
520end IndisputableMonolith
521