G_zero
plain-language theorem explainer
Normalization F(1) = 0 on a cost function forces its log-lift to vanish at the origin. Analysts of the d'Alembert consistency bridge cite this to anchor the combiner at zero arguments. The argument is a direct substitution from the definition of the log-lift together with exp 0 = 1.
Claim. Let $F : ℝ → ℝ$ satisfy $F(1) = 0$. The log-lift $G(t) := F(e^t)$ then obeys $G(0) = 0$.
background
The Analytic Bridge module proves that structural axioms on a cost function together with an interaction combiner force the d'Alembert functional equation. The log-lift is defined by G_of F (t) := F(exp t), converting the multiplicative consistency equation on F into an additive equation on G. Upstream results include the identical reparametrization in Cost.FunctionalEquation.G and the J-cost evaluation G(t) = cosh(t) - 1 in Gravity.JCostInflaton.
proof idea
The proof is a one-line term-mode simplification that unfolds the definition of G_of, substitutes Real.exp 0 = 1, and applies the normalization hypothesis F 1 = 0.
why it matters
G_zero supplies the boundary value used by Q_boundary_v to obtain P(a, 0) = 2a and by Q_boundary_u for the symmetric case. It forms the initial normalization step in the Bridge Theorem strategy before interaction forces the hyperbolic ODE G'' = G + 1 and the uniqueness result F_forced_to_Jcost. The result closes the normalization anchor prior to deriving the J-cost form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.