IsCouplingCombiner
plain-language theorem explainer
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.
Claim. A 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 2 of 2)
-
Nonlinear heads escape collapse by generating negative curvature
"the pullback metric G(z) = Jh(z)⊤Jh(z) is singular ... v⊤G(z)v = 0 for v in Vaug"
-
Convex minimization yields fast convergence for quantum electrostatics
"The NHL equation... can be proved that it is free from the convergence problems... any gradient descent approach must converge to the unique solution."