powerSpectrum
plain-language theorem explainer
The definition supplies the primordial power spectrum P(φ) as V³/(V')² for the J-cost inflaton potential V at positive field values. Cosmologists modeling early-universe perturbations from recognition principles would cite this when deriving scalar spectra in J-cost slow-roll inflation. It is assembled by direct substitution of the inflatonPotential definition together with an explicit slope term.
Claim. The power spectrum $P(φ)$ for $φ > 0$ is $V(φ)^3 / [V'(φ)]^2$ when the slope term is nonzero and 0 otherwise, where $V(φ)$ is the inflaton potential obtained from the J-cost function $J(φ) = (φ + φ^{-1})/2 - 1$.
background
The COS-001 module derives cosmic inflation from J-cost slow roll on the recognition manifold. The J-cost is $J(x) = (x + x^{-1})/2 - 1$, which has a parabolic minimum at $x = 1$ and linear growth far from it; the inflaton is identified with this cost field, so that a flat region produces exponential expansion. Upstream, the inflatonPotential declaration states that the inflaton potential in RS is just the J-cost, with the explicit form $V(φ) := Jcost(φ)$ for $φ > 0$. Supporting V constructions appear in InflatonPotentialFromJCost and SpectralEmergence, while the module itself lists the horizon, flatness, and monopole problems solved by this mechanism.
proof idea
This is a direct definition. It calls inflatonPotential to obtain V, inserts the explicit derivative term Vp = (1 - 1/φ²)/2, and returns the ratio V³/Vp² when Vp is nonzero (otherwise zero).
why it matters
The definition supplies the scalar power spectrum required by FourierOperation in FourierAnalysisFromRS. It completes the COS-001 target of obtaining inflation from J-cost structure and feeds the slow-roll parameters used to obtain n_s ≈ 0.96. Within the framework it sits between the J-uniqueness property and the emergence of spectral features on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.