Foundation Universal Forcing Forced Semiring Forcing Fn Eq Id

The identity map

The natural numbers, written ℕ, are the counting numbers 0, 1, 2, 3, and so on, with the operations of addition and multiplication. A semiring is a set with these two operations, obeying the usual distributive law. The declaration forcingFn_eq_id in the Recognition Science library proves that the canonical map between two strict realizations of ℕ is the identity function. In plainer terms: if you have two copies of the counting numbers, built in the framework's specific way, the only sensible way to translate between them is to send each number to itself.

The proof rests on a chain of lemmas. Any function that sends zero to zero and commutes with the successor step (the operation that takes n to n+1) must preserve addition, multiplication, and the number one. The forcing map, which is the canonical translation between two realizations, has exactly these two properties. Therefore it preserves all arithmetic structure. A separate theorem, forcingFn_unique, shows that any function with these two properties must equal the forcing map. Since the identity function also fixes zero and commutes with successor, the forcing map must be the identity.

This result is a theorem in the machine-checked library, meaning it is proved from the framework's axioms without gaps. It is not a definition or a modeling choice. The theorem does not claim that the natural numbers are the only possible arithmetic, nor does it say anything about how the framework derives the natural numbers from first principles. The honest note in the library states that on the strict path, the two realizations use the same carrier, so the map being the identity is expected. The non-trivial content lies in the general preservation lemmas and the cross-carrier canonicity, not in this specific identity.

/-- The forced-semiring certificate holds. -/
noncomputable def forcedSemiringCert_holds : ForcedSemiringCert where
  map := forcingFn
  bij := forcingFn_bijective
  zero := forcingFn_zero
  one := forcingFn_one
  add := forcingFn_add
  mul := forcingFn_mul
  unique := forcingFn_unique

/-! ## Honest note: on the strict path the forcing map is the identity.

`StrictLogicRealization` uses a uniform free orbit (`LogicNat`) for every
realization, so the two forced arithmetics are literally the same carrier and the
canonical map between them is the identity. This does not trivialize the theory:
the non-trivial content is (a) the general preservation lemmas above, which apply
to *any* zero/step map, and (b) the cross-carrier canonicity in
`CanonicalForcing.ArithmeticOf.forcing_map_unique`. It is simply honest about the
strict presentation. -/
theorem forcingFn_eq_id (R S : UniversalForcing.Strict.StrictLogicRealization.{0,0}) :
    forcingFn R S = id :=
  (forcingFn_unique R S id rfl (fun _ => rfl)).symm

/-- A map fixing zero and commuting with `succ` preserves addition. Addition
recurses on its second argument, so the proof is a single induction. -/
theorem map_preserves_add (h : LogicNat → LogicNat)
    (h0 : h LogicNat.zero = LogicNat.zero)
    (hs : ∀ n, h (LogicNat.succ n) = LogicNat.succ (h n)) :
    ∀ a b : LogicNat, h (a + b) = h a + h b := by
  intro a b
  induction b with
  | identity =>
      show h (a + LogicNat.zero) = h a + h LogicNat.zero
      rw [add_zero, h0, add_zero]
  | step b ih =>
      show h (a + LogicNat.succ b) = h a + h (LogicNat.succ b)
      rw [add_succ, hs, ih, hs, add_succ]

/-- A map fixing zero and commuting with `succ` (hence, by the previous lemma,
preserving `+`) preserves multiplication. Multiplication recurses on its second
argument via addition. -/
theorem map_preserves_mul (h : LogicNat → LogicNat)
    (h0 : h LogicNat.zero = LogicNat.zero)
    (hs : ∀ n, h (LogicNat.succ n) = LogicNat.succ (h n)) :
    ∀ a b : LogicNat, h (a * b) = h a * h b := by
  have hadd := map_preserves_add h h0 hs
  intro a b
  induction b with
  | identity =>
      show h (a * LogicNat.zero) = h a * h LogicNat.zero
      rw [mul_zero, h0, mul_zero]
  | step b ih =>
      show h (a * LogicNat.succ b) = h a * h (LogicNat.succ b)
      rw [mul_succ, hadd, ih, hs, mul_succ]

/-- **Uniqueness as a semiring map.** Any function preserving zero and step
equals the forcing map, so in particular the forcing map is the unique semiring
homomorphism — it is determined, not chosen. (Restated from canonicity for the
`LogicNat` presentation.) -/
theorem forcingFn_unique (R S : UniversalForcing.Strict.StrictLogicRealization.{0,0})
    (f : LogicNat → LogicNat)
    (h0 : f LogicNat.zero = LogicNat.zero)
    (hs : ∀ n, f (LogicNat.succ n) = LogicNat.succ (f n)) :
    f = forcingFn R S :=
  UniversalForcing.Strict.StrictLogicRealization.universal_forcing_unique R S f h0 hs

What this page does not claim

This theorem does not claim that the natural numbers are the only possible arithmetic structure. This theorem does not derive the natural numbers from first principles; it only shows a map between two realizations is the identity. This theorem does not apply to non-strict realizations where the carriers may differ.

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/ForcedSemiring.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: