Foundation Universal Forcing Forced Semiring Forcing Fn Unique

The unique arithmetic

The natural numbers, 0, 1, 2, 3 and so on, are usually taken as a starting point for mathematics. The theorem forcingFn_unique in the Recognition Science framework's machine-checked library of formal theorems says they are instead an unavoidable conclusion. The claim, in plain language, is this: if you have any structure that recognizes a starting point (zero) and a way to step from one item to the next (successor), then the way those items add and multiply is already fixed. You cannot choose a different arithmetic; there is only one.

The theorem is precise about what "cannot choose" means. One can have two such structures, each with its own zero and its own successor step. The framework's library proves there is exactly one map between them that sends zero to zero and commutes with the successor step. That map is called the forcing map. The theorem forcingFn_unique states that any function with those two properties must equal this forcing map. The library then shows this map preserves addition, multiplication, and the number one, and that it is a bijection, meaning it pairs up the two structures perfectly. The capstone result is that the forced arithmetic is isomorphic to the natural numbers themselves, as a structure with 0, 1, +, and ×.

The history of this idea runs through the Peano axioms, named after Giuseppe Peano, who in 1889 gave the standard axioms for the natural numbers using zero and successor. The framework's theorem is a different kind of claim. It does not posit those axioms; it derives the arithmetic from the mere requirement of a zero and a successor step, within its own formal system. The proof is carried out in a machine-checked library, meaning every step is verified by a computer, not by hand. This is a formal result about a specific construction, not a claim about how human beings learn to count.

What the theorem does not claim is just as important. It does not say that the natural numbers are the only possible structure with a zero and a successor. It says that within the framework's strict presentation, any two such structures are forced to have the same arithmetic. The library itself notes that on this strict path the forcing map is simply the identity function, because both structures use the same carrier set. The nontrivial content is in the general preservation lemmas and in the cross-carrier canonicity proved elsewhere. The theorem also does not claim that this forces the natural numbers in any physical or philosophical sense; it is a mathematical result about a specific formal setup.

/-- **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

/-- **The forcing map preserves addition.** -/
theorem forcingFn_add (R S : UniversalForcing.Strict.StrictLogicRealization.{0,0})
    (a b : LogicNat) :
    forcingFn R S (a + b) = forcingFn R S a + forcingFn R S b :=
  map_preserves_add (forcingFn R S) (forcingFn_zero R S) (forcingFn_succ R S) a b

/-- **The forcing map preserves multiplication.** -/
theorem forcingFn_mul (R S : UniversalForcing.Strict.StrictLogicRealization.{0,0})
    (a b : LogicNat) :
    forcingFn R S (a * b) = forcingFn R S a * forcingFn R S b :=
  map_preserves_mul (forcingFn R S) (forcingFn_zero R S) (forcingFn_succ R S) a b

/-- **The forcing map preserves one.** -/
theorem forcingFn_one (R S : UniversalForcing.Strict.StrictLogicRealization.{0,0}) :
    forcingFn R S 1 = 1 :=
  map_preserves_one (forcingFn R S) (forcingFn_zero R S) (forcingFn_succ R S)

/-- The forcing map is a bijection: it is the underlying function of the
universal-forcing equivalence. -/
theorem forcingFn_bijective (R S : UniversalForcing.Strict.StrictLogicRealization.{0,0}) :
    Function.Bijective (forcingFn R S) :=
  (UniversalForcing.Strict.StrictLogicRealization.universal_forcing.{0,0,0,0,0,0} R S).bijective

/-- The forced arithmetic is `ℕ`. -/
noncomputable def forcedArithmeticIsNat : ForcedArithmeticIsNat where
  toEquiv := LogicNat.equivNat
  map_zero := LogicNat.toNat_zero
  map_one := toNat_one
  map_add := LogicNat.toNat_add
  map_mul := LogicNat.toNat_mul

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

What this page does not claim

The theorem does not claim that the natural numbers are the only possible structure with a zero and a successor step. The theorem does not claim that the forcing map is nontrivial in the strict presentation; it is the identity there. The theorem does not claim that the natural numbers are forced in any physical or philosophical sense.

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: