`V`

definition

show as: view math explainer →

module: IndisputableMonolith.Cosmology.InflatonPotentialFromJCost
domain: Cosmology
line: 44 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Cosmology.InflatonPotentialFromJCost on GitHub at line 44.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  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]

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.