sixty_efolds
plain-language theorem explainer
The theorem shows that the e-folding count from inflaton value 16 to 2 equals 63 under the J-cost potential approximation. Cosmologists working in Recognition Science would cite it to verify that slow-roll starting near φ=16 supplies the expansion duration needed for horizon and flatness resolution. The proof is a one-line wrapper that substitutes the closed-form expression for N and evaluates it by normalization.
Claim. The e-folding number satisfies $N = (16^2 - 2^2)/4 = 63$, where $N$ approximates the integral of the slow-roll trajectory for the J-cost potential $J(x) = (x + x^{-1})/2 - 1$.
background
The Cosmology.Inflation module derives cosmic inflation from J-cost slow roll. The J-cost $J(x) = (x + x^{-1})/2 - 1$ reaches its global minimum at $x=1$ and grows linearly for large $x$, producing a flat region that drives exponential expansion until the field reaches the minimum. The eFoldings definition supplies the explicit integral approximation $N = (φ_start^2 - φ_end^2)/4$ for this potential.
proof idea
The proof unfolds the eFoldings definition to substitute the quadratic formula, then applies norm_num to reduce (256 - 4)/4 directly to the integer 63.
why it matters
This anchors the inflation calculation by confirming that φ_start ≈ 16 produces N = 63, close to the 60 e-foldings required to solve the horizon problem. It sits downstream of PhiForcingDerived and SpectralEmergence structures that fix the J-cost and discrete geometry, and supplies the numerical input for the horizon_problem_solved, flatness_problem_solved and monopole_problem_solved siblings. The result closes the COS-001 step that links T5 J-uniqueness through the phi-ladder to observable cosmology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.