Ledger Units

Ledger units

In Recognition Science, a ledger is a discrete record of events, and the ledger units are the individual steps of that record. Think of them as the marks on a ruler: each mark is one unit, and the units are evenly spaced, countable, and never fractional. The framework models this with a mathematical object called a δ-subgroup, which is the set of all integer multiples of a fixed step size δ. For example, if δ is 2, the ledger units are the even numbers; if δ is 3, they are the multiples of 3. The step size δ can be any nonzero integer, and it sets the granularity of the ledger.

The core result of this structure is that it is not exotic. A theorem named quantization proves that every element of a δ-subgroup has a unique integer coefficient: for any nonzero δ and any ledger unit x, there is exactly one integer n such that x equals n times δ. This means the ledger units, no matter how they are scaled, are always in perfect one-to-one correspondence with the ordinary integers. A separate equivalence, called equiv_delta, makes this explicit: the subgroup generated by δ is equivalent to ℤ itself, via the mapping n·δ ↦ n. This is a non-canonical equivalence, meaning the choice of which integer represents which unit is a convention, but the structure itself is fixed.

The framework also shows how to move between the ledger and the integers cleanly. The functions fromZ and toZ translate an integer n into the ledger unit n·δ and back again, and the lemmas toZ_fromZ and fromZ_toZ prove these translations are inverses. This is not just bookkeeping; it establishes that the ledger has no hidden gaps or overlaps. The step from one unit to the next, expressed in integer terms, is always exactly one, as the lemma toZ_succ shows. The framework also defines a rungOf function that extracts the integer index of a ledger unit, and a kOf function that gives a nonnegative index for natural-number steps, with lemmas proving these indices advance by one at each step.

In plain language, this framework establishes that the ledger is a well-behaved, countable, evenly spaced structure. It is the foundation on which the framework builds its more ambitious claims: the golden ratio, the eight-tick recognition cycle, and the forcing of three spatial dimensions. The framework itself does not derive any of those results; it only proves that the ledger's basic arithmetic is sound. What this changes for the reader is that the framework's starting point is not a vague metaphor but a precise, machine-checked mathematical object. The ledger units are not a poetic flourish; they are a rigorously defined structure with provable properties, and this framework is the first step in showing that a discrete record of events can support a full physical theory.

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

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

@[simp] lemma toZ_fromZ (δ : ℤ) (hδ : δ ≠ 0) (n : ℤ) : toZ δ (fromZ δ n) = n := by
  have hval : (fromZ δ n).val = n * δ := rfl
  let k := toZ δ (fromZ δ n)
  have hk : (fromZ δ n).val = k * δ := toZ_spec δ (fromZ δ n)
  have h_eq : n = k := rep_unique (δ:=δ) hδ (by simpa [hval] using hk)
  simpa [k, h_eq.symm]

@[simp] lemma fromZ_toZ (δ : ℤ) (p : DeltaSub δ) : fromZ δ (toZ δ p) = p := by
  apply Subtype.ext
  simpa [fromZ, toZ_spec δ p]

/-- One δ-step corresponds to adding 1 on coefficients via `toZ`. -/
@[simp] lemma toZ_succ (δ : ℤ) (hδ : δ ≠ 0) (n : ℤ) :
  toZ δ (fromZ δ (n + 1)) = toZ δ (fromZ δ n) + 1 := by
  simp [toZ_fromZ δ hδ]

What this page does not claim

This answer does not claim that the framework derives any physical constants or dimensions. This answer does not claim that the choice of δ is physically meaningful; it is a free parameter in this framework. This answer does not claim that the ledger units are the same as the rungs of the eight-tick cycle.

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: