Foundation Universal Forcing Forced Integers Integers Surject

The forced integers

An integer is a whole number, positive, negative, or zero: ... -2, -1, 0, 1, 2, and so on. In the Recognition Science framework, the basic objects are not numbers but recognition events, discrete records of one thing being distinguished from another. The framework's starting question is what structure such a ledger of distinctions forces into existence. The declaration integers_surject is part of the answer: it proves that the integers are not an optional addition to such a ledger but a necessary consequence of it.

The theorem itself is simple to state. It says that every integer can be written as a difference of two forced numbers, where a forced number is a count of recognition events. The proof constructs the two counts explicitly: for any integer z, it takes the positive part of z and the positive part of -z, then subtracts one from the other. This construction is checked line by line in a machine-checked library of formal theorems, so the claim carries the full weight of a formal proof rather than a paper argument.

What makes this interesting is what it shows about the framework's reach. The integers come with their usual arithmetic: the embedding preserves zero, one, addition, and multiplication. It is injective, meaning different forced numbers map to different integers, so no information is lost. And the differences cover all of the integers, not just a subset. The framework also proves a structural mirror: negation, which swaps the two counts of a difference, fixes a difference exactly when the two counts are equal, just as the reciprocal operation on ratios fixes a ratio exactly at the unit. The integer layer and the ratio layer carry the same comparison geometry.

In Recognition Science, this result is a step in a larger chain. The framework models reality as a forced ledger of recognition events, and from that starting point it derives constants and structures that in conventional physics are taken as given. The integers being forced is a foundational piece of that derivation: if the ledger forces the integers, then arithmetic itself is not an assumption but a consequence. The certificate structure in the library bundles the embedding, the surjectivity, and the negation property into a single statement, and the library proves that this certificate holds.

What the theorem does not claim is equally important. It does not say that the integers are the only structure that exists, nor that every mathematical truth follows from the ledger. It does not claim that the integers exist independently of the framework's axioms; the proof lives inside a specific logical system with its own postulates. And it does not say anything about how the integers relate to physical measurements or to the framework's later results about constants like the golden ratio. Those are separate claims with their own proofs and their own limits.

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

@[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

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

/-- **The additive analogue of the reciprocal fixed-point law.** The negation
involution fixes a forced difference exactly on the diagonal `a = b` — just as the
reciprocal involution fixes a forced ratio exactly on the unit `a = b`. The two
forced layers, integers and ratios, carry the same comparison geometry: an
involution that swaps two counts, fixed precisely where the counts agree. -/
theorem forced_difference_fixed_iff (a b : LogicNat) :
    (toInt a - toInt b = -(toInt a - toInt b)) ↔ a = b := by
  rw [forced_difference_neg_swap]
  constructor
  · intro h
    have hz : toInt a - toInt b = 0 := by omega
    exact (forced_difference_zero_iff a b).mp hz
  · intro h; subst h; ring

What this page does not claim

The integers are the only structure forced by the recognition ledger. The integers exist independently of the framework's logical postulates. The theorem says anything about how the integers relate to physical measurements or to the framework's later constants.

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: