IsCouplingCombiner
A combiner P from reals to reals counts as a coupling combiner exactly when it fails to factor as separate functions of each argument. The branch selection theorem cites this predicate to force the nonzero parameter in the Recognition Composition Law family and thereby exclude the additive branch. The definition is the direct negation of the SeparatelyAdditive predicate.
claimA function $P : {}$ is a coupling combiner when it is not separately additive, that is, when there do not exist single-argument functions $p, q$ such that $P(u, v) = p(u) + q(v)$ for all real $u, v$.
background
The BranchSelection module works inside the Recognition Composition Law family produced by the Logic_FE rigidity theorem. That family takes the form $F(xy) + F(x/y) = 2F(x) + 2F(y) + c F(x)F(y)$ and attaches the polynomial combiner $P(u, v) = 2u + 2v + c u v$. SeparatelyAdditive P holds when P factors as $p(u) + q(v)$ for some $p, q : {}$. The companion definition interactionDefect records the canonical witness $P(u, v) - P(u, 0) - P(0, v) + P(0, 0)$, which vanishes precisely on the separately additive case.
proof idea
The definition is the direct negation of the SeparatelyAdditive predicate defined earlier in the same module.
why it matters in Recognition Science
This predicate supplies the non-degeneracy condition for the branch selection theorem, which concludes that IsCouplingCombiner applied to the RCLCombiner forces the parameter c nonzero. The result excludes the additive branch (c = 0, representative ½(ln x)²) and selects the bilinear branch whose calibrated representative is J(x) = ½(x + x⁻¹) - 1. It thereby closes the translation theorem by enforcing the strengthened (L4*) coupling requirement from RS_Branch_Selection.tex, isolating J modulo residual α freedom.
formal statement (Lean)
54def IsCouplingCombiner (P : ℝ → ℝ → ℝ) : Prop :=
proof body
Definition body.
55 ¬ SeparatelyAdditive P
56
57/-- The **interaction defect** of a combiner at a pair `(u, v)`:
58\[
59\Delta P(u, v) := P(u, v) - P(u, 0) - P(0, v) + P(0, 0).
60\]
61For a separately additive combiner this is identically zero. The defect
62is the canonical detector of coupling. -/