Foundation Universal Forcing Forced Integers To Int Nonneg

The nonnegative embedding

In the Recognition Science framework, the basic objects of arithmetic are not chosen freely. They are forced: a discrete record of events, a ledger, whose structure is derived from a proved cost law rather than assumed. The declaration toInt_nonneg is a small but load-bearing theorem in that construction. It states that when a forced counting number is mapped into the ordinary integers by its iteration count, the result is always at least zero. In plainer terms: no matter how the ledger is built, its entries never represent a negative quantity.

The mapping itself, called toInt, is the canonical bridge from the framework's internal arithmetic to the integers a working mathematician already knows. It sends the forced zero to the integer 0, the forced one to the integer 1, and preserves addition and multiplication. The theorem toInt_nonneg adds the order property: the image of every forced number lies in the nonnegative half of the integer line. This is not a deep result on its own, but it is the kind of fact that must hold if the framework's arithmetic is to behave like ordinary counting. A structure that could map a positive construction to a negative integer would be unusable as a foundation.

The certificate that bundles these properties together, ForcedIntegersCert, also records that the embedding is injective, meaning distinct forced numbers stay distinct in the integers, and that every integer, including the negative ones, appears as a difference of two forced numbers. That last fact is the substantive one: the framework's arithmetic does not stop at the nonnegative half-line. By taking differences, it generates the full additive group of integers, so the ledger's reach extends to negative quantities even though its primitive entries never go below zero.

What toInt_nonneg does not claim is equally important. It says nothing about which integers the framework can reach directly; it only guarantees that the direct image is nonnegative. It does not assert that every nonnegative integer is the image of some forced number, though the surjectivity of differences implies a weaker related fact. And it makes no claim about the physical meaning of the integers it produces. The theorem is a formal guarantee about the internal arithmetic, not a statement about measurement, geometry, or the empirical content of the framework.

theorem toInt_nonneg (n : LogicNat) : 0 ≤ toInt n := by
  simp only [toInt]
  exact Int.natCast_nonneg _

@[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 theorem does not assert that every nonnegative integer is the image of some forced number. The theorem makes no claim about the physical meaning or empirical content of the integers it produces. The theorem does not establish that the framework's arithmetic is consistent or complete beyond the specific properties recorded in the certificate.

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: