interactionDefect_eq_zero_of_separatelyAdditive
If a combiner P admits functions p and q such that P(u, v) equals p(u) plus q(v) for all real arguments, then the interaction defect of P vanishes identically. This direction is cited inside the equivalence that characterises coupling combiners and thereby selects the bilinear branch of the Recognition Composition Law over the additive branch. The argument extracts the additive witnesses, substitutes them into the four terms of the defect, and cancels by ring arithmetic.
claimIf $P : ℝ → ℝ → ℝ$ satisfies $P(u,v) = p(u) + q(v)$ for some $p, q : ℝ → ℝ$ and all real $u, v$, then $P(u,v) - P(u,0) - P(0,v) + P(0,0) = 0$ for all real $u, v$.
background
The Branch Selection module isolates the bilinear branch of the Recognition Composition Law family by requiring a coupling combiner, i.e., one that is not separately additive. SeparatelyAdditive P is the proposition that there exist single-argument functions p and q with P(u, v) = p(u) + q(v) for every pair of reals. The interaction defect is the canonical detector of coupling, given by the expression P(u, v) minus P(u, 0) minus P(0, v) plus P(0, 0). This lemma supplies the forward half of the equivalence separatelyAdditive_iff_interactionDefect_zero.
proof idea
The term proof first rcases the SeparatelyAdditive hypothesis to obtain the witness functions p, q and the equality hP. It then introduces arbitrary u and v, unfolds interactionDefect, rewrites each of the four summands via hP at the points (u, v), (u, 0), (0, v) and (0, 0), and finishes with the ring tactic.
why it matters in Recognition Science
The result supplies one direction of the equivalence that characterises coupling combiners as those with nonzero interaction defect. It is invoked by separatelyAdditive_iff_interactionDefect_zero, which in turn supports RCLCombiner_isCoupling_iff showing that the RCL combiner is coupling precisely when the parameter c is nonzero. This forces the bilinear branch with representative J, as required by the strengthened Composition Consistency (L4*) in RS_Branch_Selection.tex.
scope and limits
- Does not prove the converse that vanishing defect implies separate additivity.
- Does not fix the numerical value of the RCL parameter c.
- Does not extend the statement to combiners with more than two arguments.
- Does not invoke the Recognition Composition Law itself.
formal statement (Lean)
70theorem interactionDefect_eq_zero_of_separatelyAdditive
71 {P : ℝ → ℝ → ℝ} (h : SeparatelyAdditive P) :
72 ∀ u v : ℝ, interactionDefect P u v = 0 := by
proof body
Term-mode proof.
73 rcases h with ⟨p, q, hP⟩
74 intro u v
75 unfold interactionDefect
76 rw [hP u v, hP u 0, hP 0 v, hP 0 0]
77 ring
78
79/-- Conversely: a combiner whose interaction defect is identically zero is
80separately additive. The witness functions are `p(u) := P(u, 0) - P(0, 0)`
81and `q(v) := P(0, v)`. -/