Foundation Branch Selection Additive Branch Not Coupling

The additive branch

A cost function measures the price of recognizing one thing in terms of another. In Recognition Science, the framework's central theorem derives a family of possible cost functions from a few plain conditions. The family splits into two branches. One branch, the bilinear branch, has the representative J(x) = ½(x + x⁻¹) − 1. The other, the additive branch, has the representative ½(ln x)². The translation theorem alone does not choose between them.

The declaration additive_branch_not_coupling settles part of that choice. It proves that the additive branch fails a structural condition called coupling. A combiner is a rule that takes two costs and returns the cost of the composite recognition. The combiner is separately additive when it can be written as P(u, v) = p(u) + q(v), meaning the two arguments enter the output without interacting. A coupling combiner is one that is not separately additive: the joint structure of the two arguments matters, so the cost of a composite genuinely depends on how its components fit together.

The theorem states that the combiner for the additive branch, P(u, v) = 2u + 2v, is not a coupling combiner. Its interaction defect, the quantity ΔP(u, v) = P(u, v) − P(u, 0) − P(0, v) + P(0, 0), is identically zero. A zero interaction defect is exactly the signature of separate additivity. Since the strengthened composition consistency condition requires a coupling combiner, the additive branch is excluded.

In Recognition Science, this is the branch-selection theorem. It forces the bilinear branch, with J(x) = ½(x + x⁻¹) − 1 as the α = 1 representative. The result is a proved theorem in the framework's machine-checked library of formal theorems. It does not, however, fix the remaining α-coordinate freedom within the bilinear family. That residual freedom is addressed by separate generator-calibration, higher-derivative, or action-functional conditions, none of which are part of this declaration.

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

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

/-- **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 declaration does not prove that the additive branch is impossible under all conditions, only under the strengthened coupling requirement. The declaration does not fix the value of α within the bilinear branch. The declaration does not derive the fine-structure constant or any other physical constant.

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: