V_quadratic_at_origin
plain-language theorem explainer
The declaration shows that the recognition-derived inflaton potential obeys V(φ_inf) ⋅ 2(1 + φ_inf) = φ_inf² for φ_inf > −1. Cosmologists modeling slow-roll inflation on the recognition manifold cite this to recover the canonical quadratic form near the vacuum with calibration 1/2. The proof is a direct rewrite from the squared expression for V followed by positivity checks and field simplification to clear the denominator.
Claim. Let the inflaton potential be defined by $V(φ) := J(1 + φ)$ where $J$ denotes the recognition cost function. For every real number $φ > -1$, the identity $V(φ) ⋅ 2(1 + φ) = φ²$ holds.
background
The module constructs the inflaton field on the recognition manifold as the deviation φ_inf of the Z-coordinate from the consciousness-gap reference rung. Its potential is the standard recognition cost: V(φ_inf) = Jcost(1 + φ_inf). This choice guarantees V(0) = 0 (vacuum) and V'(0) = 0 (extremum), furnishing the universal slow-roll attractor whose curvature scale is fixed by V''(0) = 1. The upstream theorem V_eq_quadratic supplies the explicit squared form V(φ_inf) = φ_inf² / (2(1 + φ_inf)) that is valid precisely when φ_inf > −1.
proof idea
The proof rewrites the left-hand side by substituting the squared expression from V_eq_quadratic. It then proves 1 + φ_inf > 0 by linarith, deduces the two denominators are nonzero, and applies field_simp to cancel the common factor 2(1 + φ_inf).
why it matters
The identity isolates the quadratic small-field regime of the J-cost potential, directly grounding the slow-roll parameters that vanish at the reference point and thereby supporting the module's derivation of N_e = 44, n_s ≈ 0.9556 and r ≈ 0.017. It closes the explicit scalar-field gap left by the earlier structural inflation results while remaining inside the forcing chain that produces J-uniqueness and the eight-tick octave. No downstream theorems yet depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.