Foundation Branch Selection

Choosing the cost function's branch

In mathematics, a functional equation is an equation where the unknown is a function itself, and often the equation alone leaves several possible functions as answers. The Recognition Composition Law family is one such equation: it asks for a function F satisfying F(xy) + F(x/y) = 2F(x) + 2F(y) + c·F(x)F(y), where c is a real number. The equation splits naturally into two branches: if c is nonzero, the solutions form a bilinear family with representative J(x) = ½(x + x⁻¹) − 1; if c equals zero, the representative solution is ½(ln x)². The equation alone does not say which branch is correct.

The branch selection module in the Recognition Science framework closes this gap by strengthening a structural requirement called composition consistency. The strengthened condition demands that the combiner, the rule that merges two costs into one, must be a coupling combiner: it must not be separately additive in its arguments. A separately additive combiner would have the form P(u, v) = p(u) + q(v), meaning the two inputs contribute independently to the output. The module defines a coupling combiner as one that is not separately additive, and it introduces the interaction defect ΔP(u, v) := P(u, v) − P(u, 0) − P(0, v) + P(0, 0), which measures exactly how much the joint structure of the two arguments matters. A combiner is separately additive precisely when its interaction defect vanishes identically.

For the Recognition Composition Law family, the combiner is the polynomial P(u, v) = 2u + 2v + c·u·v. Its interaction defect at (u, v) is exactly c·u·v. The module proves that this combiner is a coupling combiner if and only if c ≠ 0. Therefore the strengthened condition excludes the additive branch c = 0 outright, leaving the bilinear branch as the only possibility. This is the branch selection theorem: under the coupling requirement, the parameter c is forced to be nonzero, and the additive representative ½(ln x)² is excluded.

In Recognition Science, this result matters because it pins down the cost function J(x) = ½(x + x⁻¹) − 1 as the unique representative of the bilinear branch, up to a residual coordinate freedom that the module explicitly acknowledges. The machine-checked library of formal theorems verifies each step: the equivalence between separate additivity and vanishing interaction defect, the coupling condition for the polynomial combiner, and the final branch selection theorem. The outcome is that a structural requirement, not an arbitrary choice, decides which branch of the functional equation survives.

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

/-- **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 residual α-coordinate freedom in the bilinear branch is resolved by this module. The coupling combiner condition is derived from more basic principles within this module. The branch selection theorem applies to functional equations outside the polynomial RCL 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: