additive_branch_not_coupling
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the explicit calibrated form of J.
- Does not address the residual α-coordinate freedom.
- Does not treat empirical calibration of constants such as α^{-1}.
- Does not extend to non-polynomial combiners outside the RCL family.
formal statement (Lean)
180theorem additive_branch_not_coupling :
181 ¬ IsCouplingCombiner (RCLCombiner 0) := by
proof body
Term-mode proof.
182 intro h
183 exact branch_selection 0 h rfl
184
185/-! ## Headline Certificate -/
186
187/-- **Branch Selection Certificate.**
188
189The structural strengthening of (L4) — coupling, that is, non-additivity —
190forces the bilinear branch within the polynomial RCL family produced by
191the translation theorem of `Logic_Functional_Equation.tex`. -/