Fquad_is_flat
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not establish uniqueness of the flat branch among all possible costs.
- Does not derive the explicit closed form of Fquad beyond its definition as F_ofLog Gquad.
- Does not address calibration or the spherical branch.
- Does not connect to physical constants such as alpha or the phi ladder.
formal statement (Lean)
90theorem Fquad_is_flat : ¬ HasInteraction Counterexamples.Fquad := Fquad_noInteraction
proof body
Term-mode proof.
91
92/-! ## Gate 2: Entanglement Characterizes the Combiner -/
93
94/-- RCL combiner is entangling. -/