Foundation Universal Forcing Forced Semiring Forcing Fn Succ

The step-preserving map

In the Recognition Science framework, a recognition event is a discrete record of a distinction being made. The framework's library of formal theorems works with a carrier called LogicNat, a structure meant to capture the bare idea of counting without any arithmetic axioms. The declaration forcingFn_succ is a theorem about the canonical map between two such structures. It states that if forcingFn is the map from one strict realization to another, then for any number n, the image of the successor of n is the successor of the image of n. In plainer terms, the map sends each number to its successor: it preserves the act of stepping forward.

This single property, together with the companion theorem that the map fixes zero, is enough to force the entire arithmetic structure. The library proves that any map which fixes zero and commutes with the successor function must preserve addition, multiplication, and the number one. The successor step is the seed; the rest of arithmetic grows from it. The framework's certificate bundles these results: the canonical map is a bijection, and it is the unique zero/step-preserving map. The forced object is, up to canonical isomorphism, exactly the natural numbers with their usual operations.

The framework is honest about a subtlety: on the strict path it uses, every realization has the same carrier, so the canonical map is literally the identity function. The theorem forcingFn_eq_id states this directly. This does not trivialize the theory. The preservation lemmas apply to any zero/step map, not just the identity, and the cross-carrier canonicity lives in a separate module. The strict presentation is a deliberate simplification, not a hidden assumption.

What the declaration does not claim is as important as what it proves. It does not claim that the natural numbers are the only possible arithmetic, nor does it claim anything about the physical world. It establishes a structural fact within a formal system: a map that respects the successor step is uniquely determined and preserves the arithmetic built on it. The theorem is a piece of pure mathematics, machine-checked, with no empirical content.

theorem forcingFn_succ (R S : UniversalForcing.Strict.StrictLogicRealization.{0,0}) (n : LogicNat) :
    forcingFn R S (LogicNat.succ n) = LogicNat.succ (forcingFn R S n) :=
  UniversalForcing.Strict.StrictLogicRealization.universal_forcing_map_step R S n

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

/-- **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 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 the natural numbers are the only possible arithmetic. The theorem does not claim any empirical fact about the physical world. The theorem does not claim the strict presentation is the only one; it is a deliberate simplification.

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: