separatelyAdditive_iff_interactionDefect_zero
plain-language theorem explainer
A combiner P from reals to reals is separately additive exactly when its interaction defect vanishes for every pair of arguments. Workers on the Recognition Composition Law branch selection between bilinear and additive forms cite this equivalence to enforce coupling. The proof is the direct pairing of the two one-way implications already shown for the defect functional.
Claim. A function $P:ℝ→ℝ→ℝ$ satisfies $P(u,v)=p(u)+q(v)$ for some single-argument maps $p,q$ if and only if the interaction defect vanishes identically, where the defect at $(u,v)$ is defined by $ΔP(u,v):=P(u,v)-P(u,0)-P(0,v)+P(0,0)$.
background
The module formalizes the structural distinction between coupling and separately additive combiners inside the Recognition Composition Law family. SeparatelyAdditive P asserts the existence of maps p and q such that P(u,v) equals p(u) plus q(v) for all real u,v; this is the additive branch excluded by the strengthened composition consistency (L4*). The interaction defect is the canonical witness: it subtracts the separate contributions at the axes and returns zero precisely on the separately additive case.
proof idea
Term proof that directly supplies the two directions already proved in the same module: interactionDefect_eq_zero_of_separatelyAdditive and separatelyAdditive_of_interactionDefect_zero.
why it matters
The equivalence supplies one of the three certificates inside branchSelectionCert, which in turn implements the branch-selection argument of RS_Branch_Selection.tex. It isolates the bilinear branch (c≠0, represented by J) by ruling out the additive branch under the coupling requirement. The result sits between the RCL polynomial form and the downstream isCouplingCombiner_iff_interactionDefect_nonzero theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.