Padd_mixed_diff_zero
plain-language theorem explainer
The additive combiner Padd(u,v) = 2u + 2v has vanishing mixed second difference for all real inputs, confirming separability. Researchers formalizing the entanglement gate in Recognition Science cite this to separate the additive counterexample from the RCL combiner. The proof unfolds the definition of Padd and reduces the identity via algebraic normalization.
Claim. For the additive combiner $P(u,v) := 2u + 2v$, the mixed second difference vanishes: $P(u_1,v_1) - P(u_1,v_0) - P(u_0,v_1) + P(u_0,v_0) = 0$ for all $u_0,v_0,u_1,v_1$ in the reals.
background
The Entanglement Gate module requires a combiner P to have nonzero cross-derivative ∂²P/∂u∂v to qualify as entangling, corresponding to an interaction term that couples observations of composite systems. The additive combiner Padd(u,v) = 2u + 2v is defined as the separable counterexample satisfying P(u,v) = α(u) + β(v). This theorem shows its mixed second difference is identically zero, matching the separability property stated in the module doc-comment.
proof idea
The term proof introduces the four real variables, simplifies the expression by unfolding the definition of Padd, and applies the ring tactic to confirm the algebraic cancellation.
why it matters
This result feeds directly into the parent theorem Padd_not_entangling, which concludes that Padd fails to be entangling. It supplies the zero mixed-difference fact needed to contrast the additive combiner against the RCL combiner 2uv + 2u + 2v that carries the nonzero cross term from the Recognition Composition Law. In the foundation layer it helps delineate separable from entangling operations ahead of the eight-tick octave and D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.