normalized_implies_G_zero
plain-language theorem explainer
If a cost function F satisfies the normalization condition F(1) = 0, then its log-reparametrized form G_F vanishes at the origin. Workers on the T5 J-uniqueness step in Recognition Science cite this when fixing the zero point before deriving the cosh-add identity. The proof is a direct one-line application of the unit-zero lemma for G.
Claim. Let $F : ℝ → ℝ$ satisfy the normalization condition $F(1) = 0$. Define the log-reparametrization $G_F(t) := F(e^t)$. Then $G_F(0) = 0$.
background
The module supplies helper lemmas for the T5 cost-uniqueness argument. IsNormalized is the proposition $F(1) = 0$. The auxiliary function G reparametrizes any cost function via $G_F(t) := F(e^t)$, converting the multiplicative composition law on F into an additive identity on G. The upstream lemma G_zero_of_unit states that $F(1) = 0$ directly implies $G_F(0) = 0$ by substitution of $t = 0$.
proof idea
The proof is a one-line wrapper that applies the lemma G_zero_of_unit to the given F and the hypothesis hNorm (which supplies $F(1) = 0$).
why it matters
This result anchors the zero point for any normalized cost function before the CoshAddIdentity is imposed, a prerequisite for the T5 forcing step that isolates the unique J-cost. It sits inside the FunctionalEquation helpers that prepare the ground for the eight-tick octave and the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.