entangling_with_boundary_is_RCL
plain-language theorem explainer
Any entangling combiner P that meets the boundary conditions P(u,0)=2u and P(0,v)=2v together with C² smoothness must equal the explicit bilinear form 2uv+2u+2v. Workers on the analytic bridge from consistency equations to d'Alembert's equation cite this to fix the interaction term Q. The argument isolates the interaction piece via boundary rewriting and invokes the mixed-difference identity of the RCL combiner to obtain uniqueness by algebraic closure.
Claim. Let $P:ℝ→ℝ→ℝ$ be entangling (its mixed second difference nonzero at some quadruple) and satisfy the boundary conditions $P(u,0)=2u$ for all $u$ and $P(0,v)=2v$ for all $v$. Assume $P$ is twice continuously differentiable. Then $P(u,v)=2uv+2u+2v$ for all real $u,v$.
background
The Analytic Bridge module shows that structural axioms plus interaction force the d'Alembert equation on the log-lift $H(t)=F(e^t)+1$. IsEntangling declares a combiner non-separable precisely when its mixed second difference fails to vanish identically. The upstream result Prcl_mixed_diff states that the canonical RCL combiner satisfies Prcl(u₁,v₁)-Prcl(u₁,v₀)-Prcl(u₀,v₁)+Prcl(u₀,v₀)=2(u₁-u₀)(v₁-v₀). The local setting is the consistency equation $G(t+u)+G(t-u)=Q(G(t),G(u))$ whose interaction term Q must be constrained by boundary data coming from the J-cost calibration.
proof idea
Decompose $P(u,v)$ by the boundary hypotheses to isolate the interaction term $I(u,v)=P(u,v)-2u-2v$, which vanishes on both axes. Apply the mixed-difference identity from Prcl_mixed_diff to the entangling hypothesis, forcing the cross-derivative to be the constant 2. Integrate the resulting PDE under the zero-boundary conditions on the axes; the unique C² solution is $I(u,v)=2uv$. The tactic proof closes with a linarith step after rewriting the decomposition and invoking the mixed-difference lemma.
why it matters
The result supplies the precise form of the interaction combiner required by the differentiation_key_lemma, which then distinguishes flat ODEs (separable case) from hyperbolic ODEs (entangling case). It realizes the module claim that interaction plus boundary data forces the RCL shape $2ab+2a+2b$, thereby closing the bridge from multiplicative consistency to d'Alembert structure. Within Recognition Science it instantiates the Recognition Composition Law as the unique entangling solution compatible with the J-cost boundary conditions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.