IndisputableMonolith.Papers.GCIC.Thermodynamics

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Cost
   4import IndisputableMonolith.Foundation.DiscretenessForcing
   5import IndisputableMonolith.Numerics.Interval.Log
   6
   7/-!
   8# GCIC Phase Thermodynamics: Stiffness, Barrier, and Phase Structure
   9
  10Formalizes the key constants from the GCIC Response paper
  11"Two Upgrades for the GCIC Paper" (Feb 2026).
  12-/
  13
  14namespace IndisputableMonolith
  15namespace Papers.GCIC
  16namespace Thermodynamics
  17
  18open Real
  19
  20/-- log(Constants.phi) > 0.48. Inherited from the Numerics log-bound on goldenRatio. -/
  21private lemma log_phi_gt_048 : (0.48 : ℝ) < Real.log Constants.phi := by
  22  have h := IndisputableMonolith.Numerics.log_phi_gt_048
  23  simpa [IndisputableMonolith.Constants.phi, Real.goldenRatio] using h
  24
  25/-- log(Constants.phi) < 0.483. -/
  26private lemma log_phi_lt_0483 : Real.log Constants.phi < (0.483 : ℝ) := by
  27  have h := IndisputableMonolith.Numerics.log_phi_lt_0483
  28  simpa [IndisputableMonolith.Constants.phi, Real.goldenRatio] using h
  29
  30/-! ## Part I: GCIC Constants -/
  31
  32/-- **GCIC STIFFNESS CONSTANT**: κ = (ln φ)²/2 ≈ 0.116. -/
  33noncomputable def gcic_stiffness : ℝ := (Real.log Constants.phi) ^ 2 / 2
  34
  35theorem gcic_stiffness_pos : 0 < gcic_stiffness := by
  36  unfold gcic_stiffness
  37  apply div_pos _ (by norm_num)
  38  exact pow_pos (Real.log_pos Constants.one_lt_phi) 2
  39
  40/-- κ ∈ (0.1152, 0.1167). -/
  41theorem gcic_stiffness_bounds :
  42    (0.1152 : ℝ) < gcic_stiffness ∧ gcic_stiffness < 0.1167 := by
  43  unfold gcic_stiffness
  44  have hlo := log_phi_gt_048
  45  have hhi := log_phi_lt_0483
  46  constructor <;> nlinarith [sq_nonneg (Real.log Constants.phi - 0.48),
  47                              sq_nonneg (Real.log Constants.phi - 0.483),
  48                              sq_nonneg (Real.log Constants.phi)]
  49
  50/-- **PHASE BARRIER**: J̃(1/2) = cosh(ln φ/2) - 1 ≈ 0.029. -/
  51noncomputable def phase_barrier : ℝ :=
  52  Real.cosh (Real.log Constants.phi / 2) - 1
  53
  54theorem phase_barrier_pos : 0 < phase_barrier := by
  55  unfold phase_barrier
  56  have hne : Real.log Constants.phi / 2 ≠ 0 := by
  57    apply div_ne_zero _ two_ne_zero
  58    exact Real.log_ne_zero_of_pos_of_ne_one Constants.phi_pos (ne_of_gt Constants.one_lt_phi)
  59  have hgt : 1 < Real.cosh (Real.log Constants.phi / 2) := Real.one_lt_cosh.mpr hne
  60  linarith
  61
  62/-- J̃(1/2) lower bound: phase_barrier ≥ 0.0287.
  63    Proof: log φ / 2 > 0.24, cosh(0.24) ≥ 1 + 0.24²/2 = 1.0288. -/
  64theorem phase_barrier_lower : (0.0287 : ℝ) ≤ phase_barrier := by
  65  unfold phase_barrier
  66  have hlo := log_phi_gt_048
  67  have hmono_lo : Real.cosh 0.24 ≤ Real.cosh (Real.log Constants.phi / 2) := by
  68    rw [Real.cosh_le_cosh, abs_of_nonneg (by norm_num : (0 : ℝ) ≤ 0.24),
  69        abs_of_nonneg (by linarith)]; linarith
  70  have h_lo_val : 1.0288 ≤ Real.cosh 0.24 := by
  71    have h := Cost.cosh_quadratic_lower_bound 0.24; norm_num at h; linarith
  72  linarith
  73
  74/-- J̃(1/2) upper bound: phase_barrier < 0.032.
  75    Numerically: cosh(log φ/2) ≈ cosh(0.241) ≈ 1.0293 < 1.032.
  76    Proof: cosh_quadratic_bound gives |cosh x - 1 - x²/2| ≤ x⁴/20 for |x| < 1.
  77    With x = log φ/2 < 0.2415, we get cosh x ≤ 1 + x²/2 + x⁴/20 < 1.032. -/
  78theorem phase_barrier_upper : phase_barrier < 0.032 := by
  79  unfold phase_barrier
  80  have hx_pos : 0 < Real.log Constants.phi / 2 := div_pos (Real.log_pos Constants.one_lt_phi) (by norm_num)
  81  have hx_lt : Real.log Constants.phi / 2 < (0.242 : ℝ) := by linarith [log_phi_lt_0483]
  82  have hx_abs : |Real.log Constants.phi / 2| < 1 := by rw [abs_of_pos hx_pos]; linarith
  83  have hbound := Foundation.DiscretenessForcing.cosh_quadratic_bound (Real.log Constants.phi / 2) hx_abs
  84  have hx_sq : (Real.log Constants.phi / 2) ^ 2 < (0.0586 : ℝ) := by
  85    calc (Real.log Constants.phi / 2) ^ 2 < (0.242 : ℝ) ^ 2 := sq_lt_sq' (by linarith) hx_lt
  86      _ = 0.058564 := by norm_num
  87      _ < 0.0586 := by norm_num
  88  have hx_four : (Real.log Constants.phi / 2) ^ 4 < (0.00344 : ℝ) := by
  89    have hsq : (Real.log Constants.phi / 2) ^ 2 < (0.242 : ℝ) ^ 2 := sq_lt_sq' (by linarith) hx_lt
  90    have hneg : -((0.242 : ℝ) ^ 2) < (Real.log Constants.phi / 2) ^ 2 := by
  91      have : 0 ≤ (Real.log Constants.phi / 2) ^ 2 := sq_nonneg _
  92      linarith
  93    calc (Real.log Constants.phi / 2) ^ 4 = ((Real.log Constants.phi / 2) ^ 2) ^ 2 := by ring
  94      _ < ((0.242 : ℝ) ^ 2) ^ 2 := sq_lt_sq' hneg hsq
  95      _ = (0.242 : ℝ) ^ 4 := by ring
  96      _ < 0.00344 := by norm_num
  97  have h_rest : Real.cosh (Real.log Constants.phi / 2) - 1 - (Real.log Constants.phi / 2) ^ 2 / 2 ≤
  98      (Real.log Constants.phi / 2) ^ 4 / 20 := by
  99    rw [abs_le] at hbound; exact hbound.2
 100  calc Real.cosh (Real.log Constants.phi / 2) - 1
 101      = (Real.cosh (Real.log Constants.phi / 2) - 1 - (Real.log Constants.phi / 2) ^ 2 / 2) +
 102          (Real.log Constants.phi / 2) ^ 2 / 2 := by ring
 103    _ ≤ (Real.log Constants.phi / 2) ^ 4 / 20 + (Real.log Constants.phi / 2) ^ 2 / 2 := by linarith
 104    _ < 0.00344 / 20 + 0.0586 / 2 := by nlinarith
 105    _ = 0.029472 := by norm_num
 106    _ < 0.032 := by norm_num
 107
 108/-- **MEAN-FIELD CRITICAL TEMPERATURE**: TRc,MF = 3(ln φ)² ≈ 0.694 (d=3, z=6). -/
 109noncomputable def mf_critical_temperature : ℝ := 3 * (Real.log Constants.phi) ^ 2
 110
 111theorem mf_critical_temperature_pos : 0 < mf_critical_temperature := by
 112  unfold mf_critical_temperature
 113  apply mul_pos (by norm_num)
 114  exact pow_pos (Real.log_pos Constants.one_lt_phi) 2
 115
 116/-- TRc,MF ∈ (0.691, 0.701). -/
 117theorem mf_critical_temperature_bounds :
 118    (0.691 : ℝ) < mf_critical_temperature ∧ mf_critical_temperature < 0.701 := by
 119  unfold mf_critical_temperature
 120  have hlo := log_phi_gt_048
 121  have hhi := log_phi_lt_0483
 122  constructor <;> nlinarith [sq_nonneg (Real.log Constants.phi - 0.48),
 123                              sq_nonneg (Real.log Constants.phi - 0.483),
 124                              sq_nonneg (Real.log Constants.phi)]
 125
 126theorem mf_temp_eq_six_kappa : mf_critical_temperature = 6 * gcic_stiffness := by
 127  unfold mf_critical_temperature gcic_stiffness; ring
 128
 129/-! ## Part II: Uniform Convexity (Proposition 1) -/
 130
 131/-- V''(t) = cosh(t) ≥ 1 — uniform convexity of the phase potential. -/
 132theorem noncompact_uniform_convexity (t : ℝ) : 1 ≤ Real.cosh t :=
 133  Real.one_le_cosh t
 134
 135/-- cosh(t) - 1 ≥ t²/2 (quadratic lower bound from uniform convexity). -/
 136theorem jlog_above_half_square (t : ℝ) : t ^ 2 / 2 ≤ Real.cosh t - 1 := by
 137  have := Cost.cosh_quadratic_lower_bound t; linarith
 138
 139/-! ## Summary certificate -/
 140
 141theorem gcic_thermodynamics_cert :
 142    0 < gcic_stiffness ∧ 0 < phase_barrier ∧ 0 < mf_critical_temperature ∧
 143    (∀ t, 1 ≤ Real.cosh t) :=
 144  ⟨gcic_stiffness_pos, phase_barrier_pos, mf_critical_temperature_pos,
 145   noncompact_uniform_convexity⟩
 146
 147end Thermodynamics
 148end Papers.GCIC
 149end IndisputableMonolith
 150