eFoldings
plain-language theorem explainer
The eFoldings definition supplies the number of inflationary e-foldings N as (φ_start² - φ_end²)/4 for a J-cost potential. Cosmologists working in Recognition Science frameworks would cite it when deriving the 60 e-folds needed to solve the horizon problem. The definition is a direct algebraic reduction from the slow-roll integral approximation ∫ φ dφ.
Claim. The number of e-foldings is given by $N(φ_ start, φ_ end) = (φ_ start² - φ_ end²)/4$.
background
In the Recognition Science treatment of inflation the inflaton is identified with the J-cost field J(x) = (x + x^{-1})/2 - 1, which has a parabolic minimum at x = 1 and linear growth for large x. Module COS-001 derives exponential expansion from slow roll of this J-cost potential, with the nearly constant value acting like a cosmological constant until the field reaches the minimum at φ = 1. Upstream results supply the cost function as the derived cost of a multiplicative recognizer comparator and as the J-cost of a recognition event, together with the from theorem that extracts four structural conditions from seven axioms.
proof idea
The definition is a direct algebraic encoding of the integrated slow-roll formula N ≈ ∫ φ dφ for the linear regime of the J-cost potential, reducing to the difference of squares divided by 4. No lemmas are applied beyond basic real arithmetic.
why it matters
This definition feeds the sixty_efolds theorem that verifies N = 63 when φ starts at 16 and ends at 2, confirming the 60 e-foldings required to solve the horizon, flatness and monopole problems. It realizes the COS-001 target of deriving inflation from J-cost slow roll, consistent with the phi-ladder scaling and eight-tick octave in the broader Recognition Science chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.