slowRollEta
plain-language theorem explainer
The second slow-roll parameter is defined as the ratio of the second derivative of the inflaton potential to the potential value itself. Cosmologists studying slow-roll inflation would cite this when deriving the scalar spectral index. The definition extracts the second derivative directly as one over phi cubed and normalizes by the potential with a positivity check.
Claim. $η(φ) = V''(φ)/V(φ)$ for $φ > 0$ if $V(φ) > 0$, and $η(φ) = 0$ otherwise, where $V(φ)$ denotes the inflaton potential obtained from the J-cost function.
background
In the Recognition Science framework, inflation is generated by the slow roll of a scalar field whose potential is the J-cost function J(x) = (x + 1/x)/2 - 1. This potential has a minimum at x = 1 and grows linearly for large x, creating a flat region suitable for inflation at large field values. The second slow-roll parameter η measures the relative curvature of the potential; standard slow-roll conditions require both the first parameter ε and |η| to be much less than one. The module imports the inflatonPotential definition, which sets V(φ) equal to Jcost(φ). Upstream results confirm that the potential is positive away from the minimum.
proof idea
The definition proceeds by binding the inflaton potential to the variable V via the upstream inflatonPotential. It hard-codes the second derivative as 1 over φ to the third power. Division by V occurs only when V is positive; otherwise the result is zero. This implements the mathematical definition of η without additional lemmas.
why it matters
This supplies η to the spectralIndex computation, which produces a value near 0.96 consistent with observations. It also enters the InflatonCert structure that verifies the five inflation regimes and the Fibonacci relation for φ^5. The declaration completes the slow-roll parameter set in the J-cost derivation of inflation, supporting the solution to the horizon and flatness problems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.