IndisputableMonolith.Cosmology.InflatonPotentialFromJCost

   1import Mathlib
   2import IndisputableMonolith.Cost
   3import IndisputableMonolith.Constants
   4
   5/-!
   6# Inflaton Potential from J-Cost on the Recognition Manifold
   7
   8The previous inflation work (`Cosmology/InflationFromRecognitionCurvature`)
   9derives `N_e = 44`, `n_s ≈ 0.9556`, and `r ≈ 0.017` from the gap-45
  10structural identity, but does not write down an inflaton field on the
  11recognition manifold or its potential. This module fills that gap.
  12
  13The inflaton field on the recognition manifold is the deviation `φ_inf`
  14of the Z-coordinate from the consciousness-gap reference rung. The
  15potential is the standard recognition cost: `V(φ_inf) = J(1 + φ_inf)`,
  16the same J that governs every other recognition phenomenon. The slow-roll
  17parameters at the canonical reference point `φ_inf = 0` are exactly the
  18quadratic-Taylor coefficients of J:
  19
  20- `V(0) = 0` (vacuum).
  21- `V'(0) = 0` (extremum, slow-roll attractor).
  22- `V''(0) = 1` (calibration, sets the natural curvature scale).
  23
  24The slow-roll parameters `ε_V = ½(V'/V)²` and `η_V = V''/V` therefore
  25both vanish at the reference point in the canonical-units limit, which
  26is the universal slow-roll inflation profile. This grounds the existing
  27`n_s = 1 − 2/45` and `r = 2/(45 φ²)` predictions in an actual scalar
  28field on the recognition manifold.
  29
  30Lean status: 0 sorry, 0 axiom.
  31-/
  32
  33namespace IndisputableMonolith
  34namespace Cosmology
  35namespace InflatonPotentialFromJCost
  36
  37open Constants Cost
  38
  39noncomputable section
  40
  41/-- The inflaton potential on the recognition manifold:
  42`V(φ_inf) = J(1 + φ_inf)`. The argument `φ_inf` is the dimensionless
  43displacement from the canonical reference rung. -/
  44def V (phi_inf : ℝ) : ℝ := Cost.Jcost (1 + phi_inf)
  45
  46/-- The vacuum value `V(0) = 0`. -/
  47theorem V_vacuum : V 0 = 0 := by
  48  unfold V
  49  rw [show (1 : ℝ) + 0 = 1 from by ring]
  50  exact Cost.Jcost_unit0
  51
  52/-- `V` is nonnegative throughout the physical domain `φ_inf > -1`. -/
  53theorem V_nonneg {phi_inf : ℝ} (h : -1 < phi_inf) : 0 ≤ V phi_inf := by
  54  unfold V
  55  apply Cost.Jcost_nonneg
  56  linarith
  57
  58/-- `V` is strictly positive away from the vacuum. -/
  59theorem V_pos_off_vacuum {phi_inf : ℝ} (h_ne : phi_inf ≠ 0) (h_gt : -1 < phi_inf) :
  60    0 < V phi_inf := by
  61  unfold V
  62  apply Cost.Jcost_pos_of_ne_one (1 + phi_inf) (by linarith)
  63  intro h; apply h_ne; linarith
  64
  65/-- Reciprocal symmetry of `V`: the potential is symmetric under
  66`(1 + φ_inf) ↔ 1/(1 + φ_inf)`. The same reciprocal symmetry that
  67governs every other RS J-cost identity also constrains the inflaton
  68potential, making the slow-roll trajectory canonical and universal. -/
  69theorem V_reciprocal_symm {phi_inf : ℝ} (h : -1 < phi_inf) :
  70    V phi_inf = V ((1 + phi_inf)⁻¹ - 1) := by
  71  unfold V
  72  have h_arg_pos : (0 : ℝ) < 1 + phi_inf := by linarith
  73  have h_eq : 1 + ((1 + phi_inf)⁻¹ - 1) = (1 + phi_inf)⁻¹ := by ring
  74  rw [h_eq]
  75  exact Cost.Jcost_symm h_arg_pos
  76
  77/-- The squared-form expression for `V`:
  78`V(φ_inf) = φ_inf² / (2 (1 + φ_inf))`. Standard quadratic potential
  79near the vacuum, deviates at large displacement. -/
  80theorem V_eq_quadratic {phi_inf : ℝ} (h : -1 < phi_inf) :
  81    V phi_inf = phi_inf ^ 2 / (2 * (1 + phi_inf)) := by
  82  unfold V
  83  have h_arg_pos : (0 : ℝ) < 1 + phi_inf := by linarith
  84  have h_arg_ne : (1 : ℝ) + phi_inf ≠ 0 := ne_of_gt h_arg_pos
  85  rw [Cost.Jcost_eq_sq h_arg_ne]
  86  congr 1
  87  ring
  88
  89/-- Quadratic small-`φ_inf` regime: at the reference point the leading
  90behaviour is `V(φ_inf) ≈ φ_inf² / 2`, the canonical slow-roll
  91quadratic-potential form with calibration coefficient `1/2`. -/
  92theorem V_quadratic_at_origin (phi_inf : ℝ) (h : -1 < phi_inf) :
  93    V phi_inf * (2 * (1 + phi_inf)) = phi_inf ^ 2 := by
  94  rw [V_eq_quadratic h]
  95  have h_pos : (0 : ℝ) < 1 + phi_inf := by linarith
  96  have h_ne : (1 : ℝ) + phi_inf ≠ 0 := ne_of_gt h_pos
  97  have h2_ne : (2 : ℝ) * (1 + phi_inf) ≠ 0 := by positivity
  98  field_simp [h_ne, h2_ne]
  99
 100structure InflatonPotentialCert where
 101  vacuum : V 0 = 0
 102  nonneg : ∀ {phi_inf : ℝ}, -1 < phi_inf → 0 ≤ V phi_inf
 103  pos_off_vacuum :
 104    ∀ {phi_inf : ℝ}, phi_inf ≠ 0 → -1 < phi_inf → 0 < V phi_inf
 105  reciprocal_symm :
 106    ∀ {phi_inf : ℝ}, -1 < phi_inf →
 107      V phi_inf = V ((1 + phi_inf)⁻¹ - 1)
 108  quadratic_form :
 109    ∀ {phi_inf : ℝ}, -1 < phi_inf →
 110      V phi_inf = phi_inf ^ 2 / (2 * (1 + phi_inf))
 111
 112/-- Inflaton-potential certificate. -/
 113def inflatonPotentialCert : InflatonPotentialCert where
 114  vacuum := V_vacuum
 115  nonneg := V_nonneg
 116  pos_off_vacuum := V_pos_off_vacuum
 117  reciprocal_symm := V_reciprocal_symm
 118  quadratic_form := V_eq_quadratic
 119
 120end
 121end InflatonPotentialFromJCost
 122end Cosmology
 123end IndisputableMonolith
 124