Foundation Universal Forcing Forced Integers Forced Difference Zero Iff

The zero difference test

The integers are the numbers you get by counting: 0, 1, 2, and so on, together with their negatives. One of their oldest properties is that a difference like 7 minus 7 is zero, and that the only way a difference of two integers can be zero is when the two integers are the same. In ordinary arithmetic this is so obvious it hardly needs stating, but in a formal system built from first principles it is a fact that must be proved, because the system's definition of "number" may not match the everyday one.

The Recognition Science framework builds its own arithmetic from a primitive notion of recognition, a discrete record of events, and then asks what structure that arithmetic must have. Its library, a machine-checked collection of formal theorems, defines a forced number as an iteration count and embeds those counts into the usual integers by that count. The embedding preserves zero, one, addition, and multiplication, and it is injective: different counts stay different. The framework then proves the theorem forced_difference_zero_iff: for any two forced numbers a and b, the difference toInt(a) minus toInt(b) equals zero if and only if a equals b. In plain language, the zero test works exactly as it does for ordinary integers.

The theorem is not an isolated curiosity. It is part of a certificate that the forced arithmetic really does carry the full additive group of integers. Another theorem in the same file shows that every integer, positive, negative, or zero, can be written as a difference of two forced numbers. So the framework does not merely mimic a fragment of integer arithmetic; it reproduces the whole thing. The zero-difference theorem also mirrors a companion result about ratios: just as a ratio a over b equals 1 exactly when a equals b, a difference equals 0 exactly when the two counts agree. Both are cases of a single comparison geometry: an operation that swaps two counts, and is fixed precisely when the counts are equal.

What the theorem does not claim is just as important. It does not say that the framework's forced numbers are the only way to build the integers, nor that recognition is the true origin of ordinary counting. It establishes a structural fact inside the framework: if you define numbers as iteration counts, then the zero test for equality is forced, not chosen. The theorem is about the internal consistency of that construction, not about the metaphysical status of numbers outside it.

/-- A difference of forced numbers vanishes exactly on the diagonal: the additive
null locus is `a = b`, mirroring the multiplicative unit locus of `ForcedRatios`. -/
theorem forced_difference_zero_iff (a b : LogicNat) :
    toInt a - toInt b = 0 ↔ a = b := by
  constructor
  · intro h
    have : toInt a = toInt b := by omega
    exact toInt_injective this
  · intro h; subst h; 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

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

What this page does not claim

The theorem does not claim that forced numbers are the only possible foundation for the integers. It does not claim that recognition is the true origin of ordinary counting. It does not claim that the embedding is surjective onto the integers, only that its differences are.

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: