separatelyAdditive_iff_interactionDefect_zero
plain-language theorem explainer
The equivalence states that a combiner P from reals to reals is separately additive precisely when its interaction defect vanishes for every pair of arguments. Branch selection arguments cite it to equate the additive branch of the RCL family with identically zero defect. The proof is a one-line wrapper that invokes the two directional implications already proved for the defect.
Claim. Let $P : ℝ → ℝ → ℝ$. Then $P$ is separately additive (i.e., there exist $p, q : ℝ → ℝ$ such that $P(u,v) = p(u) + q(v)$ for all $u,v$) if and only if the interaction defect $ΔP(u,v) := P(u,v) - P(u,0) - P(0,v) + P(0,0)$ equals zero for all real $u,v$.
background
In the BranchSelection module a combiner $P$ is separately additive when it decomposes as $P(u,v) = p(u) + q(v)$ for single-argument functions $p$ and $q$; this is the structural form excluded from genuine coupling combiners under the strengthened (L4*). The interaction defect is defined by $ΔP(u,v) = P(u,v) - P(u,0) - P(0,v) + P(0,0)$ and serves as the canonical detector of coupling; the upstream theorem interactionDefect_eq_zero_of_separatelyAdditive shows it vanishes for every separately additive $P$, while separatelyAdditive_of_interactionDefect_zero supplies the converse with explicit witnesses $p(u) := P(u,0) - P(0,0)$ and $q(v) := P(0,v)$. The local setting is the RCL family $P(u,v) = 2u + 2v + c·u·v$ produced by the Logic_FE translation theorem, where the additive branch corresponds to $c=0$.
proof idea
The proof is a one-line wrapper that applies interactionDefect_eq_zero_of_separatelyAdditive in the forward direction and separatelyAdditive_of_interactionDefect_zero in the reverse direction.
why it matters
This equivalence populates the separately_additive_iff_defect_zero field of the BranchSelectionCert record, which certifies the full branch-selection argument. It supports the claim that a coupling combiner requirement forces the bilinear branch (with representative $J$) rather than the additive branch, consistent with the forcing chain step T5 that isolates $J$ modulo residual $α$ freedom. The downstream theorem isCouplingCombiner_iff_interactionDefect_nonzero directly rewrites via this result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.