rclCombiner
plain-language theorem explainer
The bilinear polynomial P(u,v)=2uv+2u+2v is the canonical right-hand side of the Recognition Composition Law. Anyone proving that a cost composes through a combiner, or that the factorization-associativity gate forces RCL, cites this object as the unique target. It is a three-term arithmetic definition with no proof obligations.
Claim. Define the canonical RCL combiner by $P(u,v) := 2uv + 2u + 2v$ for real $u,v$. This is the unique polynomial that appears on the right-hand side of the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$.
background
The module FactorizationForcing isolates the algebraic core of the B2 closure program. After an analytic step that turns factorization plus three-way compatibility into affinity of the combiner in its second argument, the remaining work is pure algebra: symmetry, the boundary law $P(u,0)=2u$, and the normalization $P(1,1)=6$ force a single polynomial.
That polynomial is the right-hand side of the Recognition Composition Law (RCL). In RS, the cost $J(x)=\frac12(x+x^{-1})-1$ (equivalently $\cosh(\log x)-1$) satisfies $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$ for positive $x,y$. The present definition packages the bilinear expression $2uv+2u+2v$ as a named two-argument map so that gate characterizations and ledger-composition theorems can refer to it uniformly.
Sibling notions in the module include the factorization-associativity gate (a structure of algebraic constraints on a candidate combiner) and the theorems that equate satisfaction of that gate with pointwise equality to this polynomial.
proof idea
Pure definition: the body is the three-term real polynomial $2uv+2u+2v$. No tactics, no lemmas, no hypotheses. Downstream proofs unfold this name and reduce by ring or direct rewriting against the RCL identity for $J$.
why it matters
This is the algebraic fixed point of the composition-law story. Downstream, factorization_gate_iff_rcl states that a map satisfies the full factorization-associativity gate if and only if it equals this combiner pointwise; rclCombiner_satisfies_gate shows the gate holds for it by a short ring calculation.
In the ledger path, jcost_composesThrough_rclCombiner proves $J(xy)+J(x/y)=P(J(x),J(y))$ with $P$ this combiner, so the composition setup is non-vacuous: $J$ is a fixed point of the law it forces. That fact feeds jcost_combinationCostDetermined, the LedgerCompositionCertificate (whose first field equates SatisfiesCompositionLaw with composition through this combiner), and ledgerComposition_forces_jcost.
Framework landmark: RCL itself, and the T5 uniqueness of $J$. The definition is the concrete target that turns "some combiner exists" into "the combiner is exactly RCL," closing the algebraic half of B2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.