RCLCombiner_nonzero_couples
plain-language theorem explainer
The declaration shows that the RCL combiner with nonzero parameter c produces nonzero interaction defect at the test pair (1,1). Researchers on branch selection between bilinear and additive RCL solutions cite it to enforce the coupling condition. The proof rewrites the defect via the explicit RCL formula and simplifies directly against the nonzero hypothesis.
Claim. Let $P(u,v) = 2u + 2v + c uv$ for $c : ℝ$. If $c ≠ 0$ then the interaction defect satisfies $ΔP(1,1) ≠ 0$, where $ΔP(u,v) := P(u,v) - P(u,0) - P(0,v) + P(0,0)$.
background
The module formalizes selection between branches of the Recognition Composition Law family $F(xy) + F(x/y) = 2F(x) + 2F(y) + c F(x)F(y)$. The RCL combiner is the polynomial $P(u,v) = 2u + 2v + c uv$. The interaction defect of any combiner $P$ at a pair $(u,v)$ is $ΔP(u,v) := P(u,v) - P(u,0) - P(0,v) + P(0,0)$, which vanishes for all pairs precisely when $P$ is separately additive. Upstream lemma interactionDefect_RCLCombiner states that this defect equals $c u v$ for the RCL combiner. The module document notes that a coupling combiner is required by the strengthened (L4*) and that this is equivalent to $c ≠ 0$, thereby excluding the additive branch.
proof idea
The proof is a one-line wrapper that applies interactionDefect_RCLCombiner to reduce the defect at (1,1) to the scalar $c$, then uses simpa to obtain the contradiction with the hypothesis $c ≠ 0$.
why it matters
This result is invoked by the downstream theorem RCLCombiner_isCoupling_iff to obtain the full equivalence 'RCL combiner is coupling iff $c ≠ 0$'. It supplies the concrete witness needed for the branch-selection argument in RS_Branch_Selection.tex, which strengthens composition consistency to force the bilinear branch whose representative is $J(x) = ½(x + x^{-1}) - 1$. In the Recognition Science chain this isolates J-uniqueness (T5) by ruling out the additive solution.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.