G
plain-language theorem explainer
G(t) reparametrizes the J-cost into logarithmic coordinates t = ln(x) to yield the inflaton potential cosh(t) - 1. Alpha-attractor inflation modelers cite this to extract slow-roll parameters from the Recognition Composition Law without external inputs. The definition follows at once from the identity ½(e^t + e^{-t}) = cosh(t) applied to J(e^t).
Claim. Define $G:ℝ→ℝ$ by $G(t):=cosh(t)-1$. This equals the J-cost evaluated at $e^t$, where $J(x)=½(x+x^{-1})-1$.
background
The J-cost is the unique function obeying the Recognition Composition Law J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y) together with the normalization J(1)=0 and J''(1)=1. The module re-expresses this cost in log coordinates via the reparametrization G_F t = F(exp t) from Cost.FunctionalEquation, producing the plateau form with minimum at t=0 and curvature 1 at that point. Upstream results include the cost definition from ObserverForcing.cost and the multiplicative cost from MultiplicativeRecognizerL4.cost; the module doc states that this yields the canonical Starobinsky-style potential with G(0)=0, G'(0)=0 and G''(0)=1.
proof idea
Direct definition. It applies the log reparametrization G_F t = F(exp t) to the J-cost and substitutes the closed-form identity ½(e^t + e^{-t}) = cosh(t).
why it matters
This definition supplies the inflaton potential used by cost_algebra_unique and cost_algebra_unique_aczel in Algebra.CostAlgebra, which establish uniqueness of the cost function under the calibration deriv(deriv(cost∘exp)) 0 =1. It realizes T5 J-uniqueness from the forcing chain and enables the slow-roll derivations in the same module, recovering α=φ² and the spectral index 1-2/N. It supports the zero-parameter status hypothesis in Astrophysics.MassToLight and ObservabilityLimits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.