Padd_separable
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.