associativity_contradicts_boundary
plain-language theorem explainer
No symmetric real combiner f for compound J-costs can be associative once it obeys f(0,0)=0 and the boundary f(a,0)=2a. Auditors of the RCL forcing chain and the old Open Problem B scaffold cite this as the inconsistency that kills the associativity-only closure. The proof evaluates associativity at (0,0,1) and obtains 2=4.
Claim. Let $f:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ be symmetric. If $f(0,0)=0$, $f(a,0)=2a$ for all $a\in\mathbb{R}$, and $f$ is associative, then a contradiction follows.
background
In Recognition Science the Recognition Composition Law packages how the J-cost of products and quotients recombines: $J(xy)+J(x/y)=f(J(x),J(y))$ for a binary combiner $f$. A composition rule is exactly such an $f$, required only to be symmetric on $\mathbb{R}$. The d'Alembert (RCL) polynomial is $f(a,b)=2ab+2a+2b$, equivalently $2(a+1)(b+1)-2$.
That polynomial satisfies the zero-boundary $f(a,0)=2a$ and $f(0,0)=0$, but is not associative. Earlier scaffolding treated associativity of $f$ itself as a candidate closure axiom (Open Problem B / Bridge B2). This module lives in the exclusivity verification layer that classifies which combiners are admissible for the forcing chain.
proof idea
Symmetry plus the boundary give $f(0,1)=f(1,0)=2\cdot 1=2$ and $f(0,2)=4$. Associativity at the triple $(0,0,1)$ reads $f(f(0,0),1)=f(0,f(0,1))$. Substituting $f(0,0)=0$ and $f(0,1)=2$ yields $f(0,1)=f(0,2)$, i.e. $2=4$. Linear arithmetic finishes. No external lemmas beyond the structure's symmetry field and the three hypotheses are used.
why it matters
The theorem shows the associativity-only formulation of Bridge B2 was malformed: it is inconsistent with the already-proved boundary law $f(a,0)=2a$. The module records what the RS algebraic closure actually needs instead: symmetry, right-affine response in the second argument, the zero-boundary, and the normalization $f(1,1)=6$. Under those hypotheses the combiner is forced to the RCL polynomial $f(a,b)=2ab+2a+2b$.
Clearing the bad scaffold lets the honest classification proceed without pretending associativity of $f$ is available. The result sits next to the RCL landmark and the T5 J-uniqueness step of the forcing chain; it does not itself force uniqueness, but removes a false path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.