Ledger Units From Z One

The unit step

A ledger, a discrete record of events, needs a unit: the smallest step by which entries advance. The declaration fromZ_one in the framework's machine-checked library of formal theorems fixes that unit for the simplest case. It states that every integer, positive or negative, can be placed onto the ledger's step of size one, and that this placement loses nothing. The round trip is exact: send an integer to its ledger entry, then read the entry back, and you recover the integer you started with. The same holds in reverse for every entry on that unit step. The two directions together make the integer line and the unit-step ledger interchangeable as ordered structures.

This is a bookkeeping fact, not a physical one. The declaration does not say that the universe counts in ones, that recognition events must be spaced by a single unit, or that any particular quantity in nature equals one. It says only that a ledger whose step is one is a faithful copy of the integers: no information is added, none is lost, and the copy respects the order of counting. The proof is immediate from the definitions, and the library records it as a pair of simplification rules plus an explicit equivalence.

The wider file generalizes the same idea. For any nonzero integer step, the entries on that step still form a copy of the integers, though the matching is no longer canonical: the map from entry to coefficient depends on a choice. The unit case is the clean one, and fromZ_one is its foundation. What the declaration changes for a reader is simple. When the framework later speaks of rung indices or step counts, the unit case already guarantees that counting by ones is a well-defined, reversible operation, not a convention left floating.

/-- Embed ℤ into the δ=1 subgroup. -/
def fromZ_one (n : ℤ) : DeltaSub 1 := ⟨n, by exact ⟨n, by simpa using (Int.mul_one n)⟩⟩

@[simp] lemma toZ_fromZ_one (n : ℤ) : toZ_one (fromZ_one n) = n := rfl

@[simp] lemma fromZ_toZ_one (p : DeltaSub 1) : fromZ_one (toZ_one p) = p := by
  cases p with
  | mk x hx =>
    apply Subtype.ext
    rfl

/-- Explicit equivalence between the δ=1 subgroup and ℤ (mapping n·1 ↦ n). -/
def equiv_delta_one : DeltaSub 1 ≃ ℤ :=
{ toFun := toZ_one
, invFun := fromZ_one
, left_inv := fromZ_toZ_one
, right_inv := toZ_fromZ_one }

/-- For any nonzero δ, the subgroup of ℤ generated by δ is (non‑canonically) equivalent to ℤ via n·δ ↦ n. -/
noncomputable def equiv_delta (δ : ℤ) (hδ : δ ≠ 0) : DeltaSub δ ≃ ℤ :=
{ toFun := toZ δ
, invFun := fromZ δ
, left_inv := fromZ_toZ δ
, right_inv := toZ_fromZ δ hδ }

/-- Quantization: every element of the δ-subgroup has a unique integer coefficient. -/
theorem quantization {δ : ℤ} (hδ : δ ≠ 0) (x : DeltaSub δ) :
  ∃! (n : ℤ), x.val = n * δ :=
by
  classical
  -- Existence from `toZ_spec`
  refine ⟨toZ δ x, ?eq, ?uniq⟩
  · simpa [toZ_spec δ x]
  · intro m hm
    -- Uniqueness from `rep_unique`
    have h1 : x.val = toZ δ x * δ := toZ_spec δ x
    have h2 : x.val = m * δ := hm
    have : m * δ = toZ δ x * δ := by rw [← h2, h1]
    exact rep_unique (δ:=δ) hδ this

What this page does not claim

The declaration does not claim that the universe counts in ones or that any physical quantity equals one. It does not claim that recognition events are spaced by a single unit. It does not claim that the unit step is derived from the cost function; it is a definitional choice.

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/LedgerUnits.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: