Gquad
plain-language theorem explainer
Gquad supplies the explicit quadratic G(t) = t²/2 as the flat-space counterexample inside the curvature gate. Researchers testing the Recognition Composition Law against degenerate geometries cite this definition when building the Fquad family and its consistency lemmas. The declaration is a direct one-line definition with no lemmas or reductions applied.
Claim. The flat curvature case in logarithmic coordinates is defined by the quadratic function $G(t) = t^2 / 2$.
background
The Curvature Gate module distinguishes three constant-curvature possibilities for the cost metric. In log coordinates the line element is ds² = G''(t) dt² where G(t) = F(e^t). The quadratic choice yields zero curvature (independent comparisons), the hyperbolic choice G(t) = cosh(t) - 1 yields negative curvature (entangled comparisons), and the spherical choice is ruled out by non-negativity of F. Upstream, Cost.FunctionalEquation.G supplies the general reparametrization G_F(t) := F(exp t), while Gravity.JCostInflaton.G fixes the hyperbolic solution as the J-cost evaluated at e^t.
proof idea
The declaration is a direct definition Gquad t := t^2 / 2. It is applied unchanged by the downstream lemmas Fquad_on_exp, Fquad_unit0 and Fquad_symm inside the Counterexamples module.
why it matters
Gquad anchors the flat branch of the curvature gate, allowing explicit verification that the quadratic satisfies a weakened additive consistency but violates the full multiplicative Recognition Composition Law. It feeds the family of Fquad lemmas that demonstrate the gate's necessity: only the hyperbolic solution (T5 J-uniqueness and T6 phi fixed point) survives. The definition therefore closes the counterexample path that would otherwise leave the curvature requirement unforced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.