branchSelectionCert
plain-language theorem explainer
The branchSelectionCert packages the interaction-defect equivalences and the branch-selection theorem into a single certificate asserting that coupling excludes the additive RCL branch. Researchers citing RS_Branch_Selection.tex would invoke it to confirm that the strengthened (L4*) forces the bilinear representative J(x) = ½(x + x^{-1}) - 1. The definition is assembled by direct field assignment of the relevant equivalences and the theorem branch_selection.
Claim. The certificate asserts that for any combiner $P : ℝ → ℝ → ℝ$, $P$ is separately additive if and only if its interaction defect vanishes identically; $P$ is a coupling combiner if and only if the defect is nonzero for some pair of arguments; the RCL combiner with parameter $c$ is coupling precisely when $c ≠ 0$; the bilinear branch is forced under the coupling requirement while the additive branch is excluded.
background
In the BranchSelection module the Recognition Composition Law yields the family of combiners $P(u,v) = 2u + 2v + c·u·v$. The strengthened composition consistency (L4*) requires the combiner to be a coupling combiner, i.e., not separately additive in its arguments. The interaction defect is the canonical witness for non-additivity, and RCLCombiner c attaches the polynomial form to the parameter $c$. Upstream, branch_selection shows that IsCouplingCombiner forces $c ≠ 0$, excluding the additive branch whose calibrated representative is ½(ln x)².
proof idea
The definition constructs the BranchSelectionCert structure by direct assignment of each field: separately_additive_iff_defect_zero receives separatelyAdditive_iff_interactionDefect_zero, coupling_iff_defect_nonzero receives isCouplingCombiner_iff_interactionDefect_nonzero, rcl_coupling_iff receives RCLCombiner_isCoupling_iff, bilinear_branch_forced receives branch_selection, and additive_branch_excluded receives additive_branch_not_coupling. It is a one-line packaging of these results.
why it matters
This definition supplies the headline BranchSelectionCert that witnesses exclusion of the additive branch under the coupling requirement of the strengthened (L4*). It is used by branchSelectionCert_inhabited to establish nonemptiness. In the Recognition framework it completes the selection between the bilinear J and the additive ½(ln x)² branches, isolating the J-uniqueness result (T5) modulo residual α freedom. The module documentation states that together with Logic_FE this isolates J.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.