separatelyAdditive_iff_interactionDefect_zero
Separate additivity of a combiner P is equivalent to its interaction defect vanishing identically for all arguments. Branch selection arguments in the Recognition framework cite this to exclude the additive RCL branch under the coupling requirement. The proof is a direct composition of the two one-directional implications proved earlier in the module.
claimA combiner $P : ℝ → ℝ → ℝ$ is separately additive if and only if its interaction defect vanishes: $P(u,v) - P(u,0) - P(0,v) + P(0,0) = 0$ for all real $u, v$.
background
The BranchSelection module formalizes the argument that the Recognition Composition Law forces the bilinear branch once the combiner is required to be coupling. The RCL family takes the form $F(xy) + F(x/y) = 2F(x) + 2F(y) + c F(x)F(y)$, and the additive branch corresponds to the case $c=0$ where the combiner $P(u,v)=2u+2v$ is separately additive. SeparatelyAdditive P holds when $P(u,v)=p(u)+q(v)$ for single-argument functions p and q. The interaction defect is defined as $ΔP(u,v) := P(u,v) - P(u,0) - P(0,v) + P(0,0)$, which measures the failure of separate additivity. Two upstream theorems in the same module establish the equivalence directions: interactionDefect_eq_zero_of_separatelyAdditive shows that separate additivity implies zero defect, while separatelyAdditive_of_interactionDefect_zero constructs the witness functions p and q from the zero-defect assumption.
proof idea
The proof is a term-mode construction that applies the two directional theorems interactionDefect_eq_zero_of_separatelyAdditive and separatelyAdditive_of_interactionDefect_zero to obtain the biconditional.
why it matters in Recognition Science
This equivalence supplies the key step in branchSelectionCert, which certifies the selection of the bilinear branch under the strengthened composition consistency (L4*). It is invoked by isCouplingCombiner_iff_interactionDefect_nonzero to equate coupling with the existence of nonzero defect. In the Recognition Science framework this closes the argument that the J-uniqueness theorem (T5) selects the bilinear representative $J(x) = (x + x^{-1})/2 - 1$ once the additive branch is excluded by the coupling requirement.
scope and limits
- Does not establish the value of the RCL parameter c.
- Does not verify the defect for the explicit J function.
- Does not address higher-dimensional or non-real combiners.
- Does not prove existence of coupling combiners.
formal statement (Lean)
93theorem separatelyAdditive_iff_interactionDefect_zero
94 (P : ℝ → ℝ → ℝ) :
95 SeparatelyAdditive P ↔ ∀ u v : ℝ, interactionDefect P u v = 0 :=
proof body
Term-mode proof.
96 ⟨interactionDefect_eq_zero_of_separatelyAdditive,
97 separatelyAdditive_of_interactionDefect_zero⟩
98
99/-- **Equivalence: coupling is non-vanishing interaction defect.** -/