Ledger Units Equiv Delta One

The unit equivalence

The integers are the simplest infinite counting system: ..., -2, -1, 0, 1, 2, ... with addition and order. A ledger, a discrete record of events, often needs a unit step, a fixed interval between consecutive entries. The Recognition Science declaration equiv_delta_one proves, in the framework's machine-checked library of formal theorems, that when the unit step is 1, the ledger's structure is exactly the integers: every ledger entry corresponds to exactly one integer, and every integer corresponds to exactly one ledger entry. The two are interchangeable, a clean order isomorphism.

The proof is built from two simple maps. One takes an integer n and embeds it into the ledger as the entry n·1, which is just n. The other takes a ledger entry and extracts its integer value. The declaration then verifies the two essential properties: applying one map and then the other returns you to where you started, in both directions. This is the definition of an equivalence, and the machine checks every step. The result is tagged as a definition in the library, but its correctness rests on lemmas the kernel verifies, not on an axiom about ledgers.

The declaration does not claim that this equivalence is the only possible one, nor that it extends to other unit steps. For a general nonzero step δ, the library separately proves a non-canonical equivalence: the subgroup generated by δ is still equivalent to the integers, via n·δ ↦ n, but that choice of map is not forced. The special case δ = 1 is canonical because the map is the identity in disguise. The general case requires a choice, marked noncomputable, and the library says so explicitly.

What this buys is a vocabulary. Once the δ = 1 ledger is known to be the integers, every integer fact, every theorem about addition, order, and divisibility, becomes a fact about the ledger. The declaration is the bridge that lets later work in the framework speak of rungs, coefficients, and steps without re-proving the integers from scratch. It is a small, quiet result, but it is the kind of result that makes a larger structure safe to build on.

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

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

The declaration does not prove that the ledger's order structure is preserved, only its underlying set and group structure. It does not claim that the equivalence for δ = 1 is unique, only that this particular map is an equivalence. It says nothing about what happens when δ is zero.

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: