Foundation Branch Selection Is Coupling Combiner Iff Interaction Defect Nonzero

The coupling test

A combiner is a rule that takes two numbers and produces a third, like the way a cost of two parts might combine into a cost of the whole. Some combiners are separately additive: they simply add the result of one function of the first input to the result of another function of the second input, so the two inputs never actually interact. Others are coupling: the joint structure matters, and the output depends on how the inputs fit together, not just on each one alone.

The declaration isCouplingCombiner_iff_interactionDefect_nonzero proves a precise equivalence: a combiner is coupling if and only if there exists some pair of inputs where its interaction defect is nonzero. The interaction defect is a simple algebraic quantity, written ΔP(u, v) = P(u, v) − P(u, 0) − P(0, v) + P(0, 0). It measures how much the output at a pair differs from what separate additivity would predict. If the defect vanishes for every pair, the combiner is separately additive; if it is nonzero anywhere, the combiner genuinely couples its inputs. This is a theorem in the framework's machine-checked library of formal theorems.

The result matters because it gives a concrete, computable test for a structural property. Instead of searching for two functions p and q that might decompose a combiner, one simply evaluates the defect at a single pair. For the polynomial family P(u, v) = 2u + 2v + c·u·v, the defect at (u, v) is exactly c·u·v. So the combiner is coupling precisely when c ≠ 0. This is the branch-selection step: requiring coupling forces the parameter c to be nonzero, which excludes the additive branch where c = 0 and the cost would be a pure function of logarithms.

In Recognition Science, this theorem is one link in the chain that selects the bilinear branch of the recognition composition law, leading to the cost function J(x) = ½(x + x⁻¹) − 1. But the theorem itself is narrower: it establishes the equivalence between a structural property (coupling) and an algebraic condition (nonzero defect). It does not by itself decide which branch is physically correct; that requires the additional structural strengthening called coupling, which is a separate premise. The theorem is a tool, not a verdict.

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

What this page does not claim

The theorem does not prove that the bilinear branch is physically correct; it only proves that coupling forces c ≠ 0 within the polynomial family. The theorem does not identify the value of c or the scaling parameter α; those require separate calibration conditions. The theorem does not apply to combiners outside the polynomial RCL family, such as non-polynomial or discontinuous rules.

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: