Foundation Dalembert Ledger Factorization Combiner Zero Boundary

The zero boundary

In mathematics, a ledger, a discrete record of events, can track the cost of comparing two positive numbers. The comparison cost J(x) measures how far a number x sits from 1, the point of perfect equality. The declaration combiner_zero_boundary establishes a specific fact about how these individual costs combine when you compare products and quotients.

The result concerns a combiner P that takes two individual costs and returns the total cost of a compound comparison. The theorem states that when one of those individual costs is zero, meaning one comparison is already at perfect equality, the total cost is exactly twice the other cost. In symbols, P(u, 0) = 2u. This follows from setting the second comparison to the number 1, so the compound cost J(x·1) + J(x/1) reduces to 2J(x).

This zero boundary is one of four properties that together force the combiner to take a specific algebraic form. The other properties are symmetry, the unit diagonal P(1,1) = 6, and a right-affine response. Once all four hold, the framework's library proves the combiner must equal P(u,v) = 2uv + 2u + 2v, which is the Recognition Composition Law. The zero boundary is therefore a load-bearing step in a chain that leads from basic ledger principles to a unique cost function.

In Recognition Science, this chain is part of a larger argument that a single cost function J(x) = (x + 1/x)/2 − 1 is forced by five plain conditions. The zero boundary theorem is a proved result in the framework's machine-checked library of formal theorems, meaning it follows from the stated hypotheses without additional assumptions. It does not, however, claim anything about what happens when both comparisons are nonzero, nor does it establish the full cost function on its own.

/-- The zero boundary `P(u, 0) = 2u` follows from setting `y = 1`:
`J(x·1) + J(x/1) = 2J(x) = P(J(x), J(1)) = P(J(x), 0)`. -/
theorem combiner_zero_boundary
    (J : ℝ → ℝ) (hJ0 : J 1 = 0)
    (P : ℝ → ℝ → ℝ)
    (hComp : ∀ x y : ℝ, 0 < x → 0 < y →
      J (x * y) + J (x / y) = P (J x) (J y))
    (hSurj : ∀ a : ℝ, ∃ x : ℝ, 0 < x ∧ J x = a) :
    ∀ u, P u 0 = 2 * u := by
  intro u
  obtain ⟨x, hx, hJx⟩ := hSurj u
  have h := hComp x 1 hx one_pos
  rw [mul_one, div_one, hJ0] at h
  rw [← hJx]
  linarith

What this page does not claim

The zero boundary alone does not determine the combiner; the other three properties are needed. The theorem does not apply when the second cost is nonzero. This result does not by itself prove the full cost function J(x) = (x + 1/x)/2 − 1.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/DAlembert/LedgerFactorization.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: