Foundation Universal Forcing Forced Integers To Int Mul

The integer embedding

The integers are the everyday numbers we use for counting and arithmetic: 0, 1, 2, and their negatives. They obey familiar rules, such as the fact that multiplying 2 by 3 gives 6. The Recognition Science framework builds its own collection of counting numbers, called forced numbers, from the idea that a recognition event is a discrete step in a ledger. The declaration toInt_mul is a formal theorem in the framework's machine-checked library of formal theorems. It states that when you map a forced number to an ordinary integer by its iteration count, the multiplication of two forced numbers maps to the multiplication of the corresponding integers. In plain terms, the forced arithmetic's multiplication is perfectly compatible with the multiplication we already know.

This compatibility is not assumed; it is proved. The proof works by expanding the definition of the mapping, using the fact that the underlying forced counting numbers already multiply correctly, and then applying the standard arithmetic of integers. The same style of proof establishes the analogous compatibility for addition, for the special numbers zero and one, and for the fact that the mapping never sends two different forced numbers to the same integer. Together, these theorems form a certificate: the forced arithmetic embeds into the integers while preserving all the basic operations.

The deeper point is structural. The framework's library also proves that every integer, including the negative ones, can be written as a difference of two forced numbers. Since the forced numbers themselves are built from nonnegative counts, this shows that the full additive group of integers, with its negatives, is forced into existence by the framework's own construction. The theorem toInt_mul is a load-bearing piece of that larger result: it guarantees that the multiplication structure of the forced layer matches the multiplication structure of the integers exactly, so the integer layer is not a mere approximation but a faithful copy.

What the theorem does not claim is just as important. It does not say that the forced numbers are the same objects as the integers, only that they can be mapped into them faithfully. It does not say that the framework derives the integers from nothing; it assumes the integers as the ambient number system in which the proof is carried out. And it does not say anything about which specific physical quantities take integer values in the framework; that is a separate question about how the framework's numbers are applied to the world.

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

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 derive the integers from a more primitive framework concept. The theorem does not assign integer values to any specific physical quantity. The theorem does not show that the forced numbers are identical to the integers, only that they embed into them.

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: