composition_rule_f00_eq_zero
plain-language theorem explainer
Any composition rule compatible with a cost J that vanishes at 1 must send the pair (0,0) to 0. Workers deriving the Recognition Composition Law from first principles cite this as Boundary condition 1 on the binary kernel. The argument is a one-line specialization of the composition identity at the multiplicative unit, followed by arithmetic.
Claim. Let $f:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ be the binary map of a composition rule, and let $J:\mathbb{R}\to\mathbb{R}$ satisfy $J(1)=0$. If $J(xy)+J(x/y)=f(J(x),J(y))$ holds for all $x,y>0$, then $f(0,0)=0$.
background
In the Recognition framework a cost $J$ is required to package the pair of compound values $J(xy)$ and $J(x/y)$ into a single binary operation on the cost scale. A composition rule is exactly that package: a symmetric map $f:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ obeying $J(xy)+J(x/y)=f(J(x),J(y))$ for positive arguments.
The classical d'Alembert (Recognition Composition Law) choice is $f(a,b)=2ab+2a+2b$, equivalently $2(a+1)(b+1)-2$. Before uniqueness is settled one extracts the boundary values that every admissible $f$ is forced to satisfy once the normalization $J(1)=0$ is imposed. That normalization is the standard fixed point of cost at the multiplicative identity and sits inside the T5 J-uniqueness package $J(x)=(x+x^{-1})/2-1$.
This module lives in the exclusivity/verification layer that classifies which composition rules can arise from a genuine cost.
proof idea
Specialize the composition identity at $x=y=1$ (both strictly positive). The left-hand side collapses to $J(1)+J(1)$. The right-hand side is $f(J(1),J(1))$. Substitute the hypothesis $J(1)=0$ to obtain $0=f(0,0)$, then finish by linear arithmetic on $\mathbb{R}$. No continuity or other regularity is used.
why it matters
This is Boundary condition 1 in the RCL-derivation pipeline. Together with the companion identity $f(a,0)=2a$ it pins every candidate composition kernel on the coordinate axes. Those axis values later feed the local classification that only the d'Alembert rule (hence the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$) survives. The RCL is the functional equation underlying T5 J-uniqueness in the forcing chain.
No recorded downstream edges yet; the immediate consumers are the sibling results that establish the second boundary, verify that d'Alembert meets both boundaries, and classify admissible rules. The lemma therefore closes the first forced constraint in the exclusivity argument that no rival composition law is compatible with a genuine cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.