Ledger Units Equiv Delta

The unit equivalence

In mathematics, the integers ℤ form the standard infinite counting line. A subgroup of ℤ generated by a single integer δ consists of all multiples of δ: the set {0, ±δ, ±2δ, ±3δ, ...}. When δ = 1, this subgroup is exactly ℤ itself, and the identity map is the obvious equivalence. The Recognition Science declaration equiv_delta (a formal statement in the framework's machine-checked library of formal theorems) proves that for any nonzero integer δ, this subgroup is equivalent to ℤ via the map n·δ ↦ n.

The equivalence is non-canonical in the general case: it depends on choosing, for each element of the subgroup, which integer coefficient n represents it. The proof uses the classical choice principle to pick such a coefficient, then shows the round-trip maps compose to the identity. A companion theorem, quantization, states that every element of the δ-subgroup has a unique integer coefficient n such that x = nδ. Together these results say that the structure of the subgroup is always the same as ℤ, regardless of the step size δ.

In Recognition Science, this lemma supports a unit-convention observation: the framework's discrete ledger of recognition events can be indexed by any fixed nonzero integer step δ, and the resulting counting structure is order-isomorphic to the plain integers. The special case δ = 1 gives a clean, canonical isomorphism that the framework uses for its standard rung indexing. The general case shows that no particular step size is privileged by the mathematics alone.

What equiv_delta does not claim: it does not assert that different step sizes produce different physical theories, nor that any specific δ is forced by the framework's axioms. It is a structural lemma about integer subgroups, not a statement about which unit the universe must use. The choice of δ remains a modeling decision, not a theorem.

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

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

No specific step size δ is forced by the framework's axioms. The lemma does not establish any physical unit system as preferred. The equivalence does not extend to real-valued step sizes.

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: