separable_forces_additive
plain-language theorem explainer
If P is separable and obeys the boundary conditions P(a,0) = 2a together with P(0,b) = 2b, then P(u,v) = 2u + 2v for all real u and v. Workers on the analytic bridge from structural axioms to the d'Alembert equation cite the result to close the non-interacting case. The proof is a one-line wrapper that invokes the boundary-additivity lemma.
Claim. Let $P : ℝ × ℝ → ℝ$ be separable. If $P(a,0) = 2a$ for all real $a$ and $P(0,b) = 2b$ for all real $b$, then $P(u,v) = 2u + 2v$ for all real $u,v$.
background
The Analytic Bridge module shows that structural axioms plus interaction force the d'Alembert functional equation on the log-lift H(t) = F(e^t) + 1. Separability of the combiner P encodes the absence of cross terms in the consistency equation G(t+u) + G(t-u) = Q(G(t),G(u)). The supplied boundary conditions fix the normalization so the additive solution matches G(0) = 0 and G'(0) = 0.
proof idea
The proof is a one-line wrapper that applies the boundary-additivity lemma to the separability hypothesis and the two boundary conditions.
why it matters
The lemma supplies the additive case for the downstream theorem separable_combiner_forces_flat, which concludes G'' = 1. It completes one branch of the bridge theorem, showing that consistency plus separability yields the flat ODE while interaction yields the hyperbolic d'Alembert form. This step sits inside the Recognition Science forcing chain that constrains the combiner to either additive or d'Alembert shape.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.