Padd_mixed_diff_zero
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not address the RCL combiner or any entangling function.
- Does not extend beyond real numbers or smooth combiners.
- Applies only to the specific linear form Padd and does not treat general separability tests.
- Does not quantify entanglement strength or higher-order interactions.
Lean usage
exact h (Padd_mixed_diff_zero u0 v0 u1 v1)formal statement (Lean)
60theorem Padd_mixed_diff_zero : ∀ u₀ v₀ u₁ v₁ : ℝ,
61 Padd u₁ v₁ - Padd u₁ v₀ - Padd u₀ v₁ + Padd u₀ v₀ = 0 := by
proof body
Term-mode proof.
62 intro u₀ v₀ u₁ v₁
63 simp only [Padd]
64 ring
65
66/-- Padd is not entangling. -/