G_at_zero
G(0) equals zero because the vacuum state corresponds to the fixed point of the J-cost where the argument is unity. Model builders working with alpha-attractor inflation cite the result to confirm that the potential minimum lies at the origin with vanishing energy. The term proof unfolds the definition of G as cosh(t) minus one and reduces via the standard identity cosh(0) equals one.
claim$G(0) = 0$ where $G(t) = J(e^t) = ½(e^t + e^{-t}) - 1 = cosh(t) - 1$ is the inflaton potential obtained by reparametrizing the J-cost in logarithmic coordinates.
background
In the JCostInflaton module the inflaton potential is defined by G(t) := cosh(t) - 1, which equals the J-cost J(e^t) where J(x) = (x + x^{-1})/2 - 1. This reparametrization converts the multiplicative Recognition Composition Law into an additive form on the real line. Upstream results establish that the cost of any recognition event equals its J-cost and that G arises as the log-coordinate version of the functional equation solution.
proof idea
The proof is a term-mode one-liner. It unfolds the definition of G and invokes simp on the lemma Real.cosh_zero to conclude that cosh(0) - 1 equals zero.
why it matters in Recognition Science
This theorem supplies the vacuum_zero_cost field in the master certificate inflation_from_jcost_cert, which asserts that every ingredient of the inflationary chain follows from J-cost uniqueness with zero free parameters. It corresponds to the T5 J-uniqueness step in the forcing chain and anchors the phi-ladder minimum at the vacuum. The result closes the scaffolding for the alpha-attractor identification alpha = phi^2.
scope and limits
- Does not prove that G is nonnegative for nonzero t.
- Does not derive the slow-roll parameters epsilon or eta.
- Does not compute the number of e-folds or spectral index.
- Does not connect the potential to the value of Newton's constant.
Lean usage
vacuum_zero_cost := G_at_zeroformal statement (Lean)
64theorem G_at_zero : G 0 = 0 := by
proof body
Term-mode proof.
65 unfold G; simp [Real.cosh_zero]
66
67/-- G is non-negative: J-cost is always ≥ 0. -/