interactionDefect
plain-language theorem explainer
The interaction defect of a combiner P at a pair (u, v) is the algebraic remainder that vanishes precisely when P is separately additive. Researchers formalizing branch selection between additive and bilinear solutions of the Recognition Composition Law cite this quantity as the canonical detector of coupling. It is introduced by the direct four-term expression isolating the cross term in P.
Claim. For a combiner function $P : ℝ → ℝ → ℝ$, the interaction defect at the pair $(u, v)$ is the quantity $ΔP(u, v) := P(u, v) - P(u, 0) - P(0, v) + P(0, 0)$.
background
The Branch Selection module formalizes the structural strengthening of composition consistency that requires a coupling combiner rather than a separately additive one. The Recognition Composition Law produces the polynomial family $P(u, v) = 2u + 2v + c · u · v$ for some real $c$. Separate additivity means $P(u, v) = p(u) + q(v)$ for functions $p$ and $q$; the interaction defect is the witness that this decomposition fails, which is equivalent to $c ≠ 0$ and selects the bilinear branch with representative $J(x) = ½(x + x^{-1}) - 1$ over the additive branch.
proof idea
The declaration is a direct definition that computes the four-term remainder $P(u, v) - P(u, 0) - P(0, v) + P(0, 0)$ to isolate any coupling contribution.
why it matters
This definition supplies the witness inside the BranchSelectionCert structure, which encodes the equivalences between separate additivity and vanishing defect together with coupling and nonvanishing defect. It supports the sibling theorems showing that the RCL combiner is coupling precisely when $c ≠ 0$, thereby forcing the bilinear branch. The construction connects to the translation theorem of Logic_FE and isolates $J$ modulo the residual α-coordinate freedom noted in §5 of RS_Branch_Selection.tex.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.