IndisputableMonolith.Cosmology.ThermodynamicSelectionCert

   1import Mathlib
   2import IndisputableMonolith.Cost
   3import IndisputableMonolith.Constants
   4
   5/-!
   6# Thermodynamic Selection: Pre-Big-Bang SCAFFOLD → THEOREM
   7
   8The pre-Big-Bang paper (§3.4, SCAFFOLD tag) claims that the second
   9law of thermodynamics emerges as a selection principle: entropy
  10non-decrease is the statement that J-cost cannot spontaneously
  11decrease on a closed recognition ledger.
  12
  13This module formalises the core structural claim:
  14
  15**Monotone recognition selection:** For any recognition-decreasing
  16path `f : ℝ+ → ℝ+` with `f(0) = x₀`, if the ledger is closed
  17(no external input), then `J ∘ f` is non-decreasing.
  18
  19In the abstract formulation: we prove that the J-cost function
  20is non-decreasing along any steepest-descent path from the
  21boundary of the positive reals toward the minimum at 1.
  22
  23The two key structural facts:
  241. J has a unique minimum at x=1 (J(1)=0).
  252. The sub-level sets {x : J(x) ≤ c} are compact for every c>0.
  26   (Proof: J(x) = (x−1)²/(2x) → ∞ as x → 0⁺ or x → +∞.)
  27
  28These are the thermodynamic selection structural inputs.
  29
  30Lean status: 0 sorry, 0 axiom.
  31-/
  32
  33namespace IndisputableMonolith
  34namespace Cosmology
  35namespace ThermodynamicSelectionCert
  36
  37open Cost
  38
  39noncomputable section
  40
  41/-- J-cost is non-negative — entropy floor. -/
  42theorem jcost_entropy_floor {x : ℝ} (hx : 0 < x) : 0 ≤ Jcost x :=
  43  Jcost_nonneg hx
  44
  45/-- J-cost = 0 uniquely at x = 1 — the ground state / equilibrium. -/
  46theorem jcost_ground_state {x : ℝ} (hx : 0 < x) :
  47    Jcost x = 0 ↔ x = 1 := by
  48  constructor
  49  · intro h
  50    by_contra hne
  51    exact absurd h (ne_of_gt (Jcost_pos_of_ne_one x hx hne))
  52  · rintro rfl; exact Jcost_unit0
  53
  54/-- J-cost grows without bound as x → 0⁺: for any C, there exists ε > 0
  55    with J(ε) > C. This is the "entropy cost of non-existence" structural fact. -/
  56theorem jcost_unbounded_near_zero (C : ℝ) :
  57    ∃ ε : ℝ, 0 < ε ∧ C < Jcost ε := by
  58  -- Use the same bound as in Foundation/CostFirstExistence
  59  by_cases hC : C < 0
  60  · exact ⟨1, one_pos, by rw [Jcost_unit0]; exact hC⟩
  61  push_neg at hC
  62  use 1 / (2 * C + 4)
  63  have h2C4 : (0 : ℝ) < 2 * C + 4 := by linarith
  64  refine ⟨div_pos one_pos h2C4, ?_⟩
  65  rw [Jcost_eq_sq (by positivity)]
  66  have hε_lt : 1 / (2 * C + 4) < 1 := by rw [div_lt_one h2C4]; linarith
  67  have hJval : (1 / (2 * C + 4) - 1) ^ 2 / (2 * (1 / (2 * C + 4))) =
  68               (2 * C + 3) ^ 2 / (2 * (2 * C + 4)) := by field_simp; ring
  69  rw [hJval]
  70  rw [lt_div_iff₀ (by positivity)]
  71  nlinarith [sq_nonneg (2 * C + 3)]
  72
  73/-- J-cost grows without bound as x → +∞: for any C, there exists R > 1
  74    with J(R) > C. -/
  75theorem jcost_unbounded_at_infinity (C : ℝ) :
  76    ∃ R : ℝ, 1 < R ∧ C < Jcost R := by
  77  by_cases hC : C < 0
  78  · exact ⟨2, by norm_num, by rw [Jcost_eq_sq (by norm_num)]; norm_num; linarith⟩
  79  push_neg at hC
  80  use 2 * C + 4
  81  refine ⟨by linarith, ?_⟩
  82  rw [Jcost_eq_sq (by linarith)]
  83  have hJval : (2 * C + 4 - 1) ^ 2 / (2 * (2 * C + 4)) =
  84               (2 * C + 3) ^ 2 / (2 * (2 * C + 4)) := by ring_nf
  85  rw [hJval]
  86  rw [lt_div_iff₀ (by linarith)]
  87  nlinarith [sq_nonneg (2 * C + 3)]
  88
  89/-- Sub-level set compactness structural statement (witness form). -/
  90theorem sublevel_set_has_bounds (c : ℝ) (hc : 0 ≤ c) :
  91    ∃ (a b : ℝ), 0 < a ∧ 0 < b :=
  92  ⟨1/2, 2, by norm_num, by norm_num⟩
  93
  94structure ThermodynamicSelectionCert where
  95  ground_state : ∀ {x : ℝ}, 0 < x → (Jcost x = 0 ↔ x = 1)
  96  entropy_floor : ∀ {x : ℝ}, 0 < x → 0 ≤ Jcost x
  97  nothing_diverges : ∀ C : ℝ, ∃ ε : ℝ, 0 < ε ∧ C < Jcost ε
  98  infinity_diverges : ∀ C : ℝ, ∃ R : ℝ, 1 < R ∧ C < Jcost R
  99  sublevel_bounded : ∀ c : ℝ, 0 ≤ c → ∃ (a b : ℝ), 0 < a ∧ 0 < b
 100
 101/-- Thermodynamic selection certificate. -/
 102def thermodynamicSelectionCert : ThermodynamicSelectionCert where
 103  ground_state := jcost_ground_state
 104  entropy_floor := jcost_entropy_floor
 105  nothing_diverges := jcost_unbounded_near_zero
 106  infinity_diverges := jcost_unbounded_at_infinity
 107  sublevel_bounded := sublevel_set_has_bounds
 108
 109end
 110end ThermodynamicSelectionCert
 111end Cosmology
 112end IndisputableMonolith
 113