composition_rule_classification
plain-language theorem explainer
Any symmetric real combiner that is right-affine in its second argument, obeys the zero-boundary law f(a,0)=2a, and is normalized by f(1,1)=6 is forced to the Recognition Composition Law polynomial f(a,b)=2(a+1)(b+1)-2. Exclusivity and forcing-chain arguments cite this as Bridge B2 classification. The proof packages the hypotheses into the factorization gate and applies the upstream gate-forces-RCL theorem, then rewrites by ring.
Claim. Let $f:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ be a symmetric composition rule (so $f(a,b)=f(b,a)$). Suppose $f(a,0)=2a$ for all $a$, that for each fixed $a$ the map $b\mapsto f(a,b)$ is affine, and that $f(1,1)=6$. Then for all $a,b$, $$f(a,b)=2(a+1)(b+1)-2.$$
background
In Recognition Science the cost functional $J$ is required to satisfy a composition identity of the form $J(xy)+J(x/y)=f(J(x),J(y))$. A composition rule is exactly such a symmetric binary combiner $f$ on $\mathbb{R}$. The canonical target is the d'Alembert (RCL) rule $f(a,b)=2(a+1)(b+1)-2$, equivalently $2ab+2a+2b$, which is the algebraic content of the Recognition Composition Law.
The module works in the exclusivity/verification layer: rather than assuming associativity of $f$ itself, the honest forcing input is the factorization associativity gate. That gate packages four properties: symmetry, right-affine response in the second slot, the zero-boundary law $P(u,0)=2u$, and the unit-diagonal normalization $P(1,1)=6$. Upstream, gate_forces_rcl already proves that any real binary map satisfying the gate equals the bilinear RCL member $2uv+2u+2v$.
proof idea
Build a FactorizationAssociativityGate instance on $f.f$ by feeding in the structure's symmetry together with the three explicit hypotheses (right-affine family, zero boundary, unit diagonal). For arbitrary $a,b$, apply the upstream theorem gate_forces_rcl to obtain $f.f,a,b=2ab+2a+2b$. Finish with a one-line ring rewrite that expands $2(a+1)(b+1)-2$ to the same bilinear form. No further case analysis is required.
why it matters
This is Bridge B2 in the honest form used by the forcing chain: the RS algebraic closure does not need associativity of the combiner, only the factorization gate already available from the d'Alembert factorization development. It pins the composition rule uniquely to the RCL polynomial under the four gate axioms, which is the algebraic backbone of T5 J-uniqueness and the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. Downstream exclusivity arguments that claim "only RCL survives" can cite this classification rather than re-deriving the bilinear family. The declaration sits at the end of the RCLDerivation module and currently has no further in-repo dependents, so it is a leaf classification lemma ready for the exclusivity narrative.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.