Jcost_is_hyperbolic
plain-language theorem explainer
The J-cost satisfies the interaction gate: there exist positive x and y such that the product-quotient combination deviates from additivity. Researchers tracing the Recognition Science forcing chain from J-uniqueness to the hyperbolic branch cite this to exclude the flat quadratic case. The proof is a direct one-line term reference to the witness theorem in NecessityGates.
Claim. The cost function $J$ satisfies the interaction property: there exist $x, y > 0$ such that $J(xy) + J(x/y) ≠ 2J(x) + 2J(y)$.
background
The triangulated proof module assembles four gates to reach full inevitability of the J-cost. The interaction gate is defined as HasInteraction F, the proposition that there exist positive x and y with F(xy) + F(x/y) ≠ 2F(x) + 2F(y). This gate excludes the flat branch Fquad. Upstream, Jcost_hasInteraction supplies the concrete witness x = y = 2 and verifies the inequality by direct evaluation of Jcost.
proof idea
One-line term proof that directly applies the theorem Jcost_hasInteraction from NecessityGates.
why it matters
This places J in the hyperbolic branch as the first gate of the triangulated structure, feeding the full inevitability result. It corresponds to the interaction step in the module's four-gate outline and to T5 J-uniqueness in the forcing chain, excluding the flat case before curvature and d'Alembert gates are applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.