pith. sign in
theorem

RCLCombiner_isCoupling_iff

proved
show as:
module
IndisputableMonolith.Foundation.BranchSelection
domain
Foundation
line
145 · github
papers citing
58 papers (below)

plain-language theorem explainer

The equivalence shows that the RCL polynomial combiner with parameter c is a coupling combiner precisely when c is nonzero. Branch-selection arguments in the Recognition framework cite it to exclude the additive branch of the composition-law family. The proof rewrites the coupling predicate through the interaction-defect characterization and dispatches both directions by substitution plus a test-point evaluation.

Claim. Let $P_c(u,v) := 2u + 2v + c uv$. A combiner $P$ is coupling when it is not separately additive. Then $P_c$ is coupling if and only if $c ≠ 0$.

background

The Recognition Composition Law family is $F(xy) + F(x/y) = 2F(x) + 2F(y) + c F(x)F(y)$, realized by the polynomial combiner $P(u,v) = 2u + 2v + c uv$. The module distinguishes the bilinear branch ($c ≠ 0$, representative $J(x) = ½(x + x^{-1}) - 1$) from the additive branch ($c = 0$, representative ½(ln x)²). The strengthened (L4*) requires the combiner to be coupling rather than separately additive, which forces the bilinear branch.

proof idea

The proof rewrites the statement with isCouplingCombiner_iff_interactionDefect_nonzero. The forward direction assumes a pair with nonzero defect, supposes c = 0 for contradiction, substitutes the defect formula interactionDefect_RCLCombiner and obtains zero by ring. The reverse direction applies RCLCombiner_nonzero_couples at the test point (1,1) to exhibit a nonzero defect.

why it matters

This supplies the central equivalence for the downstream branch_selection theorem, which is the Lean rendering of the branch-selection result in RS_Branch_Selection.tex. It isolates the bilinear representative J of the RCL family, aligning with the J-uniqueness step (T5) of the forcing chain and the Recognition Composition Law. Residual α-coordinate freedom is deferred to separate calibration conditions outside this operator-level statement.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.