V_pos_off_vacuum
plain-language theorem explainer
The theorem shows that the inflaton potential V(φ_inf) is strictly positive whenever the displacement φ_inf is nonzero and satisfies -1 < φ_inf. Cosmologists building slow-roll models on the recognition manifold cite it to guarantee a unique vacuum minimum. The proof is a one-line wrapper that unfolds V to Jcost(1 + φ_inf) and invokes the Jcost positivity lemma after linarith confirms the argument lies in (0, ∞) excluding 1.
Claim. Let φ_inf ∈ ℝ satisfy φ_inf ≠ 0 and -1 < φ_inf. Then 0 < V(φ_inf), where V(φ_inf) := J(1 + φ_inf) and J denotes the recognition cost function J(x) = (x + x^{-1})/2 - 1.
background
The module defines the inflaton field φ_inf as the dimensionless deviation of the Z-coordinate from the consciousness-gap reference rung on the recognition manifold. Its potential is given by the sibling definition V(phi_inf : ℝ) := Cost.Jcost(1 + phi_inf), so that V(0) = 0, V'(0) = 0 and V''(0) = 1. The upstream lemma Jcost_pos_of_ne_one states that J(x) > 0 whenever x > 0 and x ≠ 1; the present theorem simply transfers that positivity to V away from the vacuum.
proof idea
The term proof unfolds the definition of V, then applies Cost.Jcost_pos_of_ne_one to the argument (1 + phi_inf). The hypothesis -1 < phi_inf supplies the positivity side via linarith; the hypothesis phi_inf ≠ 0 supplies the inequality to 1, again via linarith on the intro branch.
why it matters
This result supplies the positivity field required by the downstream certificate inflatonPotentialCert, which assembles the full set of vacuum, non-negativity, positivity-off-vacuum, reciprocal-symmetry and quadratic-form properties of V. It thereby anchors the slow-roll analysis (ε_V and η_V vanishing at the reference point) to the Recognition Composition Law and the J-cost positivity that follows from T5 J-uniqueness. The module itself notes that the construction grounds the earlier N_e = 44, n_s ≈ 0.9556 and r ≈ 0.017 predictions in an explicit scalar field.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.