Gquad
plain-language theorem explainer
Gquad supplies the quadratic map t maps to t squared over 2 that generates the log-cost counterexample showing an additive combiner satisfies the weak functional equation without forcing d'Alembert structure on the shifted lift. Researchers auditing nondegeneracy conditions in the Recognition Composition Law cite this when testing whether existence of P alone suffices. The definition proceeds by direct one-line assignment of the monomial.
Claim. Define the quadratic function $G:ℝ→ℝ$ by $G(t):=t^2/2$.
background
The counterexamples module establishes that existence of a 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 the quadratic log-cost is F(x):=(log x)^2/2, which admits the additive combiner P(u,v):=2u+2v, yet the shifted lift H(t):=F(exp t)+1 fails d'Alembert. Gquad supplies the underlying G such that F(exp t)=G(t), providing the concrete quadratic instance contrasted with the hyperbolic G of the RCL.
proof idea
The definition is a direct one-line assignment of the monomial t^2/2.
why it matters
Gquad populates the counterexample that feeds Fquad, Fquad_consistency, Fquad_on_exp and curvature_gate_summary. It demonstrates that the RCL forcing chain (T5 J-uniqueness onward) requires nondegeneracy axioms beyond mere existence of P, closing a loophole before deriving the eight-tick octave and D=3. The construction is referenced in downstream lemmas that calibrate derivatives and symmetry for the quadratic case.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.