interaction_implies_entangling
plain-language theorem explainer
If F satisfies the d'Alembert consistency relation with a combiner P, plus F(1)=0 and inversion symmetry, and F exhibits interaction on some positive pair, then P cannot be separable. Researchers tracing the Recognition Science forcing chain cite this to rule out additive combiners before deriving the hyperbolic ODE for the cost function. The proof proceeds by contradiction: non-entangling forces an additive decomposition of P on the image of F, which collides with the interaction witness via the consistency equation.
Claim. Let $F : (0,∞) → ℝ$ and $P : ℝ → ℝ → ℝ$ satisfy $F(xy) + F(x/y) = P(F(x), F(y))$ for all $x,y > 0$, with $F(1) = 0$ and $F(x) = F(x^{-1})$ for $x > 0$. Suppose $F$ has interaction, i.e., there exist $x,y > 0$ such that $F(xy) + F(x/y) ≠ 2F(x) + 2F(y)$. Then $P$ is entangling: there exist $u_0,v_0,u_1,v_1$ with $P(u_1,v_1) - P(u_1,v_0) - P(u_0,v_1) + P(u_0,v_0) ≠ 0$.
background
The Entanglement Gate module isolates the cross-derivative requirement on any combiner P that respects the functional equation for F. IsEntangling P means the mixed second difference is nonzero somewhere, equivalently (under smoothness) a nonzero ∂²P/∂u∂v. The module contrasts the separable case P(u,v) = 2u + 2v (zero cross term) with the RCL case P(u,v) = 2uv + 2u + 2v (cross term 2), noting that entanglement encodes the coupling between composite and separate observations.
proof idea
Proof by contradiction. Assume ¬IsEntangling P, so the mixed difference vanishes identically. This yields the additive decomposition P(u,v) = P(u,0) + P(0,v) - P(0,0). Boundary evaluations via the consistency relation at y=1 (using mul_one, one_mul) and symmetry give P(u,0) = 2u and P(0,v) = 2v on the image of F, with P(0,0)=0. Hence P(Fx,Fy) = 2Fx + 2Fy. The interaction witness then supplies x,y where the left side of consistency differs from 2Fx + 2Fy, a direct contradiction.
why it matters
This result supplies the first link in the chain that forces F to Jcost: interaction implies entangling P (this theorem), entangling forces the hyperbolic ODE, and the ODE plus initial conditions recover J. It is invoked by F_forced_to_Jcost and Jcost_satisfies_dAlembert in AnalyticBridge, and by interaction_forces_entanglement in TriangulatedProof. Within the framework it closes the step from T5 (J-uniqueness) to the RCL combiner before the eight-tick octave and D=3 emerge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.