Foundation Universal Forcing Forced Integers To Int Add

Addition is preserved

In ordinary mathematics, the integers are the whole numbers ..., -2, -1, 0, 1, 2, ... with their usual addition and multiplication. The Recognition Science framework builds its own arithmetic from a discrete record of events, which it calls a ledger, a record that keeps a count of how many times something has happened. The declaration toInt_add is a theorem in the framework's machine-checked library of formal theorems. It states that if you take two of these counts, add them using the framework's own addition rule, and then translate the result into an ordinary integer, you get the same number as if you had translated each count first and then added the ordinary integers. In symbols, for any two counts a and b, the translation of (a + b) equals the translation of a plus the translation of b.

This is not a deep fact about the universe; it is a consistency check. The framework defines its counts, defines its addition, and then proves that this addition behaves exactly like the addition everyone already knows. The proof is short and mechanical: it unwraps the definitions, uses a previously established fact about how counts translate into natural numbers, and then rearranges the result. The theorem is one of several in a certificate, a bundled collection of properties, that together show the framework's counting objects are a faithful copy of the integers. The certificate also proves that multiplication is preserved, that the translation is one-to-one, and that every integer, including negative ones, can be written as a difference of two counts.

The point of this certificate is not to discover new arithmetic. It is to show that the framework's internal arithmetic does not secretly differ from the arithmetic used everywhere else. If the framework's counts added to something other than the ordinary sum, the whole structure would be suspect. The theorem closes that door. It is a small, unglamorous lemma, but it is the kind of lemma that a large edifice needs: a guarantee that the foundation is not quietly off by one.

In Recognition Science, this result is part of a larger story. The framework derives its arithmetic from the forced cost of recognition, and this certificate shows that the arithmetic it derives is the standard one. The framework models the integers as differences of counts, and this theorem confirms that the model is faithful. What the theorem does not claim is any new fact about the integers themselves. It does not prove that addition is associative or commutative; those are properties the framework inherits from the integers it embeds into. It does not claim that the framework's counts are the only way to build the integers, nor that the framework's derivation is the only path to them. It simply certifies that the path the framework takes arrives at the same destination.

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

/-- **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 prove any new property of the integers themselves, such as associativity or commutativity. The framework's counts are not claimed to be the only way to construct the integers. The theorem does not claim that the framework's derivation of arithmetic is the only possible derivation.

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: