V_eq_quadratic
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.