separatelyAdditive_of_interactionDefect_zero
If the interaction defect of a combiner P vanishes for every pair of real arguments, then P decomposes as a sum of independent functions of each argument separately. Researchers formalizing the exclusion of the additive branch in the Recognition Composition Law cite this direction of the equivalence. The proof is a direct term-mode construction that exhibits the additive witnesses and verifies the identity by unfolding the defect and applying linear arithmetic.
claimIf $P : ℝ → ℝ → ℝ$ satisfies $ΔP(u,v) = 0$ for all $u,v ∈ ℝ$, where $ΔP(u,v) := P(u,v) - P(u,0) - P(0,v) + P(0,0)$, then there exist functions $p,q : ℝ → ℝ$ such that $P(u,v) = p(u) + q(v)$ for all $u,v ∈ ℝ$.
background
In the Branch Selection module the combiner $P$ is separately additive precisely when it factors through independent single-argument maps, i.e., $P(u,v) = p(u) + q(v)$. This factorization corresponds to the additive branch of the Recognition Composition Law family. The interaction defect $ΔP(u,v) = P(u,v) - P(u,0) - P(0,v) + P(0,0)$ is the canonical obstruction: it vanishes identically exactly when the combiner is separately additive. The local setting is the structural strengthening of composition consistency that requires a coupling combiner (nonzero cross term) to force the bilinear branch over the additive one.
proof idea
The term proof refines the SeparatelyAdditive constructor by supplying the explicit witnesses $p(u) := P(u,0) - P(0,0)$ and $q(v) := P(0,v)$. It then invokes the hypothesis that the defect vanishes at every pair, unfolds the defect definition, and closes the required equality by linear arithmetic.
why it matters in Recognition Science
This supplies the converse half of separatelyAdditive_iff_interactionDefect_zero. That equivalence is invoked by RCLCombiner_isCoupling_iff to show the RCL polynomial combiner is coupling if and only if its parameter $c$ is nonzero. The result therefore closes the branch-selection argument in RS_Branch_Selection.tex, forcing the bilinear $J$-form under the strengthened (L4*) and isolating the $J$-uniqueness step (T5) in the forcing chain.
scope and limits
- Does not prove the converse direction from separate additivity to zero defect.
- Does not quantify or constrain the RCL parameter $c$.
- Does not address physical calibration or units of the combiner.
- Does not extend the statement to non-real domains or higher-arity maps.
formal statement (Lean)
82theorem separatelyAdditive_of_interactionDefect_zero
83 {P : ℝ → ℝ → ℝ} (h : ∀ u v : ℝ, interactionDefect P u v = 0) :
84 SeparatelyAdditive P := by
proof body
Term-mode proof.
85 refine ⟨fun u => P u 0 - P 0 0, fun v => P 0 v, ?_⟩
86 intro u v
87 have h_uv := h u v
88 unfold interactionDefect at h_uv
89 linarith
90
91/-- **Equivalence: separate additivity is identical vanishing of the
92interaction defect.** -/