separable_with_boundary_is_additive
plain-language theorem explainer
If a combiner P is separable as alpha(u) plus beta(v) and obeys the boundary conditions P(u,0) equals 2u together with P(0,v) equals 2v, then P equals the additive form 2u plus 2v everywhere. Researchers formalizing the Entanglement Gate cite this to separate the non-interacting case from the RCL entangling combiner. The argument extracts alpha and beta from separability, solves them explicitly via the boundaries using linear arithmetic, and substitutes to reach additivity by ring simplification.
Claim. If $P : ℝ → ℝ → ℝ$ satisfies $P(u,v) = α(u) + β(v)$ for functions $α,β$ and the boundary conditions $P(u,0) = 2u$ for all $u$ together with $P(0,v) = 2v$ for all $v$, then $P(u,v) = 2u + 2v$ for all $u,v$.
background
The Entanglement Gate module characterizes combiners P by their cross-derivative behavior. A combiner is separable precisely when it factors as α(u) + β(v) for some real functions α and β; the additive combiner 2u + 2v is the canonical separable example with vanishing mixed second difference. The RCL combiner 2uv + 2u + 2v supplies the contrasting entangling case whose cross derivative equals 2. Boundary conditions fix the linear terms that appear when one argument vanishes, matching the structure of the Recognition Composition Law.
proof idea
The tactic proof obtains the witnessing functions α and β from the IsSeparable hypothesis. It derives α(u) = 2u - β(0) from the first boundary via rewriting and linarith, then β(v) = 2v - α(0) from the second boundary. Specializing the first expression at u = 0 yields α(0) = -β(0). Substituting these three relations into the separable decomposition and simplifying with ring produces the additive identity.
why it matters
The result is invoked directly by the private lemma separable_forces_additive in AnalyticBridge, which bridges separability to additive structure under the same boundaries. It supplies the concrete step that the separable case with these boundaries collapses exactly to the non-interacting combiner, thereby sharpening the contrast with the entangling RCL form that carries nonzero cross derivative. Within the framework this supports the gate's role in distinguishing interaction from independence, consistent with the eight-tick octave and the requirement that entanglement appear only when the 2uv term is present.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.