V_eq_quadratic
V(φ_inf) equals φ_inf² over 2(1 + φ_inf) for φ_inf > -1. Cosmologists using the Recognition manifold to derive slow-roll parameters would cite this to fix the explicit rational form of the inflaton potential. The proof unfolds V to Jcost(1 + φ_inf), applies the squared J-cost identity, and finishes by algebraic normalization.
claimFor real φ_inf > -1, the inflaton potential satisfies V(φ_inf) = φ_inf² / (2(1 + φ_inf)), where V(φ_inf) := J(1 + φ_inf) and J(x) = (x - 1)² / (2x) for x ≠ 0.
background
The module defines the inflaton potential on the recognition manifold by V(φ_inf) := Jcost(1 + φ_inf), with φ_inf the dimensionless displacement from the reference rung. This supplies the scalar field whose Taylor coefficients at zero recover the slow-roll attractor after the gap-45 inflation observables were obtained in the preceding curvature module. The key algebraic tool is the squared expression J(x) = (x - 1)² / (2x) for x ≠ 0, which converts the potential into the stated rational function.
proof idea
The tactic proof unfolds the definition of V, establishes positivity of 1 + φ_inf by linarith from the hypothesis, rewrites with the squared J-cost lemma, then applies congr and ring to equate the two sides.
why it matters in Recognition Science
The identity populates the quadratic_form slot of inflatonPotentialCert, the certificate that assembles vacuum value, non-negativity, positivity off vacuum, and reciprocal symmetry. It thereby grounds the canonical quadratic slow-roll profile V(φ_inf) ≈ φ_inf² / 2 at the reference point, linking the abstract J-cost directly to the n_s and r predictions already derived from the eight-tick octave and gap structure.
scope and limits
- Does not apply for φ_inf ≤ -1 where the J-cost argument ceases to be positive.
- Does not derive the slow-roll parameters ε_V or η_V.
- Does not incorporate loop corrections or multi-field dynamics.
- Does not address the large-field regime beyond the exact rational expression.
Lean usage
rw [V_eq_quadratic h]formal statement (Lean)
80theorem V_eq_quadratic {phi_inf : ℝ} (h : -1 < phi_inf) :
81 V phi_inf = phi_inf ^ 2 / (2 * (1 + phi_inf)) := by
proof body
Tactic-mode proof.
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`. -/