gates_equivalent_for_Jcost
plain-language theorem explainer
Jcost satisfies the interaction gate exactly when there exists an entangling combiner P reproducing the product-quotient addition rule. Researchers tracing the Recognition Science forcing chain cite this to confirm the hyperbolic branch is selected by the first two gates. The proof is a direct iff construction exhibiting the RCL combiner forward and invoking the known interaction witness backward.
Claim. Let $J$ be the J-cost function. Then $J$ has interaction (there exist $x,y>0$ such that $J(xy)+J(x/y)≠2J(x)+2J(y)$) if and only if there exists $P:ℝ→ℝ→ℝ$ such that for all $x,y>0$, $J(xy)+J(x/y)=P(J(x),J(y))$ and the mixed second difference of $P$ is nonzero at some point.
background
HasInteraction F asserts non-additivity: there exist positive x,y with F(xy)+F(x/y)≠2F(x)+2F(y). IsEntangling P requires the mixed second difference P(u1,v1)-P(u1,v0)-P(u0,v1)+P(u0,v0)≠0 at some quadruple, equivalently that P is not separable as α(u)+β(v). The RCL combiner is Prcl(u,v)=2uv+2u+2v, whose mixed difference equals 2(u1-u0)(v1-v0) and is therefore nonzero when the increments differ. This theorem belongs to the triangulated proof module that unifies the interaction, entanglement, curvature, and d'Alembert gates; the module doc states that once interaction and entanglement exclude the flat branch, the solution is forced to G=cosh-1.
proof idea
The term proof applies the iff constructor. Forward: introduce Prcl, refine with Prcl_entangling, invoke J_computes_P to obtain the functional equation, then close by linarith after unfolding Prcl. Reverse: apply Jcost_hasInteraction directly.
why it matters
The result closes the interaction-entanglement pair in the triangulated proof, showing that Jcost interaction forces the combiner to be the entangling RCL and thereby distinguishes J from Fquad. It feeds the full inevitability theorem listed among sibling declarations and aligns with the J-uniqueness step (T5) and Recognition Composition Law in the forcing chain. The module doc notes that this gate pair plus calibration yields G=cosh-1, consistent with the eight-tick octave and D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.