Ledger Units Quantization

The quantization theorem

Quantization, in its plainest form, is the statement that certain quantities come in whole-number multiples of a fixed unit. The Recognition Science framework formalizes this idea for its ledger, a discrete record of events. The framework's library, a machine-checked collection of formal theorems, proves a theorem called quantization: for any nonzero integer step size δ, every element of the subgroup generated by δ has a unique integer coefficient. In symbols, for every x in the subgroup, there exists exactly one integer n such that x = n·δ.

The proof rests on a simple algebraic fact. If n·δ = m·δ and δ is nonzero, then n = m. This uniqueness of representation is the core lemma, and the theorem packages it as an existence-plus-uniqueness statement. The framework also provides explicit maps between the subgroup and the integers: a forward map sending n to n·δ, and a backward map sending each element to its unique coefficient. These maps are proven to be inverses, making the equivalence between the subgroup and ℤ explicit.

The framework specializes to the case δ = 1, where the subgroup is all of ℤ and the equivalence is clean and canonical. For general nonzero δ, the equivalence still holds but is non-canonical, meaning the choice of which element corresponds to which integer requires a choice function. The framework also defines a rung index and a nonnegative k-index, both derived from the unique coefficient, and proves that stepping by one in the subgroup corresponds to adding one to these indices.

What the theorem does not claim is broader significance. It does not assert that physical quantities in the actual universe are quantized in this way; it only establishes the mathematical structure within the framework's ledger model. It does not claim that the step size δ is determined by the framework, only that any nonzero integer δ yields a consistent quantization. The theorem is a statement about integer arithmetic and subgroups, not about the physical constants or the fine-structure constant.

/-- 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

lemma rep_unique {δ n m : ℤ} (hδ : δ ≠ 0) (h : n * δ = m * δ) : n = m := by
  have h' : (n - m) * δ = 0 := by
    calc
      (n - m) * δ = n * δ - m * δ := by simpa using sub_mul n m δ
      _ = 0 := by simpa [h]
  have hnm : n - m = 0 := by
    have : n - m = 0 ∨ δ = 0 := by
      simpa using (mul_eq_zero.mp h')
    cases this with
    | inl h0 => exact h0
    | inr h0 => exact (hδ h0).elim
  exact sub_eq_zero.mp hnm

/-- 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δ }

What this page does not claim

Physical quantities in the actual universe are quantized in this way. The step size δ is determined by the framework. The theorem constrains the fine-structure constant or other physical constants.

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: