IndisputableMonolith.Verification.Exclusivity.RCLDerivation
Defines composition rules for a cost functional J: symmetric binary maps f with J(xy)+J(x/y)=f(J(x),J(y)). Classifies which f are compatible with boundary and associativity constraints, isolating the d'Alembert combiner that yields the Recognition Composition Law. Cited by exclusivity and no-alternatives arguments that force J uniquely. The argument is algebraic classification plus boundary contradictions, importing factorization forcing.
claimA composition rule is a symmetric $f:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ such that $J(xy)+J(x/y)=f(J(x),J(y))$. The d'Alembert rule is $f(u,v)=2uv+2u+2v$. The module proves boundary identities for such $f$, shows pure associativity conflicts with those boundaries, and classifies admissible $f$ down to the d'Alembert form (hence the Recognition Composition Law).
background
Recognition Science treats cost as a functional $J$ on positive reals obeying a two-argument decomposition under product and quotient. The Recognition Composition Law (RCL) is the concrete identity $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$, equivalent to the classical d'Alembert form after the shift $T=J+1$.
This module sits in the exclusivity verification layer. It imports shared physics-framework definitions and the factorization/associativity gate from the d'Alembert foundation: that gate reduces the hard analytic step (factorization plus three-way compatibility) to affinity of the combiner in its second argument, after which forcing is pure algebra.
Local objects are the abstract composition rule (any symmetric $f$ mediating the $J$-decomposition), the concrete d'Alembert rule, and boundary lemmas such as $f(0,0)=0$ and the value of $f$ on the zero section.
proof idea
Definition layer first: CompositionRule packages symmetry and the functional equation $J(xy)+J(x/y)=f(J(x),J(y))$; dAlembertRule is the explicit bilinear target.
Boundary lemmas evaluate $f$ at zero and check that d'Alembert meets those boundaries. An associativity-versus-boundary lemma shows that a purely associative combiner cannot satisfy the same boundary data, ruling out naive alternatives.
The classification theorem then combines those constraints with the imported factorization-forcing algebra to pin admissible $f$ to the d'Alembert combiner, recovering RCL as the unique composition law in this class.
why it matters in Recognition Science
RCL is the algebraic skeleton behind T5 J-uniqueness in the forcing chain: once composition is forced to d'Alembert form, $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$) is the unique normalized solution. This module supplies the exclusivity-side derivation of that law from composition-rule axioms rather than assuming RCL outright.
It feeds the broader no-alternatives / exclusivity program by showing competing combiners fail boundary or associativity gates. Downstream pages in Verification.Exclusivity consume the classification when closing "no other cost calculus" claims. No direct used_by edges are recorded on this module node itself; its sibling theorems are the reusable hooks.
scope and limits
- Does not prove uniqueness of J itself; only classifies the composition combiner f.
- Does not re-derive factorization-to-affinity; that is imported from FactorizationForcing.
- Does not treat non-symmetric or higher-arity composition laws.
- Does not numerically fix constants (phi, alpha, masses); pure functional-equation content.
- Does not claim a closed exclusivity theorem alone; it is one algebraic step in that program.