G_pos_of_ne_zero
plain-language theorem explainer
The declaration shows that the inflaton potential G(t) exceeds zero for every nonzero real t, confirming the vacuum at t=0 as the unique root. Cosmologists deriving slow-roll parameters from the J-cost would cite this to guarantee a single minimum in the plateau potential. The proof is a one-line wrapper that unfolds G and applies the known strict inequality for cosh together with linear arithmetic.
Claim. Let $G(t) = 1 - 1 = 1 - 1$. Then for any real $t$ with $t ≠ 0$, $G(t) > 0$.
background
The module treats the Recognition Composition Law as the source of the inflaton potential. In log coordinates t = ln(x) the J-cost becomes the function G(t) = cosh(t) - 1, which is exactly the Starobinsky-style plateau with a minimum at the origin. The module doc states that G(0) = 0, G'(0) = 0 and G''(0) = 1, recovering the calibration constant A3 and the α-attractor form α = φ². Upstream results supply the original J-cost definition and the reparametrization G_F t = F(exp t) that converts the multiplicative functional equation into the additive cosh form.
proof idea
The proof unfolds the definition of G to obtain cosh(t) - 1. It then invokes the lemma Real.one_lt_cosh.mpr on the hypothesis t ≠ 0 to obtain the strict inequality 1 < cosh(t). Linear arithmetic finishes the argument that cosh(t) - 1 > 0.
why it matters
The result secures uniqueness of the vacuum for the J-cost inflaton, which is required before the module can derive the slow-roll parameters ε = (tanh t)² / 2 and η = 1 / cosh(t) that appear in the later declarations. It directly supports the chain step that converts the Recognition Composition Law into a concrete potential whose curvature yields the spectral index 1 - 2/N. The construction sits inside the T5 J-uniqueness forcing that produces the phi-ladder and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.