dAlembert_satisfies_boundaries
plain-language theorem explainer
The d'Alembert composition rule meets both boundary conditions required of an RCL candidate: f(0,0)=0 and f(a,0)=2a for all a. Anyone classifying admissible composition rules in the exclusivity/RCL derivation cites this check. The proof is a direct unfolding of the rule definition plus ring arithmetic.
Claim. Let $f$ be the binary operation of the d'Alembert composition rule. Then $f(0,0)=0$ and, for every scalar $a$, $f(a,0)=2a$.
background
Module Verification.Exclusivity.RCLDerivation classifies binary composition rules that can underwrite the Recognition Composition Law
$J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$.
A CompositionRule packages such an $f$ together with structural hypotheses; the two boundary laws $f(0,0)=0$ and $f(a,0)=2a$ are the minimal cost-normalization conditions inherited from the J-cost (T5: $J(x)=(x+x^{-1})/2-1$).
The d'Alembert rule is the classical candidate tied to that J-form (via the factorization forcing import). Sibling lemmas record the same boundaries abstractly for any composition rule, and the next result shows that plain associativity of $f$ already collides with $f(a,0)=2a$.
proof idea
Term-mode pair constructor, no external lemmas. The left conjunct is simp on the definition of the d'Alembert rule (which hard-codes $f$). The right conjunct introduces $a$, unfolds the same definition, and finishes by ring.
why it matters
This is the concrete boundary check that licenses the d'Alembert rule inside the RCL exclusivity pipeline. The immediately following sibling uses $f(a,0)=2a$ (plus symmetry) to kill the old associativity-only scaffold: symmetry gives $f(0,1)=2$ and $f(0,2)=4$, while associativity at $(0,0,1)$ would force $f(0,1)=f(0,2)$, so Open Problem B was malformed. The real closure step is therefore the full composition-rule classification, not associativity of $f$ itself. Framework landmark: T5 J-uniqueness and the RCL identity that J satisfies.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.