RCLCombiner
The RCLCombiner supplies the explicit polynomial representative P(u, v) = 2u + 2v + c u v for the combiner in the Recognition Composition Law family. Researchers deriving branch selection from the strengthened composition consistency condition would cite this definition when distinguishing bilinear from additive solutions. The declaration is a direct functional assignment with no lemmas or reductions.
claimThe combiner attached to the Recognition Composition Law family with real parameter $c$ is the function $P(u, v) = 2u + 2v + c u v$.
background
The module formalizes branch selection inside the Recognition Composition Law family produced by the translation theorem of Logic_FE. That family takes the form $F(xy) + F(x/y) = 2F(x) + 2F(y) + c F(x)F(y)$ and splits under calibration into a bilinear branch ($c ≠ 0$, representative $J(x) = ½(x + x^{-1}) - 1$) and an additive branch ($c = 0$, representative ½(ln x)²). The RCLCombiner is the concrete polynomial that realizes the general combiner for any fixed $c$. Upstream structures include the defect functional (equal to J on positive reals) and the LedgerFactorization that calibrates J.
proof idea
Direct definition: the combiner is assigned the expression 2u + 2v + c u v by a single functional clause with no tactic steps or lemma applications.
why it matters in Recognition Science
This definition is the concrete object fed to the branch_selection theorem and the RCLCombiner_isCoupling_iff equivalence. Those results show that the strengthened (L4*) coupling requirement forces c ≠ 0 and thereby selects the bilinear branch with J-uniqueness (T5). The construction sits inside the forcing chain that isolates J modulo residual α freedom and supplies the explicit representative needed for the eight-tick octave and D = 3 derivations downstream.
scope and limits
- Does not derive the value of c or fix the representative J.
- Does not prove uniqueness of the polynomial form among all possible combiners.
- Does not address the additive branch once c is set to zero.
- Does not incorporate empirical calibration data or alpha-band constraints.
formal statement (Lean)
117def RCLCombiner (c : ℝ) : ℝ → ℝ → ℝ :=
proof body
Definition body.
118 fun u v => 2 * u + 2 * v + c * u * v
119
120/-- The interaction defect of the RCL combiner at `(u, v)` is exactly
121`c · u · v`. -/