G_zero_of_unit
plain-language theorem explainer
If a cost function F satisfies the normalization F(1) = 0, then its log-reparametrized version G_F vanishes at the origin. T5 uniqueness arguments in the Recognition framework cite this when fixing the zero point before invoking the composition law or calibration. The argument is a one-line wrapper that unfolds the definition of G and substitutes the hypothesis.
Claim. Let $F : (0,∞) → ℝ$ satisfy $F(1) = 0$. Define the log reparametrization $G_F(t) := F(e^t)$. Then $G_F(0) = 0$.
background
The module supplies short lemmas that support the T5 cost uniqueness proof. The central definition is the log-coordinate reparametrization G, given explicitly by G(F, t) = F(exp t). This converts multiplicative relations on F into additive relations on G near the origin.
proof idea
One-line wrapper that applies the definition of G. The simpa tactic rewrites G F 0 to F(exp 0) = F(1) and discharges the goal with the supplied hypothesis.
why it matters
The lemma supplies the normalization step that normalized_implies_G_zero and washburn_uniqueness invoke directly. It therefore participates in the T5 J-uniqueness result and in the full_unconditional_inevitability theorem of the DAlembert formulation. The identity is required before the Recognition Composition Law or the eight-tick octave structure can be applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.