Fquad_is_flat
plain-language theorem explainer
The quadratic-log cost Fquad satisfies the flat branch condition of having no interaction under the product-quotient operation. Researchers tracing the four-gate triangulation in Recognition Science cite this to exclude the flat branch before the entanglement and curvature gates force the hyperbolic solution. The proof is a direct term-mode application of the pre-established no-interaction theorem for this specific Fquad.
Claim. The cost function $F_ {quad}$ defined via $F_{quad} = F_{ofLog} G_{quad}$ satisfies the flat-branch condition: there do not exist $x,y>0$ such that $F_{quad}(xy)+F_{quad}(x/y) ≠ 2F_{quad}(x)+2F_{quad}(y)$.
background
The interaction gate (NecessityGates) declares that a cost function F has interaction precisely when there exist positive x,y with F(xy)+F(x/y) differing from 2F(x)+2F(y). Fquad is the explicit counterexample constructed as Cost.F_ofLog applied to the quadratic Gquad. The TriangulatedProof module assembles the four gates (interaction, entanglement, curvature, d'Alembert) to reach unified inevitability, with the module doc stating that the flat branch is excluded by interaction/entanglement before the hyperbolic ODE is forced.
proof idea
One-line term proof that directly invokes the theorem Fquad_noInteraction from NecessityGates. That upstream result assumes HasInteraction, extracts witnesses x,y, and obtains a contradiction from the additivity identity Fquad_additive.
why it matters
This declaration excludes the flat quadratic branch inside the four-gate triangulation, allowing the proof to advance to the entanglement gate (RCL is entangling) and curvature gate (J satisfies G''=G+1). It feeds the parent result full_inevitability_triangulated by confirming Fquad lies outside the interacting class required for the RCL combiner. The module doc notes that once flat and spherical branches are ruled out, G=cosh-1 follows directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.