CompositionRule
plain-language theorem explainer
A composition rule is a symmetric real binary map f that packages how recognition costs combine: J(xy)+J(x/y)=f(J(x),J(y)). Anyone deriving or classifying the Recognition Composition Law cites this carrier type. It is a bare structure (function plus symmetry), not a proved identity.
Claim. A composition rule is a pair $(f,\mathrm{sym})$ where $f:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ is symmetric, $f(a,b)=f(b,a)$ for all $a,b$, and is intended to satisfy $J(xy)+J(x/y)=f(J(x),J(y))$ for a cost $J$ on positive reals.
background
In Recognition Science the cost functional $J$ obeys a two-argument composition identity rather than a plain group law. The Recognition Composition Law (RCL) asserts that the sum of costs of the product and quotient factors through the pair of costs: $J(xy)+J(x/y)=f(J(x),J(y))$ for some fixed binary map $f$.
This module isolates that map as data. Symmetry of $f$ is built in because the left-hand side is invariant under $y\mapsto 1/y$ up to swapping the two $J$-terms, so any honest $f$ must be symmetric. The classical d'Alembert solution is $f(a,b)=2ab+2a+2b$, equivalently $2(a+1)(b+1)-2$, which is exactly the algebraic form forced later in the T5 J-uniqueness chain.
The surrounding exclusivity development treats boundary values such as $f(0,0)=0$ and $f(a,0)=2a$ as theorems deduced from $J(1)=0$ and the composition identity, not as extra structure fields.
proof idea
No proof: this is a structure declaration. It packages a binary real function together with a symmetry axiom. Inhabitants are built by supplying f and a proof of ∀ a b, f a b = f b a (as in the d'Alembert instance, which discharges symmetry by ring).
why it matters
This is the carrier type for Bridge B2 in the exclusivity/RCL derivation. Downstream, composition_rule_f00_eq_zero and composition_rule_f_at_zero derive the boundary laws $f(0,0)=0$ and $f(a,0)=2a$ from any $J$ satisfying the composition identity. composition_rule_classification then forces $f(a,b)=2(a+1)(b+1)-2$ from those boundaries plus right-affinity and the normalization $f(1,1)=6$, which is the honest form of the forcing-chain factorization gate (not associativity of $f$).
associativity_contradicts_boundary shows why the older Open Problem B scaffold was malformed: full associativity of $f$ already contradicts the proved boundary $f(a,0)=2a$. The concrete d'Alembert rule is the canonical inhabitant. Together these close the algebraic side of RCL toward T5 J-uniqueness, $J(x)=(x+x^{-1})/2-1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.