RCLCombiner
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.