Ledger Units K Of Step Succ

The step rule

A ledger, in the Recognition Science framework, is a discrete record of events, each event a step along a line of integers. The framework's library, a machine-checked collection of formal theorems, builds a unit system for such ledgers. The declaration kOf_step_succ is a lemma about that unit system. It says: if you take one step forward from a position, the count of steps from the start increases by exactly one. The statement is written for any nonzero step size δ, and for any natural number m. In symbols, the lemma reads: kOf δ (fromNat δ (m+1)) = kOf δ (fromNat δ m) + 1.

The proof is short and relies on two earlier facts. First, the function fromNat embeds a natural number into the δ-subgroup of the integers, the set of multiples of δ. Second, the function kOf extracts a nonnegative index from an element of that subgroup, by reading off its integer coefficient and truncating to a natural number. The lemma then follows by unpacking these definitions and simplifying. The same library also proves a companion statement, quantization, which says that every element of the δ-subgroup has a unique integer coefficient, provided δ is nonzero. That uniqueness is what makes the step rule meaningful: the count is well-defined, not a choice.

What the lemma does not claim is just as important as what it does. It does not say that the ledger's unit δ is forced to be 1. The framework's own docstring notes that δ = 1 is chosen for a clean order isomorphism, but the step rule holds for any nonzero δ. Nor does the lemma say anything about the physical meaning of a step, the cost of recognition, or the golden ratio. It is a purely combinatorial fact about counting in a discrete subgroup of the integers. The step rule is a building block, not a conclusion about the world.

In the wider framework, this lemma supports the idea that a ledger has a natural counting structure: steps compose, and the count behaves as expected. That structure is a prerequisite for the framework's later claims about recognition cycles and scaling. The step rule is what makes the ledger a ledger, rather than an unordered set of events.

lemma kOf_step_succ (δ : ℤ) (hδ : δ ≠ 0) (m : Nat) :
  kOf δ (fromNat δ (m+1)) = kOf δ (fromNat δ m) + 1 := by
  simp only [kOf, fromNat, toZ_fromZ δ hδ, Int.natCast_add, Int.natCast_one]
  rfl

lemma kOf_step_succ (δ : ℤ) (hδ : δ ≠ 0) (m : Nat) :
  kOf δ (fromNat δ (m+1)) = kOf δ (fromNat δ m) + 1 := by
  simp only [kOf, fromNat, toZ_fromZ δ hδ, Int.natCast_add, Int.natCast_one]
  rfl

/-- 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 step rule does not force the ledger's unit δ to be 1. The step rule says nothing about the cost of recognition or the golden ratio. The lemma is a combinatorial fact about integers, not a statement about physical space.

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: