BranchSelectionCert
plain-language theorem explainer
BranchSelectionCert packages the equivalences showing that coupling, witnessed by nonzero interaction defect, selects the bilinear RCL branch over the additive one. A researcher formalizing the Recognition Science derivation of J from the composition law would reference it to justify the strengthened (L4*) axiom. The structure is populated directly by the interaction defect lemmas and the RCL parametrization without further deduction.
Claim. A structure asserting: for any combiner $P : ℝ → ℝ → ℝ$, $P$ is separately additive (i.e., $P(u,v) = p(u) + q(v)$ for some $p,q$) 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; the RCL combiner $P_c(u,v) = 2u + 2v + c·u·v$ is coupling if and only if $c ≠ 0$; if $P_c$ is coupling then $c ≠ 0$; and $P_0$ is not coupling.
background
The module formalizes branch selection inside the RCL family produced by the translation theorem on the logic functional equation. A combiner $P$ is separately additive when it factors as $P(u,v) = p(u) + q(v)$ for single-argument maps $p,q$; this is the additive branch with representative ½(ln x)². The interaction defect is defined by ΔP(u,v) := P(u,v) − P(u,0) − P(0,v) + P(0,0) and vanishes for all pairs precisely on the separately additive case, serving as the detector of coupling.
proof idea
This is a structure definition that directly assembles four properties from the interaction defect. It populates the fields using the sibling equivalences separatelyAdditive_iff_interactionDefect_zero, isCouplingCombiner_iff_interactionDefect_nonzero, and RCLCombiner_isCoupling_iff together with the explicit form of RCLCombiner; no tactic steps or additional lemmas are invoked.
why it matters
The certificate supplies the structural content for the branch selection argument of RS_Branch_Selection.tex, which strengthens (L4) to (L4*) by requiring a coupling combiner and thereby excludes the additive branch. It is instantiated by branchSelectionCert and shown inhabited by branchSelectionCert_inhabited, feeding the isolation of J modulo residual α freedom. In the framework it closes the selection between bilinear and additive branches of the RCL family, aligning with T5 J-uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.