interaction_forces_entanglement
plain-language theorem explainer
If a cost function F obeys the consistency relation F(xy) + F(x/y) = P(F(x), F(y)) for x, y > 0, is normalized by F(1) = 0, symmetric under inversion, and exhibits interaction, then the combiner P must be entangling. Recognition Science researchers cite this to close the interaction-to-entanglement step in the four-gate triangulated proof. The proof is a direct one-line application of the interaction_implies_entangling lemma.
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$. If $F$ has interaction (i.e., $F(xy) + F(x/y) ≠ 2F(x) + 2F(y)$ for some $x,y > 0$), then $P$ is entangling: there exist $u_0,v_0,u_1,v_1$ such that $P(u_1,v_1) - P(u_1,v_0) - P(u_0,v_1) + P(u_0,v_0) ≠ 0$.
background
The TriangulatedProof module assembles four gates to establish inevitability. The Interaction Gate (NecessityGates.HasInteraction) states that F is non-additive if there exist x,y > 0 with F(xy) + F(x/y) ≠ 2F(x) + 2F(y). The Entanglement Gate (EntanglementGate.IsEntangling) declares P entangling when its mixed second difference is nonzero at some point, equivalently not separable as α(u) + β(v).
proof idea
The proof is a one-line wrapper that applies the lemma interaction_implies_entangling from EntanglementGate, forwarding the consistency hypothesis, normalization F(1)=0, symmetry under inversion, and HasInteraction F directly to obtain IsEntangling P.
why it matters
This theorem completes the second gate, forcing the combiner to be entangling once interaction is present. It is invoked by full_inevitability_triangulated to combine all four gates and conclude that F must be J and P the RCL combiner. In the framework it excludes the additive branch, preparing the path to the hyperbolic ODE G'' = G + 1 (CurvatureGate) and d'Alembert structure (FourthGate), consistent with J-uniqueness (T5) and the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.