Prcl_not_separable
plain-language theorem explainer
The RCL combiner P(u,v) = 2uv + 2u + 2v cannot be written as a sum of independent functions of u and of v. Researchers formalizing the Recognition Composition Law in the DAlembert setting cite this to establish the required nonzero cross-derivative. The tactic proof assumes separability, shows the mixed second difference must vanish, then obtains an immediate numerical contradiction with the explicit formula for that difference.
Claim. The combiner defined by $P(u,v) = 2uv + 2u + 2v$ is not separable: there do not exist functions $α,β : ℝ → ℝ$ such that $P(u,v) = α(u) + β(v)$ for all real $u,v$.
background
In the Entanglement Gate module a combiner P is separable precisely when it factors as α(u) + β(v) for some functions α and β. The RCL combiner is the concrete map Prcl(u,v) := 2uv + 2u + 2v. The module treats nonzero mixed second difference as the algebraic signature of entanglement, i.e., the presence of an interaction term that cannot be removed by redefinition of the separate observations.
proof idea
Assume for contradiction that Prcl is separable, so Prcl(u,v) = α(u) + β(v). The mixed second difference at the four points (0,0), (0,1), (1,0), (1,1) then expands to zero by direct substitution and ring arithmetic. The upstream lemma Prcl_mixed_diff supplies the same difference equal to 2, so norm_num produces the contradiction 2 = 0.
why it matters
The result places the RCL combiner on the entangling side of the separability dichotomy that the module uses to characterize the cross-derivative gate. It thereby supplies the algebraic justification for the physical claim that composite observation xy is not the sum of separate observations of x and y. In the larger Recognition Science chain this anchors the RCL as the interaction term that forces the phi-ladder and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.