inflatonPotentialCert
plain-language theorem explainer
The declaration builds the InflatonPotentialCert record by assembling the vacuum value, nonnegativity, strict positivity off vacuum, reciprocal symmetry, and quadratic-form properties of the potential V derived from the J-cost. Cosmologists modeling inflation on the recognition manifold would cite it to certify that the inflaton field satisfies the universal slow-roll conditions at the reference point. The construction is a direct record assignment that pulls in the five supporting theorems for each field.
Claim. The certificate that the inflaton potential satisfies $V(0)=0$, $V(phi_inf)geq 0$ for all $phi_inf>-1$, $V(phi_inf)>0$ whenever $phi_inf neq 0$ and $phi_inf>-1$, the reciprocal symmetry $V(phi_inf)=V((1+phi_inf)^{-1}-1)$, and the quadratic expression $V(phi_inf)=phi_inf^2/(2(1+phi_inf))$ for $phi_inf>-1$.
background
The module defines the inflaton field $phi_inf$ as the deviation of the Z-coordinate from the consciousness-gap reference rung on the recognition manifold. The potential is given by $V(phi_inf)=J(1+phi_inf)$, where J is the Recognition Science cost function obeying the composition law J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y). The structure InflatonPotentialCert packages five properties that any admissible inflaton potential must obey: vacuum energy zero, nonnegativity on the physical domain, strict positivity away from vacuum, invariance under the reciprocal map, and reduction to the quadratic Taylor form near the origin.
proof idea
The definition is a one-line record constructor that directly supplies the five fields of InflatonPotentialCert with the theorems V_vacuum, V_nonneg, V_pos_off_vacuum, V_reciprocal_symm, and V_eq_quadratic. Each of those theorems unfolds V to the underlying J-cost expression and invokes the corresponding Cost lemma (Jcost_unit0, Jcost_nonneg, Jcost_pos_of_ne_one, or Jcost_eq_sq).
why it matters
This definition completes the module's task of writing an explicit scalar potential on the recognition manifold that reproduces the slow-roll attractor and the gap-45 predictions for n_s and r. It sits downstream of the J-uniqueness (T5) and phi fixed-point (T6) steps in the forcing chain and supplies the concrete V needed for any further derivation of cosmological observables from the Recognition Composition Law. No downstream theorems yet reference it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.