combiner_zero_boundary
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not assume any convexity or differentiability on J.
- Does not derive the explicit polynomial form of P.
- Does not establish the full Recognition Composition Law.
- Requires surjectivity of J onto all reals.
formal statement (Lean)
94theorem combiner_zero_boundary
95 (J : ℝ → ℝ) (hJ0 : J 1 = 0)
96 (P : ℝ → ℝ → ℝ)
97 (hComp : ∀ x y : ℝ, 0 < x → 0 < y →
98 J (x * y) + J (x / y) = P (J x) (J y))
99 (hSurj : ∀ a : ℝ, ∃ x : ℝ, 0 < x ∧ J x = a) :
100 ∀ u, P u 0 = 2 * u := by
proof body
Term-mode proof.
101 intro u
102 obtain ⟨x, hx, hJx⟩ := hSurj u
103 have h := hComp x 1 hx one_pos
104 rw [mul_one, div_one, hJ0] at h
105 rw [← hJx]
106 linarith
107
108/-- The unit diagonal `P(1, 1) = 6` follows from calibration.
109When `J(x₀) = 1` (which exists by the intermediate value theorem
110on a strictly convex cost), `P(1,1) = J(x₀²) + J(1)`. The
111calibration `(J∘exp)''(0) = 1` together with strict convexity
112forces `J(x₀²) + J(1) = 6` at the canonical normalization. -/