G_zero_of_unit
The lemma shows that any cost function F normalized at unity has its log-reparametrized form G_F vanishing at the origin. Uniqueness proofs for the J-cost in the Recognition Science framework cite this when establishing normalization properties. The argument is a direct one-line wrapper applying the definition of G to the unit hypothesis.
claimIf $F : ℝ → ℝ$ satisfies $F(1) = 0$, then $G_F(0) = 0$, where $G_F(t) := F(e^t)$.
background
This lemma sits in the module of functional equation helpers for the T5 cost uniqueness proof. The central definition is the log-coordinate reparametrization $G_F(t) = F(ℝ.exp t)$. The module states that it supplies lemmas for the T5 cost uniqueness proof. Upstream constants supply the gravitational G and the explicit J-cost form $G(t) = cosh(t) - 1$ in log coordinates.
proof idea
The proof is a one-line wrapper that applies simpa using the definition of G to the hypothesis hUnit.
why it matters in Recognition Science
The lemma is invoked by normalized_implies_G_zero, washburn_uniqueness, washburn_uniqueness_aczel, T5_uniqueness_complete, and the full unconditional inevitability theorems. It supplies the basic normalization step inside the T5 J-uniqueness chain and the Recognition Science forcing sequence from T5 onward.
scope and limits
- Does not prove uniqueness of the J-cost function.
- Does not assume continuity, differentiability, or the composition law.
- Does not address reciprocity or calibration conditions.
- Applies only at the single point t = 0 under the given unit hypothesis.
Lean usage
theorem normalized_implies_G_zero (F : ℝ → ℝ) (hNorm : IsNormalized F) : G F 0 = 0 := G_zero_of_unit F hNormformal statement (Lean)
51lemma G_zero_of_unit (F : ℝ → ℝ) (hUnit : F 1 = 0) : G F 0 = 0 := by
proof body
One-line wrapper that applies simpa.
52 simpa [G] using hUnit
53