Ledger Units Rung Of Step

The step rule

A ledger is a discrete record of events, each entry tagged by a whole number. Recognition Science models such records with a step size δ, a fixed integer gap between consecutive entries. The declaration rungOf_step states a counting rule: if you start at any entry and move one δ-step forward, the index that counts your position increases by exactly one. The proof is short and mechanical: it identifies each entry with its integer coefficient, then applies the ordinary fact that adding one to a number's argument adds one to the number itself.

The rule holds for every nonzero step size δ, not just for δ = 1. When δ = 1, the correspondence between entries and integers is clean and canonical. For other δ, the correspondence still works but requires a choice, because an entry like 6 could be two steps of size 3 or three steps of size 2. The theorem handles this by fixing a representative for each entry, then proving the step rule is independent of that choice.

What the rule does not do is give the step size physical meaning. It says nothing about what δ should be in nature, whether it is a length, a time, or an abstract unit. It also does not say that every ledger must use a uniform step; it only describes what happens inside one that does. The theorem is a statement about counting within a fixed grid, not about which grid the universe uses.

The practical upshot is a guarantee of consistency. If a framework builds on ledgers with steps, this rule ensures that "one step forward" always means the same thing in the index, no matter where you start. That uniformity is what lets later claims about cycles and scales be stated cleanly, without worrying that the counting might drift.

lemma rungOf_step (δ : ℤ) (hδ : δ ≠ 0) (n : ℤ) :
  rungOf δ (fromZ δ (n + 1)) = rungOf δ (fromZ δ n) + 1 := by
  simpa [rungOf] using (toZ_succ (δ:=δ) (hδ:=hδ) (n:=n))

lemma rungOf_step (δ : ℤ) (hδ : δ ≠ 0) (n : ℤ) :
  rungOf δ (fromZ δ (n + 1)) = rungOf δ (fromZ δ n) + 1 := by
  simpa [rungOf] using (toZ_succ (δ:=δ) (hδ:=hδ) (n:=n))

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

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

What this page does not claim

The step size δ has no physical meaning assigned by this theorem. The theorem does not require every ledger to use a uniform step size. The rule does not identify which grid, if any, the universe actually uses.

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: