Ledger Units Rep Unique

Unique representation

The declaration rep_unique establishes a basic fact about the framework's ledger, a discrete record of events indexed by whole numbers. It says: if you have two integer labels n and m, and multiplying each by the same nonzero step size δ gives the same result, then n and m must be the same integer. In plain terms, when the step size is fixed and nonzero, every position in the ledger has exactly one integer address. No two different labels can secretly point to the same place.

This is a theorem about the integers, proved in the machine-checked library of formal theorems. The proof is short: from n·δ = m·δ, subtract to get (n - m)·δ = 0. Since δ is nonzero, the only way a product equals zero is if the other factor is zero, so n - m = 0, hence n = m. The declaration also supports the broader statement called quantization: for any nonzero step size, every element of the subgroup generated by δ has a unique integer coefficient. That means the ledger's positions are not just countable, they are labeled without ambiguity.

The classical cousin is the fundamental theorem of arithmetic's spirit applied to a single generator: the subgroup of integers generated by δ is isomorphic to the integers themselves, via the map n·δ ↦ n. The framework uses this to define rung indices: each step of size δ corresponds to adding 1 to the coefficient. The uniqueness is what makes the rung index a well-defined function rather than a choice that could vary.

What rep_unique does not claim is broader than what it does. It does not say that the step size δ is forced to be 1, or that the ledger must use unit steps. It only says that once δ is chosen and nonzero, the representation is unique. It also does not claim anything about which δ the framework actually uses, nor about the physical meaning of the rungs. The theorem is purely about integer arithmetic inside the subgroup; it is a structural guarantee, not a statement about the real world.

The consequence is practical: when the framework assigns a rung index to a position, that index is unambiguous. This is the foundation for later claims about the eight-tick cycle and the golden ratio, which rely on counting steps without ambiguity. Without rep_unique, the whole ladder of derived results would rest on a shaky base where labels could collide.

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

/-- 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 rungOf_step (δ : ℤ) (hδ : δ ≠ 0) (n : ℤ) :
  rungOf δ (fromZ δ (n + 1)) = rungOf δ (fromZ δ n) + 1 := by
  simpa [rungOf] using (toZ_succ (δ:=δ) (hδ:=hδ) (n:=n))

What this page does not claim

The theorem does not force δ to equal 1, only that any nonzero δ gives unique labels. The theorem does not assign physical meaning to the rungs or the step size. The theorem does not connect to the golden ratio or the eight-tick cycle on its own.

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: