Foundation Universal Forcing Forced Semiring Map Preserves One

The one that is forced

The natural numbers are the counting numbers: zero, then one, then two, and so on, each produced by a single step from the one before. A function that maps natural numbers to natural numbers is called zero-preserving if it sends zero to zero, and step-preserving if it sends each number to the image of its successor. The theorem map_preserves_one states that any such function must also send one to one. The proof is immediate: one is defined as the successor of zero, so a step-preserving map sends one to the successor of the image of zero, which is the successor of zero, namely one.

This small fact is the third link in a chain. The same two hypotheses, zero-preserving and step-preserving, already force the map to respect addition and multiplication. Addition recurses on its second argument, so the proof that addition is preserved is a single induction. Multiplication recurses via addition, so it follows from the first result. The preservation of one is then the special case where the second argument is zero. Together these three results mean that any zero-preserving, step-preserving map is a semiring homomorphism: it respects the entire arithmetic structure of zero, one, addition, and multiplication.

In Recognition Science, the framework models a ledger as a discrete record of events, and the natural numbers arise as the forced structure of distinction. The framework's library, a machine-checked collection of formal theorems, shows that the canonical map between any two strict realizations of this ledger is exactly such a zero-preserving, step-preserving function. Therefore that canonical map preserves one, along with all the rest of the arithmetic. The framework presents this as a certificate that distinction forces the natural numbers themselves, with no base, no positional notation, and no arithmetic axioms posited.

What the theorem does not claim is more interesting. It does not say that one is a special number with intrinsic importance; it says that one is unavoidable once zero and the successor operation are fixed. It does not say that every map preserving one must preserve zero and step; the implication runs in the other direction. And in the strict presentation, the canonical map between two realizations is literally the identity function, because both realizations use the same carrier. The nontrivial content is the general preservation lemma, which applies to any zero-preserving, step-preserving map, not just the canonical one.

/-- A zero/step-preserving map fixes `1 = succ 0`. -/
theorem map_preserves_one (h : LogicNat → LogicNat)
    (h0 : h LogicNat.zero = LogicNat.zero)
    (hs : ∀ n, h (LogicNat.succ n) = LogicNat.succ (h n)) :
    h 1 = 1 := by
  show h (LogicNat.succ LogicNat.zero) = LogicNat.succ LogicNat.zero
  rw [hs, h0]

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

The theorem does not claim that one has intrinsic importance beyond being the successor of zero. It does not claim that preserving one alone forces zero and step preservation. It does not claim that the strict presentation's identity map is the interesting case; the general lemma is.

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: