branchSelectionCert_inhabited
plain-language theorem explainer
The theorem proves that BranchSelectionCert is inhabited, supplying an explicit structure that encodes the equivalences between separate additivity, interaction defect, and coupling for RCL combiners. Researchers formalizing the Logic_FE rigidity theorem and the branch-selection argument in Recognition Science cite it to confirm that the strengthened (L4*) forces the bilinear branch. The proof is a one-line term that directly constructs the certificate from its definition.
Claim. There exists a structure witnessing that, for every combiner $P : ℝ → ℝ → ℝ$, $P$ is separately additive if and only if its interaction defect vanishes identically, $P$ is a coupling combiner if and only if its interaction defect is nonzero for some pair of arguments, and the RCL combiner with parameter $c$ is a coupling combiner if and only if $c ≠ 0$.
background
The module formalizes the structural strengthening of (L4) Composition Consistency introduced in RS_Branch_Selection.tex. A coupling combiner is one that is not separately additive in its arguments; the interaction defect supplies the canonical witness measuring deviation from separate additivity. The RCLCombiner c is the polynomial family $P(u,v) = 2u + 2v + c·u·v$ attached to the Recognition Composition Law. The upstream definition branchSelectionCert assembles the certificate by invoking the three lemmas separatelyAdditive_iff_interactionDefect_zero, isCouplingCombiner_iff_interactionDefect_nonzero, and RCLCombiner_isCoupling_iff.
proof idea
The proof is a one-line term-mode wrapper that applies the constructor of Nonempty to the definition branchSelectionCert. That definition in turn supplies the four fields of the certificate by direct substitution of the three sibling lemmas that establish the equivalences for separate additivity, coupling, and the RCL family.
why it matters
The declaration closes the existence half of the branch-selection argument, confirming that a coupling condition on the combiner isolates the bilinear branch J within the RCL family produced by the translation theorem. It supports the forcing chain by ensuring J-uniqueness (T5) is selected over the additive alternative once (L4) is strengthened to (L4*). The result feeds the isolation of J modulo 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.