combiner_zero_boundary
plain-language theorem explainer
The theorem shows that a surjective cost function J with J(1)=0 forces the combiner P to satisfy P(u,0)=2u for every real u. Ledger factorization arguments cite this zero-boundary condition when anchoring the combiner before recovering the full Recognition Composition Law. The argument is a direct substitution: instantiate the composition hypothesis at y=1, simplify with arithmetic identities, and apply surjectivity plus linear arithmetic.
Claim. Let $J:ℝ→ℝ$ satisfy $J(1)=0$ and let $P:ℝ→ℝ→ℝ$ satisfy $J(xy)+J(x/y)=P(J(x),J(y))$ whenever $x>0$ and $y>0$. If $J$ is surjective onto $ℝ$, then $P(u,0)=2u$ for all real $u$.
background
The Ledger Factorization module derives the Recognition Composition Law from contextual substitutivity and regrouping invariance on a comparison ledger. Here J denotes the J-cost induced by a multiplicative recognizer (from MultiplicativeRecognizerL4.cost and ObserverForcing.cost), normalized so that J(1)=0. The combiner P is the binary operation that packages the total cost of a pair of comparisons. Surjectivity of J guarantees every real arises as a cost value. Upstream results include the canonical arithmetic object (ArithmeticOf.canonical) and the magnitude-of-mismatch structure that enforces single-valued comparisons.
proof idea
The term proof introduces an arbitrary u, obtains x>0 with J x = u via the surjectivity hypothesis, applies the composition hypothesis to the pair (x,1), rewrites using mul_one and div_one together with J(1)=0, substitutes back the definition of u, and closes with linarith.
why it matters
The result is invoked by ledger_forces_regrouping to obtain the full regrouping-invariance package. It supplies the zero-boundary step required to pass from the ledger axioms to the Recognition Composition Law polynomial, consistent with the module's derivation path and the T5 J-uniqueness landmark. The boundary anchors the forcing chain that later yields the eight-tick octave and D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.