BranchSelectionCert
plain-language theorem explainer
BranchSelectionCert packages the five propositions that equate separate additivity of a combiner with vanishing interaction defect, coupling with nonzero defect, and the RCL combiner being coupling precisely when its parameter c is nonzero. A researcher tracing the derivation of the Recognition Composition Law would cite this certificate when applying the strengthened (L4*) condition to exclude the additive branch. The declaration is a structure definition whose fields are assembled directly from the module's equivalence lemmas.
Claim. A BranchSelectionCert is a structure containing: (i) for every combiner $P$, $P$ is separately additive if and only if its interaction defect vanishes for all arguments; (ii) for every combiner $P$, $P$ is a coupling combiner if and only if its interaction defect is nonzero for some pair; (iii) the RCL combiner with parameter $c$ is a coupling combiner if and only if $c ≠ 0$; (iv) if the RCL combiner with parameter $c$ is a coupling combiner then $c ≠ 0$; (v) the RCL combiner with parameter 0 is not a coupling combiner.
background
In this module a combiner $P : ℝ → ℝ → ℝ$ is separately additive when there exist single-argument maps $p,q$ such that $P(u,v) = p(u) + q(v)$ for all $u,v$. The interaction defect is the canonical detector $ΔP(u,v) := P(u,v) - P(u,0) - P(0,v) + P(0,0)$, which vanishes identically precisely on the separately additive combiners. A coupling combiner is defined as one that fails to be separately additive, so its defect is nonzero somewhere. The RCLCombiner $c$ is the explicit polynomial $P(u,v) = 2u + 2v + c·u·v$ attached to the Recognition Composition Law family. The module doc states that the Logic_FE rigidity theorem produces this family, which splits into a bilinear branch ($c ≠ 0$, representative $J(x) = ½(x + x^{-1}) - 1$) and an additive branch ($c = 0$, representative ½(ln x)²); the certificate records the structural strengthening that excludes the additive branch under the coupling requirement.
proof idea
This is a structure definition. Its five fields are populated by direct reference to the sibling lemmas separatelyAdditive_iff_interactionDefect_zero, isCouplingCombiner_iff_interactionDefect_nonzero, and RCLCombiner_isCoupling_iff, together with the two immediate consequences bilinear_branch_forced and additive_branch_excluded.
why it matters
BranchSelectionCert supplies the packaged certificate that the companion paper RS_Branch_Selection.tex uses to strengthen (L4) to (L4*) and thereby force the bilinear branch of the RCL family. It is instantiated by branchSelectionCert and shown inhabited by branchSelectionCert_inhabited. In the Recognition framework this isolates the J function (T5 J-uniqueness) modulo the residual α-coordinate freedom before the eight-tick octave (T7) and spatial dimension (T8) steps are applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.