Prcl_not_separable
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not prove non-separability for any combiner other than Prcl.
- Does not address continuous differentiability or higher-order mixed derivatives.
- Does not quantify entanglement strength or supply a metric on the space of combiners.
- Does not connect the algebraic statement to specific physical measurements or empirical programs.
formal statement (Lean)
91theorem Prcl_not_separable : ¬ IsSeparable Prcl := by
proof body
Tactic-mode proof.
92 intro ⟨α, β, h⟩
93 -- If Prcl(u,v) = α(u) + β(v), then the mixed second difference is 0
94 have hsep : Prcl 1 1 - Prcl 1 0 - Prcl 0 1 + Prcl 0 0 = 0 := by
95 calc Prcl 1 1 - Prcl 1 0 - Prcl 0 1 + Prcl 0 0
96 = (α 1 + β 1) - (α 1 + β 0) - (α 0 + β 1) + (α 0 + β 0) := by
97 simp only [h 1 1, h 1 0, h 0 1, h 0 0]
98 _ = 0 := by ring
99 rw [Prcl_mixed_diff] at hsep
100 norm_num at hsep
101
102/-! ## Separability is Equivalent to Zero Mixed Difference -/
103
104/-- Separable implies zero mixed difference. -/