Foundation Universal Forcing Canonical Forcing Universal Forcing Iff

The canonical map

In mathematics, a Peano system is a set with a distinguished starting element, usually called zero, and a successor operation that moves from one element to the next. The natural numbers, with zero and the operation of adding one, are the standard example. A structure-preserving map between two such systems is a function that sends the first system's zero to the second system's zero, and that commutes with the successor operation: applying the function after a step gives the same result as stepping after the function.

The Recognition Science framework builds arithmetic systems from its own foundational principles, and its machine-checked library of formal theorems proves a strong uniqueness result about them. The theorem universal_forcing_iff states that a function between two such forced arithmetic systems is the canonical structure-preserving map if and only if it preserves zero and the successor operation. This is a complete characterization: the condition of preserving the basic structure is both necessary and sufficient for being the unique map.

The force of the result is not that such a map exists, but that it is unique. Any function that respects the zero and the successor operation must be the same function. The library proves this by showing that the map built from the initial structure of one system into the other is the only possible structure morphism. There is no representational freedom: the arithmetic structure determines the map completely.

In Recognition Science, this is called the universal forcing objective. It applies to any two realizations of the framework's logic, even when their carrier sets are genuinely different objects. The theorem is proved for the strict, universe-zero case, where the carrier is a concrete logical natural number type, and also for the general case where the carrier universes are shared. The general version is stated for any two realizations whose forced arithmetics share a carrier universe, which is always arrangeable since the carrier universe is a free parameter.

The theorem does not claim that the framework derives the natural numbers from nothing, nor that it proves the consistency of arithmetic. It does not claim that the map is the identity function; in the general case the two carrier sets may be different, and the map is a nontrivial isomorphism. It also does not claim that the framework's arithmetic is the only possible arithmetic, only that within the framework, any two forced arithmetics are canonically equivalent.

/-- Complete characterization: a map is the forcing map iff it preserves zero and
step. -/
theorem universal_forcing_iff (R S : StrictLogicRealization.{0,0})
    (f : (arith.{0,0,0} R).peano.carrier → (arith.{0,0,0} S).peano.carrier) :
    (f (arith.{0,0,0} R).peano.zero = (arith.{0,0,0} S).peano.zero
        ∧ ∀ x, f ((arith.{0,0,0} R).peano.step x) = (arith.{0,0,0} S).peano.step (f x))
      ↔ f = (universal_forcing.{0,0,0,0,0,0} R S).toFun := by
  constructor
  · rintro ⟨hz, hs⟩
    exact universal_forcing_unique R S f hz hs
  · rintro rfl
    exact ⟨universal_forcing_map_zero R S, universal_forcing_map_step R S⟩

/-- **General canonicity.** Any function preserving zero and step between two
forced arithmetics (sharing a carrier universe) *is* the forcing map. The map is
determined by the zero/step data alone — no representational freedom. -/
theorem forcing_map_unique
    (A : ArithmeticOf.{u, v, w, w, w} R) (B : ArithmeticOf.{u', v', w, w, w} S)
    (f : A.peano.carrier → B.peano.carrier)
    (hz : f A.peano.zero = B.peano.zero)
    (hs : ∀ x, f (A.peano.step x) = B.peano.step (f x)) :
    f = (equivOfInitial A B).toFun := by
  have h := A.initial.uniq B.peano
      (⟨f, hz, hs⟩ : PeanoObject.Hom A.peano B.peano) (A.initial.lift B.peano)
  simpa [equivOfInitial] using h

/-- **The Universal-Forcing objective at full generality.** For *any* two
Law-of-Logic realizations `R`, `S` (in arbitrary universes) and any forced
arithmetics `A` over `R`, `B` over `S` sharing a carrier universe, there is a
structure-preserving equivalence between the carriers that is *the unique*
zero/step-preserving map. This is the precise content of
`universal-forcing-program.mdc`'s "canonical equivalence of `ArithmeticOf R` and
`ArithmeticOf S` across admissible realizations": not bare existence of some
iso, but a canonical, determined morphism.

Unlike the strict-realization certificate below (where the carrier is concretely
`LogicNat` and the map is the identity), here `A.peano.carrier` and
`B.peano.carrier` may be genuinely different Peano objects, so the equivalence is
a nontrivial iso — yet still the only structure morphism between them. -/
theorem universal_objective
    (A : ArithmeticOf.{u, v, w, w, w} R) (B : ArithmeticOf.{u', v', w, w, w} S) :
    ∃ e : A.peano.carrier ≃ B.peano.carrier,
      e A.peano.zero = B.peano.zero
      ∧ (∀ x, e (A.peano.step x) = B.peano.step (e x))
      ∧ (∀ f : A.peano.carrier → B.peano.carrier,
            f A.peano.zero = B.peano.zero →
            (∀ x, f (A.peano.step x) = B.peano.step (f x)) →
            f = e.toFun) :=
  ⟨equivOfInitial A B,
   equivOfInitial_map_zero A B,
   equivOfInitial_map_step A B,
   fun f hz hs => forcing_map_unique A B f hz hs⟩

What this page does not claim

The theorem does not prove that the natural numbers are the only possible arithmetic system. The theorem does not claim that the canonical map is the identity function. The theorem does not establish the consistency of the framework's logic.

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