inflatonPotential
plain-language theorem explainer
The inflaton potential is identified with the J-cost function J(φ) for φ > 0. Cosmologists modeling early-universe expansion inside Recognition Science would cite this identification when computing slow-roll parameters from the recognition composition law. The definition is a direct alias to the Jcost primitive with no further reduction.
Claim. The inflaton potential $V(φ)$ for $φ > 0$ is given by $V(φ) = J(φ)$, where $J(φ) = (φ + φ^{-1})/2 - 1$.
background
The Cosmology.Inflation module derives cosmic inflation from J-cost slow roll. The J-cost is the function $J(x) = (x + x^{-1})/2 - 1$, which satisfies the recognition composition law $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$ and attains its global minimum of zero at $x = 1$. Near the minimum the potential is parabolic; far away it grows linearly, producing a flat region suitable for slow roll.
proof idea
One-line definition that directly aliases the Jcost function imported from the Cost module.
why it matters
This supplies the potential $V(φ)$ used by the downstream theorems potential_min_at_one, potential_positive, slowRollEpsilon, slowRollEta and powerSpectrum. It realizes the module claim that inflation emerges from J-cost slow roll and thereby addresses the horizon, flatness and monopole problems. The construction sits inside the T5 J-uniqueness step of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.