RCLCombiner_isCoupling_iff
The equivalence shows that the RCL polynomial combiner with parameter c is a coupling combiner precisely when c is nonzero. Branch-selection arguments in the Recognition framework cite it to exclude the additive branch of the composition-law family. The proof rewrites the coupling predicate through the interaction-defect characterization and dispatches both directions by substitution plus a test-point evaluation.
claimLet $P_c(u,v) := 2u + 2v + c uv$. A combiner $P$ is coupling when it is not separately additive. Then $P_c$ is coupling if and only if $c ≠ 0$.
background
The Recognition Composition Law family is $F(xy) + F(x/y) = 2F(x) + 2F(y) + c F(x)F(y)$, realized by the polynomial combiner $P(u,v) = 2u + 2v + c uv$. The module distinguishes the bilinear branch ($c ≠ 0$, representative $J(x) = ½(x + x^{-1}) - 1$) from the additive branch ($c = 0$, representative ½(ln x)²). The strengthened (L4*) requires the combiner to be coupling rather than separately additive, which forces the bilinear branch.
proof idea
The proof rewrites the statement with isCouplingCombiner_iff_interactionDefect_nonzero. The forward direction assumes a pair with nonzero defect, supposes c = 0 for contradiction, substitutes the defect formula interactionDefect_RCLCombiner and obtains zero by ring. The reverse direction applies RCLCombiner_nonzero_couples at the test point (1,1) to exhibit a nonzero defect.
why it matters in Recognition Science
This supplies the central equivalence for the downstream branch_selection theorem, which is the Lean rendering of the branch-selection result in RS_Branch_Selection.tex. It isolates the bilinear representative J of the RCL family, aligning with the J-uniqueness step (T5) of the forcing chain and the Recognition Composition Law. Residual α-coordinate freedom is deferred to separate calibration conditions outside this operator-level statement.
scope and limits
- Does not derive the RCL family itself from Logic_FE.
- Does not select among α-representatives beyond the c ≠ 0 condition.
- Does not incorporate higher-derivative or action-functional constraints.
- Does not compute numerical values for physical constants.
Lean usage
example (c : ℝ) (h : IsCouplingCombiner (RCLCombiner c)) : c ≠ 0 := (RCLCombiner_isCoupling_iff c).mp hformal statement (Lean)
145theorem RCLCombiner_isCoupling_iff (c : ℝ) :
146 IsCouplingCombiner (RCLCombiner c) ↔ c ≠ 0 := by
proof body
Term-mode proof.
147 rw [isCouplingCombiner_iff_interactionDefect_nonzero]
148 constructor
149 · rintro ⟨u, v, huv⟩
150 intro hc
151 apply huv
152 rw [interactionDefect_RCLCombiner, hc]
153 ring
154 · intro hc
155 exact ⟨1, 1, RCLCombiner_nonzero_couples c hc⟩
156
157/-! ## Branch Selection Theorem -/
158
159/-- **Branch selection by non-degeneracy.**
160
161If the RCL polynomial combiner is required to be a coupling combiner
162(the strengthened (L4*) of the companion paper), then the parameter
163`c` is forced to be nonzero. Equivalently, the additive branch
164(`c = 0`, with calibrated representative `½(ln x)²`) is excluded.
165
166This is the branch-selection theorem of `RS_Branch_Selection.tex` in
167its Lean form. The bilinear branch is forced; `J` is the
168`α = 1` representative of the bilinear `α`-family. The residual
169`α`-coordinate freedom is acknowledged in §5 of the paper and is
170addressed by separate generator-calibration / higher-derivative /
171action-functional conditions, none of which are part of the
172operator-level Aristotelian content. -/