isCouplingCombiner_iff_interactionDefect_nonzero
plain-language theorem explainer
The equivalence states that a combiner P from reals to reals is a coupling combiner exactly when its interaction defect fails to vanish at some pair of arguments. Workers on the Recognition Science branch selection would invoke this to enforce the bilinear solution to the composition law. The proof proceeds by unfolding the coupling definition, rewriting via the separate-additivity equivalence, and splitting the biconditional with a contradiction argument in one direction.
Claim. A combiner $P : ℝ → ℝ → ℝ$ is a coupling combiner if and only if there exist $u, v ∈ ℝ$ such that the interaction defect $ΔP(u, v) ≠ 0$, where $ΔP(u, v) := P(u, v) - P(u, 0) - P(0, v) + P(0, 0)$.
background
The BranchSelection module develops the structural strengthening of composition consistency that selects the bilinear branch of the Recognition Composition Law family. A combiner is coupling when it is not separately additive, i.e., when the joint dependence on both arguments cannot be reduced to independent contributions. The interaction defect $ΔP(u, v)$ quantifies the failure of separate additivity at the pair $(u, v)$. The upstream equivalence establishes that separate additivity holds precisely when this defect vanishes for all pairs. From the module documentation, the Logic_FE rigidity theorem produces the RCL family with combiner $P(u, v) = 2u + 2v + c · u · v$, and coupling is equivalent to $c ≠ 0$, which excludes the additive branch.
proof idea
The proof first unfolds the definition of coupling as the negation of separate additivity. It then rewrites this using the upstream equivalence between separate additivity and vanishing interaction defect, converting the statement into an equivalence between the negation of universal defect vanishing and the existence of a nonzero defect. Constructor splits the biconditional. The left-to-right direction proceeds by contradiction, assuming the defect vanishes everywhere and deriving that the combiner is separately additive. The right-to-left direction extracts the witness pair and applies the universal quantification.
why it matters
This result is used to populate the branch selection certificate record and is applied directly in the theorem establishing that the RCL combiner is coupling if and only if its parameter is nonzero. It thereby implements the key step in the companion paper that strengthens (L4) to (L4*) and forces the bilinear branch with representative J. The equivalence closes the formalization of the argument that isolates J modulo residual α-coordinate freedom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.