Foundation Branch Selection Interaction Defect Eq Zero Of Separately Additive

The interaction defect

In mathematics, a function of two variables is separately additive when it can be written as one function of the first variable plus one function of the second: P(u, v) = p(u) + q(v). The function P(u, v) = u + v is separately additive; P(u, v) = u + v + 3uv is not, because the product term mixes the two inputs. The distinction matters whenever a combining rule is meant to describe how two things fit together, since a purely additive rule says the parts never influence each other.

The interaction defect is a number that measures the failure of separate additivity at a pair of inputs. For a combiner P it is defined as ΔP(u, v) = P(u, v) − P(u, 0) − P(0, v) + P(0, 0). The subtraction cancels the one-variable contributions, leaving only the part that depends on both inputs jointly. For a separately additive combiner the defect is identically zero; for the example P(u, v) = u + v + 3uv the defect is exactly 3uv. The converse also holds: if the defect vanishes for every pair, the combiner is separately additive. The theorem interactionDefect_eq_zero_of_separatelyAdditive proves the forward direction, and its companion separatelyAdditive_of_interactionDefect_zero proves the reverse, so the two properties are equivalent.

The Recognition Science framework uses this equivalence to choose between two branches of cost functions. A rigidity theorem produces a family of cost functions F satisfying a composition law with a polynomial combiner P(u, v) = 2u + 2v + c·u·v. The parameter c separates the family: when c = 0 the combiner is separately additive, and when c ≠ 0 it is a coupling combiner, meaning the joint structure of the two arguments enters the output. The framework's strengthened composition consistency requires a coupling combiner, which forces c ≠ 0 and excludes the additive branch with representative ½(ln x)². The theorem branch_selection states this exclusion directly.

In Recognition Science, the declaration interactionDefect_eq_zero_of_separatelyAdditive establishes a structural fact about combiners: if a combining rule is separately additive, its interaction defect vanishes everywhere. It is a pure statement about functions, proved in the framework's machine-checked library of formal theorems. It does not claim that any particular physical combiner is separately additive, nor that the interaction defect must vanish for the cost functions of interest. It does not assert that the additive branch is impossible on its own; that exclusion requires the additional coupling condition from the strengthened composition consistency, which is a separate theorem.

/-- A separately additive combiner has identically vanishing interaction
defect. -/
theorem interactionDefect_eq_zero_of_separatelyAdditive
    {P : ℝ → ℝ → ℝ} (h : SeparatelyAdditive P) :
    ∀ u v : ℝ, interactionDefect P u v = 0 := by
  rcases h with ⟨p, q, hP⟩
  intro u v
  unfold interactionDefect
  rw [hP u v, hP u 0, hP 0 v, hP 0 0]
  ring

/-- Conversely: a combiner whose interaction defect is identically zero is
separately additive. The witness functions are `p(u) := P(u, 0) - P(0, 0)`
and `q(v) := P(0, v)`. -/
theorem separatelyAdditive_of_interactionDefect_zero
    {P : ℝ → ℝ → ℝ} (h : ∀ u v : ℝ, interactionDefect P u v = 0) :
    SeparatelyAdditive P := by
  refine ⟨fun u => P u 0 - P 0 0, fun v => P 0 v, ?_⟩
  intro u v
  have h_uv := h u v
  unfold interactionDefect at h_uv
  linarith

/-- **The RCL combiner is a coupling combiner iff `c ≠ 0`.** -/
theorem RCLCombiner_isCoupling_iff (c : ℝ) :
    IsCouplingCombiner (RCLCombiner c) ↔ c ≠ 0 := by
  rw [isCouplingCombiner_iff_interactionDefect_nonzero]
  constructor
  · rintro ⟨u, v, huv⟩
    intro hc
    apply huv
    rw [interactionDefect_RCLCombiner, hc]
    ring
  · intro hc
    exact ⟨1, 1, RCLCombiner_nonzero_couples c hc⟩

/-- **Branch selection by non-degeneracy.**

If the RCL polynomial combiner is required to be a coupling combiner
(the strengthened (L4*) of the companion paper), then the parameter
`c` is forced to be nonzero. Equivalently, the additive branch
(`c = 0`, with calibrated representative `½(ln x)²`) is excluded.

This is the branch-selection theorem of `RS_Branch_Selection.tex` in
its Lean form. The bilinear branch is forced; `J` is the
`α = 1` representative of the bilinear `α`-family. The residual
`α`-coordinate freedom is acknowledged in §5 of the paper and is
addressed by separate generator-calibration / higher-derivative /
action-functional conditions, none of which are part of the
operator-level Aristotelian content. -/
theorem branch_selection (c : ℝ)
    (hCoupling : IsCouplingCombiner (RCLCombiner c)) :
    c ≠ 0 :=
  (RCLCombiner_isCoupling_iff c).mp hCoupling

What this page does not claim

The interaction defect theorem alone does not force the bilinear branch; the coupling condition is a separate premise. The declaration does not assert that any particular physical combiner is separately additive. The additive branch is not claimed to be impossible without the strengthened composition consistency.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/BranchSelection.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: