BranchSelectionCert
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not derive the RCL family from the functional equation.
- Does not fix the coupling parameter c beyond the condition c ≠ 0.
- Does not address residual α-coordinate freedom inside the bilinear branch.
- Does not prove that J satisfies the original axioms without further calibration.
- Does not extend the selection argument to combiners outside the RCL polynomial family.
formal statement (Lean)
192structure BranchSelectionCert where
193 separately_additive_iff_defect_zero :
194 ∀ P : ℝ → ℝ → ℝ,
195 SeparatelyAdditive P ↔ ∀ u v : ℝ, interactionDefect P u v = 0
196 coupling_iff_defect_nonzero :
197 ∀ P : ℝ → ℝ → ℝ,
198 IsCouplingCombiner P ↔ ∃ u v : ℝ, interactionDefect P u v ≠ 0
199 rcl_coupling_iff :
200 ∀ c : ℝ, IsCouplingCombiner (RCLCombiner c) ↔ c ≠ 0
201 bilinear_branch_forced :
202 ∀ c : ℝ, IsCouplingCombiner (RCLCombiner c) → c ≠ 0
203 additive_branch_excluded :
204 ¬ IsCouplingCombiner (RCLCombiner 0)
205