separatelyAdditive_of_interactionDefect_zero
plain-language theorem explainer
A combiner P on the reals whose interaction defect vanishes identically is separately additive. Branch-selection arguments cite this direction to equate vanishing defect with the additive branch of the RCL family. The term proof builds the witness functions p(u) = P(u,0) - P(0,0) and q(v) = P(0,v), then verifies the decomposition by unfolding the defect and applying linear arithmetic.
Claim. Let $P : ℝ → ℝ → ℝ$. If the interaction defect satisfies $P(u,v) - P(u,0) - P(0,v) + P(0,0) = 0$ for all real $u,v$, then there exist functions $p,q : ℝ → ℝ$ such that $P(u,v) = p(u) + q(v)$ for all $u,v$.
background
The module formalizes the structural distinction between coupling and separately additive combiners that appears in the companion paper RS_Branch_Selection.tex. Separately additive means the combiner factors as the sum of independent functions of each argument; the interaction defect is the canonical obstruction, defined by subtracting the three axis terms from P(u,v). The local setting is the translation of the Logic_FE rigidity theorem into the RCL family, where the polynomial combiner P(u,v) = 2u + 2v + c·u·v splits into bilinear (c ≠ 0) and additive (c = 0) branches; the strengthened composition-consistency axiom (L4*) requires a coupling combiner and thereby excludes the additive branch.
proof idea
Term-mode construction. The proof supplies the pair of witness functions explicitly as p(u) := P(u,0) - P(0,0) and q(v) := P(0,v), then discharges the universal quantifier by introducing u and v, unfolding the interaction-defect hypothesis, and closing with linarith.
why it matters
This direction completes the equivalence separatelyAdditive_iff_interactionDefect_zero, which is the key lemma establishing that the RCL combiner is coupling precisely when c ≠ 0. That equivalence is invoked by the branch-selection theorem that forces the bilinear representative J under the strengthened (L4*). The result therefore sits inside the T5–T6 segment of the forcing chain that isolates the self-similar fixed point modulo the residual α freedom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.