additive_branch_not_coupling
plain-language theorem explainer
The RCL combiner with coupling parameter zero fails the coupling condition required by the strengthened composition law. Researchers formalizing branch selection in Recognition Science cite this to exclude the additive branch in favor of the bilinear J-function. The proof is a one-line application of the branch selection theorem at c=0 that produces an immediate contradiction.
Claim. The combiner defined by $P(u,v)=2u+2v$ is not a coupling combiner.
background
The Branch Selection module starts from the Recognition Composition Law family $F(xy)+F(x/y)=2F(x)+2F(y)+c F(x)F(y)$ produced by the translation theorem. The associated polynomial combiner is $P(u,v)=2u+2v+cuv$. A coupling combiner is defined to be one that is not separately additive; its interaction defect is exactly $cuv$, so coupling holds precisely when $c≠0$. The module encodes the structural strengthening of (L4) from the companion paper RS_Branch_Selection.tex, under which the combiner must be coupling.
proof idea
Assume for contradiction that the RCL combiner at parameter zero is coupling. Apply the branch_selection theorem (which states that coupling of the RCL combiner forces the parameter nonzero) at c=0 together with the assumption and reflexivity on the resulting equality 0=0.
why it matters
The result supplies the contrapositive half of the branch selection theorem and is referenced by the BranchSelectionCert structure that packages the coupling criteria. It implements the exclusion of the additive branch (representative ½(ln x)²) required by the strengthened (L4*) in RS_Branch_Selection.tex, thereby isolating the bilinear J-function modulo the residual α-coordinate freedom noted in §5 of that paper.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.