Padd_separable
The theorem shows that the additive combiner Padd(u, v) = 2u + 2v meets the separability condition by exhibiting explicit functions α(u) = 2u and β(v) = 2v. Researchers formalizing the entanglement gate in Recognition Science cite it to separate the zero-interaction baseline from the RCL case. The proof is a direct term construction supplying the witnesses and confirming equality by reflexivity.
claimThe additive combiner $P(u, v) = 2u + 2v$ is separable: there exist functions $α, β : ℝ → ℝ$ such that $P(u, v) = α(u) + β(v)$ for all real $u, v$.
background
The Entanglement Gate module defines a combiner P as separable when it factors as α(u) + β(v) for functions α and β of one variable each. This is the formal negation of nonzero mixed second difference. Padd is the concrete additive example Padd(u, v) := 2u + 2v supplied by the Counterexamples module.
proof idea
The term proof directly constructs the witnessing pair α(u) = 2u, β(v) = 2v. It then applies the universal quantifier introduction over u and v, followed by reflexivity to verify the equality.
why it matters in Recognition Science
This declaration supplies the separable baseline inside the Entanglement Gate module, where the additive combiner is contrasted with the RCL combiner that carries the 2uv interaction term. It supports the module claim that zero cross-derivative corresponds to no interaction under smoothness. The result sits upstream of any later classification of physical combiners but does not yet connect to the phi-ladder or the eight-tick octave.
scope and limits
- Does not prove separability for combiners other than Padd.
- Does not compute or reference the mixed second difference.
- Does not connect to Recognition Science constants or the phi-ladder.
- Does not address quantum entanglement beyond the formal definition.
formal statement (Lean)
54theorem Padd_separable : IsSeparable Padd := by
proof body
Term-mode proof.
55 use fun u => 2 * u, fun v => 2 * v
56 intro u v
57 rfl
58
59/-- The mixed second difference of Padd is zero. -/