IsEntangling
plain-language theorem explainer
The definition characterizes a combiner from reals to reals as entangling when the mixed second difference fails to vanish at some points. Analysts working on the d'Alembert analytic bridge cite this predicate to distinguish separable additive combiners from interacting ones required by the recognition composition law. It is introduced as a direct existential statement on four real parameters.
Claim. A combiner $P : ℝ → ℝ → ℝ$ is entangling if 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$. This is equivalent to $P$ not being of the form $α(u) + β(v)$.
background
The module formalizes the Entanglement Gate as the requirement that the combiner P has nonzero cross-derivative ∂²P/∂u∂v. From the module documentation: 'Entanglement means: Observing a composite system xy is NOT just the sum of observing x and y separately. There is an interaction term that couples them.' This is precisely the 2uv term in the RCL. The definition captures non-separability via the mixed difference, contrasting with additive combiners. Upstream results supply smoothness as the top natural number infinity and point intervals for numeric checks in related proofs.
proof idea
This declaration is a direct definition. It encodes the negation of separability by requiring the second mixed difference to be nonzero at some quadruple of points.
why it matters
This definition underpins the entanglement gate theorem asserting interaction for Jcost together with the RCL combiner being entangling. It supports the differentiation key lemma connecting entangling combiners to hyperbolic ODEs and the forcing of F to Jcost. In the Recognition framework it realizes the interaction gate that forces J-uniqueness (T5) via the RCL and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.