composition_rule_f_at_zero
plain-language theorem explainer
Any composition rule compatible with a cost J that vanishes at 1 must obey the axis law f(a,0)=2a. Workers deriving the Recognition Composition Law from a free binary rule cite this to pin the second boundary. The argument is a direct specialization: set the second factor to 1 and simplify with J(1)=0.
Claim. Let $f$ be a composition rule (symmetric $f:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$) and $J:\mathbb{R}\to\mathbb{R}$ with $J(1)=0$. Suppose for all $x,y>0$, $J(xy)+J(x/y)=f(J(x),J(y))$. Then for every $x>0$, $f(J(x),0)=2\,J(x)$.
background
A composition rule packages a symmetric binary map $f$ that reconstructs compound recognition costs via $J(xy)+J(x/y)=f(J(x),J(y))$. The d'Alembert choice $f(a,b)=2ab+2a+2b$ is exactly the Recognition Composition Law once $J$ is the unique cost $J(x)=(x+x^{-1})/2-1$.
This module classifies which rules can arise from a cost normalized by $J(1)=0$. Two axis conditions pin $f$: $f(0,0)=0$ and $f(a,0)=2a$. The present result is the second boundary.
Only the real identities $x\cdot 1=x$ and $x/1=x$, plus positivity of $1$, are required.
proof idea
Instantiate the composition identity at $y=1$. Positivity of $x$ and of $1$ applies the hypothesis, giving $J(x\cdot 1)+J(x/1)=f(J(x),J(1))$. The normalization $J(1)=0$ together with $x\cdot 1=x$ and $x/1=x$ collapses the left-hand side to $J(x)+J(x)$. Linear arithmetic rewrites that as $2J(x)$, which is $f(J(x),0)$.
why it matters
This is boundary condition 2 in the RCL derivation narrative: $f(a,0)=2a$. Together with the sibling $f(0,0)=0$, it feeds the local classification of composition rules and the check that d'Alembert meets both boundaries, forcing $f$ onto $2ab+2a+2b$. That functional equation is the Recognition Composition Law, whose unique continuous solution is the J-cost of forcing step T5 and which underwrites the later forcing of $\varphi$, the eight-tick octave, and $D=3$. No downstream used-by edges are recorded yet; the lemma still closes the second named boundary in the exclusivity path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.