interactionDefect_RCLCombiner
Algebraic identity shows that the interaction defect of the RCL combiner equals the product c u v. Researchers on Recognition Science branch selection cite it to confirm the bilinear term in the combiner. The term-mode proof unfolds the two definitions and reduces via the ring tactic. This pins the defect exactly to the cross term without additional hypotheses.
claimFor all real numbers $c, u, v$, the interaction defect of the combiner $P(u, v) = 2u + 2v + c u v$ satisfies $P(u, v) - P(u, 0) - P(0, v) + P(0, 0) = c u v$.
background
The Branch Selection module formalizes how the Recognition Composition Law family splits under a strengthened coupling condition. The RCLCombiner with parameter $c$ is the polynomial $P(u, v) = 2u + 2v + c u v$. The interaction defect is the canonical witness for coupling: it extracts the bilinear remainder after subtracting the separate linear contributions in each argument.
proof idea
One-line wrapper that unfolds interactionDefect and RCLCombiner then applies the ring tactic to obtain the identity.
why it matters in Recognition Science
This identity is invoked by RCLCombiner_isCoupling_iff to prove the combiner is coupling precisely when $c ≠ 0$, and by RCLCombiner_nonzero_couples to exhibit a nonzero test point. It supplies the algebraic step that forces the bilinear branch under the strengthened (L4*) Composition Consistency, thereby isolating the J-uniqueness (T5) representative $J(x) = (x + x^{-1})/2 - 1$ from the additive alternative in the forcing chain.
scope and limits
- Does not determine any specific numerical value for the parameter c.
- Does not derive the RCL family from the upstream Logic_FE rigidity theorem.
- Does not address calibration of the residual alpha coordinate.
- Does not extend the identity to combiners with higher-degree terms.
formal statement (Lean)
122theorem interactionDefect_RCLCombiner (c u v : ℝ) :
123 interactionDefect (RCLCombiner c) u v = c * u * v := by
proof body
Term-mode proof.
124 unfold interactionDefect RCLCombiner
125 ring
126
127/-- For `c = 0`, the RCL combiner is the additive combiner
128`P(u, v) = 2u + 2v`, separately additive with `p(u) = 2u` and
129`q(v) = 2v`. -/