Jcost_hasInteraction
plain-language theorem explainer
Jcost satisfies the interaction gate, so there exist positive reals x and y for which the combined cost of the product-quotient pair deviates from additivity in the separate costs. Analysts deriving the Recognition Composition Law from symmetry, normalization and existence of a combiner cite this result to exclude the quadratic-log branch. The proof is a direct term-mode construction that selects the concrete witnesses x = y = 2 and evaluates the inequality by norm_num on the definition of Jcost.
Claim. There exist positive real numbers $x, y$ such that $J(xy) + J(x/y) = 9/8$ while $2J(x) + 2J(y) = 1$, where $J(z) = (z + z^{-1})/2 - 1$.
background
The module NecessityGates supplies the minimal nondegeneracy conditions required once the counterexample in Counterexamples.lean has shown that symmetry, normalization, C² regularity and existence of some combiner P do not yet force the Recognition Composition Law. The interaction gate is defined by HasInteraction F as the existence of x, y > 0 such that F(xy) + F(x/y) ≠ 2F(x) + 2F(y); this rules out the purely additive branch whose logarithmic lift is quadratic. The sibling lemma Fquad_additive together with Fquad_noInteraction establishes that the quadratic candidate Fquad fails the gate, leaving Jcost as the function that passes it.
proof idea
The term proof refines the existential quantifier to the explicit pair x = 2, y = 2 (both positive by norm_num). It then invokes norm_num with the Jcost definition to compute J(4) + J(1) = 9/8 on the left and 2J(2) + 2J(2) = 1 on the right, confirming the required inequality.
why it matters
The theorem is invoked by entanglement_gate_theorem, gates_connected and gates_consistent in the downstream triangulated proof; those results chain interaction to an entangling combiner, hyperbolic curvature and finally the d'Alembert equation. It supplies the weakest anti-quadratic gate that distinguishes the J-branch (T5 J-uniqueness) from the flat additive branch, thereby closing one of the four necessity gates that force the Recognition Composition Law after the counterexample has been ruled out.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.