dAlembertRule
plain-language theorem explainer
Packages the d'Alembert binary law f(a,b)=2(a+1)(b+1)-2 as a CompositionRule, i.e. the unique symmetric real map that realises J(xy)+J(x/y) once a=J(x) and b=J(y). Anyone deriving or classifying the Recognition Composition Law cites this witness. Symmetry is a one-line ring identity; the body is pure data plus that proof.
Claim. The d'Alembert composition rule is the symmetric map $f:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ given by $f(a,b)=2(a+1)(b+1)-2$, equivalently $f(a,b)=2ab+2a+2b$. It is the candidate right-hand side in $J(xy)+J(x/y)=f(J(x),J(y))$.
background
In this module a composition rule is a symmetric binary function $f$ on $\mathbb{R}$ that specifies how compound cost values decompose: $J(xy)+J(x/y)=f(J(x),J(y))$. The structure only records the map and the symmetry obligation; boundary laws and uniqueness are proved separately.
The classical d'Alembert (cosine) functional equation produces exactly $f(a,b)=2ab+2a+2b$ when the cost is the T5 J-cost $J(x)=(x+x^{-1})/2-1$. Expanding $2(a+1)(b+1)-2$ recovers the Recognition Composition Law form $2J(x)J(y)+2J(x)+2J(y)$ used throughout the exclusivity and forcing chain.
The local setting is verification of exclusivity for RCL: one exhibits a concrete rule, checks the forced boundaries $f(0,0)=0$ and $f(a,0)=2a$, then shows rival scaffolds (e.g. associativity-only) contradict those boundaries.
proof idea
Definitional construction of a CompositionRule record. The field $f$ is the closed-form $a,b\mapsto 2(a+1)(b+1)-2$. The symmetry field is discharged by intro a b; ring, which rewrites both sides to the same polynomial. No upstream lemmas are invoked beyond the structure type.
why it matters
This is the concrete RCL witness inside the exclusivity derivation. Downstream, dAlembert_satisfies_boundaries proves $f(0,0)=0$ and $\forall a,,f(a,0)=2a$ by unfolding this definition and simplifying. Those boundaries feed the classification that rules out associativity-only scaffolds and pin the Recognition Composition Law as the forced composition of the T5 J-cost.
In the primer landmarks this is exactly the right-hand side of RCL, the functional equation that sits under J-uniqueness (T5) and the later forcing of $\varphi$, the eight-tick octave, and $D=3$. Without a named, symmetry-checked rule object, the boundary and classification theorems have nothing to evaluate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.