interactionDefect_eq_zero_of_separatelyAdditive
plain-language theorem explainer
If a combiner P decomposes as P(u, v) = p(u) + q(v) for single-variable functions p and q, then its interaction defect vanishes for every pair (u, v). Researchers formalizing the branch selection between bilinear and additive forms under strengthened composition consistency cite this direction of the equivalence. The argument extracts the witness functions from the hypothesis, substitutes into the four terms of the defect, and cancels by ring arithmetic.
Claim. If $P : ℝ → ℝ → ℝ$ satisfies $P(u,v) = p(u) + q(v)$ for some $p, q : ℝ → ℝ$, then the interaction defect satisfies $ΔP(u,v) = 0$ for all real $u,v$, where $ΔP(u,v) := P(u,v) - P(u,0) - P(0,v) + P(0,0)$.
background
The BranchSelection module distinguishes coupling combiners from separately additive ones after the Logic_FE rigidity theorem produces the RCL family. SeparatelyAdditive encodes the excluded structure: a combiner factors into independent single-argument contributions. The interaction defect is the canonical detector of coupling, given explicitly as the deviation $P(u,v) - P(u,0) - P(0,v) + P(0,0)$ from that factorization.
proof idea
The term proof rcases the SeparatelyAdditive hypothesis to obtain the witness functions p, q and the equality hP. It then rewrites each of the four terms in the defect expression by hP at the pairs (u,v), (u,0), (0,v), (0,0) and finishes with the ring tactic.
why it matters
This supplies the left-to-right direction of separatelyAdditive_iff_interactionDefect_zero. That equivalence supports RCLCombiner_isCoupling_iff, which states that the RCL polynomial combiner is coupling precisely when its parameter c is nonzero. The result therefore contributes to the structural argument in RS_Branch_Selection.tex that excludes the additive branch under the coupling requirement of (L4*).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.