Foundation Branch Selection Separately Additive Iff Interaction Defect Zero

The interaction defect

In mathematics, a function of two arguments is called separately additive when it can be written as the sum of two single-argument functions: P(u, v) = p(u) + q(v). The two inputs contribute independently; changing u does not change how v enters the output. Many natural operations, such as vector addition or multiplication by a constant, have this shape. The question of whether a given rule has this shape arises whenever a composite quantity is built from components.

There is a direct test. Define the interaction defect of a two-argument function P at a pair (u, v) as ΔP(u, v) = P(u, v) − P(u, 0) − P(0, v) + P(0, 0). This expression measures how much the joint effect of u and v differs from the sum of their individual effects. For a separately additive function, the defect is identically zero. The converse also holds: if the defect vanishes for every pair, the function is separately additive. This equivalence, that separate additivity is exactly identical vanishing of the interaction defect, is a proved theorem in the machine-checked library of formal theorems of the Recognition Science framework. It is a purely structural statement about real-valued functions of two real variables.

The framework's interest in this test comes from a larger argument about the cost of recognition, the framework's term for the forced expense of recording an event in a discrete ledger. A prior theorem produces a family of possible cost functions, each attached to a polynomial combiner P(u, v) = 2u + 2v + c·u·v, where c is a real parameter. The family splits into two branches: a bilinear branch with c ≠ 0, whose representative is J(x) = ½(x + x⁻¹) − 1, and an additive branch with c = 0, whose representative is ½(ln x)². The framework's translation theorem alone does not choose between them.

In Recognition Science, the strengthened requirement is that the combiner must be a coupling combiner, meaning it is not separately additive. The interaction defect provides the canonical detector: a combiner is coupling exactly when the defect is nonzero somewhere. For the polynomial combiner above, the defect at (u, v) is exactly c·u·v. Hence the combiner is coupling if and only if c ≠ 0. The branch-selection theorem then follows: requiring coupling forces c ≠ 0, which excludes the additive branch and forces the bilinear branch. The framework proves this selection within its formal library, leaving only a residual freedom in the parameter α that is addressed by separate conditions outside the operator-level content.

What this declaration does not claim is narrower than it might appear. It does not prove that the bilinear branch is the only possible cost function; it proves that within the polynomial family, the coupling requirement excludes the additive branch. It does not establish that the interaction defect is the only way to detect coupling, only that it is a canonical one. And it does not claim that the physical recognition-to-linking bridge, which would connect this formal structure to three-dimensional space, is closed; that bridge remains open.

/-- **Equivalence: separate additivity is identical vanishing of the
interaction defect.** -/
theorem separatelyAdditive_iff_interactionDefect_zero
    (P : ℝ → ℝ → ℝ) :
    SeparatelyAdditive P ↔ ∀ u v : ℝ, interactionDefect P u v = 0 :=
  ⟨interactionDefect_eq_zero_of_separatelyAdditive,
   separatelyAdditive_of_interactionDefect_zero⟩

/-- **Equivalence: coupling is non-vanishing interaction defect.** -/
theorem isCouplingCombiner_iff_interactionDefect_nonzero
    (P : ℝ → ℝ → ℝ) :
    IsCouplingCombiner P ↔ ∃ u v : ℝ, interactionDefect P u v ≠ 0 := by
  unfold IsCouplingCombiner
  rw [separatelyAdditive_iff_interactionDefect_zero]
  constructor
  · intro h
    by_contra hno
    push_neg at hno
    exact h hno
  · rintro ⟨u, v, huv⟩ hall
    exact huv (hall u v)

/-- The interaction defect of the RCL combiner at `(u, v)` is exactly
`c · u · v`. -/
theorem interactionDefect_RCLCombiner (c u v : ℝ) :
    interactionDefect (RCLCombiner c) u v = c * u * v := by
  unfold interactionDefect RCLCombiner
  ring

/-- **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

This declaration does not prove that the bilinear branch is the only possible cost function; it proves that within the polynomial family, coupling excludes the additive branch. This declaration does not establish that the interaction defect is the only way to detect coupling, only that it is a canonical one. This declaration does not claim that the physical recognition-to-linking bridge to three-dimensional space is closed; that bridge remains open.

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: