Fquad_noInteraction
plain-language theorem explainer
The theorem proves that the quadratic cost fails the non-additivity condition, confirming it lies in the additive branch that does not yield the Recognition Composition Law. Researchers tracing the forcing chain from symmetries to the d'Alembert equation would cite this to separate the flat case from the hyperbolic cost. The argument is a direct contradiction obtained by applying the additivity property of the quadratic cost to the assumed interacting pair.
Claim. $¬ HasInteraction(F_{quad})$, where $HasInteraction(F)$ means there exist positive reals $x,y$ such that $F(xy) + F(x/y) ≠ 2F(x) + 2F(y)$, and $F_{quad}$ is the quadratic-log cost obtained from the quadratic generator via the log-cost map.
background
Module NecessityGates supplies the minimal nondegeneracy conditions needed to force the Recognition Composition Law. The counterexample quadratic cost shows that symmetry plus normalization plus smoothness plus calibration plus some combiner do not suffice. The interaction gate requires existence of a pair whose combined cost deviates from additivity. The quadratic cost is obtained from the quadratic generator via the log-cost map, and its additivity lemma establishes equality under the product and quotient operations for all positive arguments. This is the weakest anti-additive condition, satisfied by the hyperbolic cost but not by the quadratic one.
proof idea
The proof assumes the interaction property for the quadratic cost. This produces positive x and y with the strict inequality on the combined cost. The additivity lemma for the quadratic cost then supplies the matching equality, yielding a contradiction.
why it matters
It is applied in the triangulated proof to show that the quadratic cost is flat and to confirm consistency across all gates. It corresponds to the first gate, which separates the hyperbolic cost from the quadratic one by interaction. In the Recognition Science setting this step rules out the additive branch and supports the transition to the composition law, the eight-tick period, and three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.