Foundation Universal Forcing Canonical Forcing Universal Forcing Equiv Unique

The canonical map

In mathematics, a Peano structure is a way of building numbers from a starting point, usually called zero, and a next-number operation, usually called successor. The natural numbers are the classic example: start at zero, and keep taking successors to get one, two, three, and so on. The key fact about any two such structures is that there is a natural way to match them up. The map sends zero to zero, and sends the successor of any number to the successor of that number's image. This is how we know that counting with tally marks, counting with fingers, and counting with a computer's binary arithmetic are all the same activity.

The theorem universal_forcing_equiv_unique in the framework's machine-checked library of formal theorems proves a sharper version of this matching fact. It considers two arithmetic systems that both arise from the framework's forcing construction, which builds arithmetic from the logic of recognition events. The theorem states that if you have two equivalences between these systems, and both equivalences preserve zero and preserve the successor operation, then those two equivalences are actually the same function. In other words, there is no choice involved in translating between the two systems. The structure-preserving map is unique, so the arithmetic is canonical rather than representational.

The proof works by using a stronger uniqueness result. Any function that preserves zero and successor is forced to be the canonical map; there is no room for a different function that still respects the structure. The theorem also comes with a companion result, universal_forcing_iff, which says that a function is the canonical map if and only if it preserves zero and successor. Together these results give a complete characterization: the only structure-preserving maps are the canonical ones, and there is exactly one such map for each pair of systems.

What this does not claim is important. The theorem does not say that any two arithmetic systems are identical, only that there is a unique way to translate between them. It does not say that the framework's forcing construction is the only way to build arithmetic, only that within the framework, any two realizations that share a carrier universe are canonically equivalent. The theorem also does not make any empirical claims about the physical world; it is a purely formal statement about mathematical structures. It establishes a uniqueness property, not a physical law.

/-- **Uniqueness up to nothing.** Two equivalences that both preserve zero and
step are equal as functions. The forcing isomorphism is not "an" iso among many;
it is the only structure morphism, hence canonical. -/
theorem universal_forcing_equiv_unique (R S : StrictLogicRealization.{0,0})
    (e₁ e₂ : (arith.{0,0,0} R).peano.carrier ≃ (arith.{0,0,0} S).peano.carrier)
    (hz₁ : e₁ (arith.{0,0,0} R).peano.zero = (arith.{0,0,0} S).peano.zero)
    (hs₁ : ∀ x, e₁ ((arith.{0,0,0} R).peano.step x) = (arith.{0,0,0} S).peano.step (e₁ x))
    (hz₂ : e₂ (arith.{0,0,0} R).peano.zero = (arith.{0,0,0} S).peano.zero)
    (hs₂ : ∀ x, e₂ ((arith.{0,0,0} R).peano.step x) = (arith.{0,0,0} S).peano.step (e₂ x)) :
    (e₁ : (arith.{0,0,0} R).peano.carrier → (arith.{0,0,0} S).peano.carrier) = e₂ := by
  have h1 := universal_forcing_unique R S
      (e₁ : (arith.{0,0,0} R).peano.carrier → (arith.{0,0,0} S).peano.carrier) hz₁ hs₁
  have h2 := universal_forcing_unique R S
      (e₂ : (arith.{0,0,0} R).peano.carrier → (arith.{0,0,0} S).peano.carrier) hz₂ hs₂
  rw [h1, h2]

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

What this page does not claim

The theorem does not claim that any two arithmetic systems are identical, only that there is a unique translation between them. The theorem does not claim that the framework's forcing construction is the only way to build arithmetic. The theorem makes no empirical claims about the physical world.

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: