interactionDefect_eq_zero_of_separatelyAdditive
plain-language theorem explainer
If a combiner P is separately additive then its interaction defect vanishes for every pair of arguments. Branch selection arguments cite this to identify the additive branch of the RCL family. The proof cases on the witness functions from the hypothesis and reduces the defect expression by four substitutions followed by ring arithmetic.
Claim. If $P : ℝ → ℝ → ℝ$ satisfies $P(u,v) = p(u) + q(v)$ for functions $p,q$ and all real $u,v$, then the interaction defect $P(u,v) - P(u,0) - P(0,v) + P(0,0)$ equals zero for all real $u,v$.
background
The BranchSelection module distinguishes coupling combiners from separately additive ones to select the bilinear branch of the Recognition Composition Law family. SeparatelyAdditive P means there exist $p,q$ such that $P(u,v) = p(u) + q(v)$ for all $u,v$. The interaction defect is the canonical witness: $ΔP(u,v) := P(u,v) - P(u,0) - P(0,v) + P(0,0)$, which the upstream definition states is identically zero precisely for separately additive combiners.
proof idea
The term proof cases on the witness pair from the SeparatelyAdditive hypothesis. It unfolds the defect, substitutes the four argument pairs into the additivity equation, and closes with ring simplification.
why it matters
This direction supplies one half of the equivalence separatelyAdditive_iff_interactionDefect_zero, which characterises coupling combiners. The module uses the equivalence to enforce the strengthened (L4*) that excludes the additive branch and isolates the bilinear representative J. It therefore closes the structural step that forces the phi-ladder and the eight-tick octave in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.