separatelyAdditive_of_interactionDefect_zero
plain-language theorem explainer
A combiner P whose interaction defect vanishes identically for all arguments is separately additive, i.e., admits a decomposition P(u,v) = p(u) + q(v). Researchers formalizing the RCL branch selection cite this direction to equate zero defect with the additive branch. The term proof supplies the explicit witness functions p and q then verifies the identity by unfolding the defect and applying linear arithmetic.
Claim. 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 Branch Selection module introduces SeparatelyAdditive as the property that a combiner P factors into independent single-argument functions. The interaction defect is the canonical obstruction: it equals zero precisely when that factorization holds. These notions distinguish the bilinear branch of the Recognition Composition Law from its additive counterpart under the strengthened composition consistency (L4*).
The module setting requires a coupling combiner, which excludes separate additivity and thereby forces the bilinear representative J. The present theorem supplies the converse half of the equivalence between separate additivity and identically vanishing defect. It rests on the definitions of interactionDefect and SeparatelyAdditive supplied in the same file.
proof idea
The term-mode proof refines the existential quantifier in SeparatelyAdditive by exhibiting the concrete witnesses p(u) := P(u,0) - P(0,0) and q(v) := P(0,v). It then invokes the hypothesis that the defect vanishes, unfolds the defect definition, and closes the required identity with linarith.
why it matters
The result completes the equivalence separatelyAdditive_iff_interactionDefect_zero. That equivalence is the key step showing the RCL combiner is coupling precisely when its parameter c is nonzero, thereby excluding the additive branch under the coupling requirement of (L4*). The module thereby isolates the J representative of the Recognition Composition Law modulo residual α freedom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.