Fquad_unit0
The quadratic log-cost Fquad evaluates to zero at unity. Researchers constructing counterexamples to weak functional-equation hypotheses cite this normalization to anchor the quadratic case. The proof is a one-line simplification that unfolds the log-lift definition and the explicit quadratic.
claimLet $F(x) := G(1/2, x)$ where $G(t) := t^2/2$. Then $F(1) = 0$.
background
The module records counterexamples showing that existence of some combiner P satisfying F(xy) + F(x/y) = P(F(x), F(y)) does not force the d'Alembert equation on the log-lift of F. Here Fquad is obtained by lifting the quadratic Gquad(t) := t^2/2 through the standard log-lift F_ofLog(G)(x) := G(log x). The same quadratic admits the additive combiner P(u,v) := 2u + 2v, yet the shifted lift H(t) := F(exp t) + 1 fails d'Alembert. Upstream F_ofLog is the canonical composition that turns a function on the additive line into a multiplicative cost.
proof idea
One-line wrapper that applies simp to the definitions of Fquad, Cost.F_ofLog, and Gquad, reducing the claim directly to (log 1)^2/2 = 0.
why it matters in Recognition Science
This lemma supplies the base value for the quadratic counterexample that demonstrates the structural obstruction: mere existence of a combiner P does not imply the Recognition Composition Law or d'Alembert form. It supports the module claim that any derivation of RCL from a weak existence hypothesis requires an additional nondegeneracy axiom. No downstream uses are recorded, but the fact anchors the explicit counterexample used to separate the quadratic case from the hyperbolic J-cost that satisfies T5 uniqueness.
scope and limits
- Does not establish any functional equation satisfied by Fquad.
- Does not address the d'Alembert equation or its failure for the shifted lift.
- Applies only to the specific quadratic Gquad; no generality to other costs.
- Does not connect to phi-ladder, RCL, or physical constants.
formal statement (Lean)
49lemma Fquad_unit0 : Fquad 1 = 0 := by
proof body
One-line wrapper that applies simp.
50 simp [Fquad, Cost.F_ofLog, Gquad]
51