Gquad
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.
claimDefine 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 in Recognition Science
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.
scope and limits
- Does not claim that Gquad satisfies the d'Alembert equation.
- Does not derive properties of the combiner P.
- Does not address the hyperbolic G from the RCL.
formal statement (Lean)
39noncomputable def Gquad (t : ℝ) : ℝ := t ^ 2 / 2
proof body
Definition body.
40