branchSelectionCert
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive a specific nonzero value for the RCL parameter c.
- Does not address the residual α-coordinate freedom within the bilinear branch.
- Does not prove existence of a coupling combiner from first principles.
- Does not extend the selection argument beyond the polynomial RCL family.
Lean usage
theorem branchSelectionCert_inhabited : Nonempty BranchSelectionCert := ⟨branchSelectionCert⟩formal statement (Lean)
206def branchSelectionCert : BranchSelectionCert where
207 separately_additive_iff_defect_zero :=
proof body
Definition body.
208 fun P => separatelyAdditive_iff_interactionDefect_zero P
209 coupling_iff_defect_nonzero :=
210 fun P => isCouplingCombiner_iff_interactionDefect_nonzero P
211 rcl_coupling_iff := RCLCombiner_isCoupling_iff
212 bilinear_branch_forced := branch_selection
213 additive_branch_excluded := additive_branch_not_coupling
214