Foundation Branch Selection Interaction Defect Rclcombiner

The interaction defect

A combiner is a rule that takes two numbers and returns a third; in Recognition Science it describes how the cost of two recognized events combines into the cost of recognizing them together. The interaction defect is a number computed from a combiner that measures whether the two inputs affect the output independently or jointly. For a combiner P with inputs u and v, the defect is defined as P(u,v) − P(u,0) − P(0,v) + P(0,0). If the combiner is separately additive, meaning it can be written as p(u) + q(v) for some single-argument functions p and q, then this defect is identically zero: the cross terms cancel exactly.

The declaration interactionDefect_RCLCombiner proves a concrete fact about the specific polynomial combiner used in the framework's derivation. That combiner is P(u,v) = 2u + 2v + c·u·v, where c is a real parameter. The theorem states that the interaction defect of this combiner at any pair (u,v) is exactly c·u·v. This is a direct computation, verified by expanding the definition and simplifying with the ring axioms. The result is a machine-checked theorem in the framework's library of formal proofs.

The significance is that the defect is zero only when c = 0. When c is nonzero, the defect is nonzero for any nonzero u and v, which means the combiner is not separately additive: the two inputs genuinely interact. This distinction matters because the framework's derivation produces a family of possible cost functions, and a structural requirement called the coupling condition selects one branch. The theorem RCLCombiner_isCoupling_iff uses this defect computation to prove that the combiner is coupling exactly when c ≠ 0. A companion theorem, branch_selection, then forces the bilinear branch of the solution family, excluding the additive branch where c = 0.

What the declaration does not claim is equally important. It does not determine the value of c; it only shows that c must be nonzero under the coupling requirement. The theorem does not select the representative J(x) = ½(x + x⁻¹) − 1 over other members of the bilinear family; that residual freedom remains acknowledged as open. The declaration also does not establish that the coupling condition itself is physically necessary, only that if it is imposed, the additive branch is excluded.

In the framework's account, this defect computation is the hinge that turns a family of possible cost functions into a specific structural choice. The reader can now see that a single algebraic identity, the defect formula, carries the entire weight of the branch selection. The theorem is a precise, limited claim: it computes a number, and that number distinguishes two cases. Everything beyond that distinction remains explicitly unclaimed.

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

/-- The contrapositive: if `c = 0`, the RCL combiner is not coupling. The
additive branch fails the strengthened (L4*). -/
theorem additive_branch_not_coupling :
    ¬ IsCouplingCombiner (RCLCombiner 0) := by
  intro h
  exact branch_selection 0 h rfl

What this page does not claim

The declaration does not determine the numerical value of c, only that it is nonzero under the coupling requirement. The declaration does not establish that the coupling condition is physically necessary. The declaration does not select J(x) = ½(x + x⁻¹) − 1 over other members of the bilinear family.

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: