inflatonPotential
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not prove that the potential produces at least 60 e-foldings.
- Does not derive the scalar spectral index from the slow-roll parameters.
- Does not incorporate reheating or the transition to radiation domination.
- Does not address quantum corrections or the initial conditions for the inflaton field.
Lean usage
theorem potential_positive (φ : ℝ) (hφ : φ > 0) (hne : φ ≠ 1) : inflatonPotential φ hφ > 0 := by unfold inflatonPotential; exact Cost.Jcost_pos_of_ne_one φ hφ hneformal statement (Lean)
48noncomputable def inflatonPotential (φ : ℝ) (hφ : φ > 0) : ℝ := Jcost φ
proof body
Definition body.
49
50/-- **THEOREM**: The potential has a minimum at φ = 1. -/