Foundation Universal Forcing Forced Integers To Int Injective

The embedding

The integers are the everyday counting numbers, their negatives, and zero. In the Recognition Science framework, a ledger (a discrete record of events) gives rise to a collection of forced numbers, each built from a count of repeated steps. The declaration toInt_injective proves that this collection embeds into the integers: every forced number is assigned an integer, and two different forced numbers never receive the same integer. In plain terms, the map is a perfect one-to-one labeling; nothing is lost and nothing is conflated.

The proof is short and mechanical. It shows that if two forced numbers map to the same integer, then their underlying counts are equal, and therefore the numbers themselves are equal. This injectivity is one part of a larger certificate: the forced arithmetic preserves zero, one, addition, and multiplication, and its differences cover every integer. The certificate, assembled in the framework's machine-checked library of formal theorems, confirms that the integer layer is not a partial copy but the full additive group.

What the declaration does not claim is equally important. It does not say that every integer is itself a forced number; that is a separate surjectivity result. It does not assert that the embedding is unique, nor that it respects order or any structure beyond the listed operations. It only guarantees that the labeling is faithful. This faithfulness matters because it lets the framework treat forced numbers as genuine integers when doing arithmetic, without fear of silent collisions.

theorem toInt_injective : Function.Injective toInt := by
  intro a b h
  have hnat : LogicNat.toNat a = LogicNat.toNat b := by
    have : (LogicNat.toNat a : ℤ) = (LogicNat.toNat b : ℤ) := h
    exact_mod_cast this
  exact LogicNat.equivNat.injective hnat

@[simp] theorem toInt_zero : toInt LogicNat.zero = 0 := by simp [toInt]

@[simp] theorem toInt_one : toInt 1 = 1 := by
  show ((LogicNat.toNat 1 : ℕ) : ℤ) = 1
  rw [show LogicNat.toNat 1 = 1 from rfl]
  norm_num

theorem toInt_add (a b : LogicNat) : toInt (a + b) = toInt a + toInt b := by
  simp only [toInt]
  rw [LogicNat.toNat_add]
  push_cast
  ring

theorem toInt_mul (a b : LogicNat) : toInt (a * b) = toInt a * toInt b := by
  simp only [toInt]
  rw [LogicNat.toNat_mul]
  push_cast
  ring

/-- **Every integer is a difference of two forced numbers.** The forced
difference layer is all of `ℤ`, so distinction forces the full additive group of
integers, not a proper sub-collection. -/
theorem integers_surject (z : ℤ) :
    ∃ a b : LogicNat, z = toInt a - toInt b := by
  refine ⟨LogicNat.fromNat z.toNat, LogicNat.fromNat (-z).toNat, ?_⟩
  simp only [toInt, LogicNat.toNat_fromNat]
  omega

What this page does not claim

The declaration does not claim that every integer is a forced number. The declaration does not claim the embedding is unique or that it preserves order. The declaration does not claim the forced numbers form the full ring of integers themselves.

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/Foundation/UniversalForcing/ForcedIntegers.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: