Foundation Universal Forcing Canonical Forcing Forcing Equiv Unique

The canonical forcing map

A ledger, a discrete record of events, needs a way to count. Recognition Science starts from the idea that reality keeps such a ledger, and that the cost of recognition is forced, not chosen. From that starting point, the framework builds arithmetic objects it calls forced arithmetics, each with a zero and a successor step function, the raw material of counting. The question is whether two different such arithmetics, built from different logical realizations, are compatible. The declaration forcing_equiv_unique answers that question with a theorem: for any two forced arithmetics that share a carrier universe, there is exactly one bijection between their carriers that preserves zero and step.

This is a canonicity result, not a construction. The theorem does not build the map; it says that if two maps both preserve zero and step, they are the same function. The proof in the machine-checked library of formal theorems runs through a standard argument: any such map is a homomorphism of Peano objects, and the initiality of the natural numbers forces that homomorphism to be unique. The upshot is that the structure of counting is rigid. There is no representational freedom in how one forced arithmetic relates to another. Once you know where zero goes and how successor behaves, the entire map is determined.

The theorem comes in two forms. The general version, forcing_equiv_unique, works for any two realizations whose arithmetics share a carrier universe, a condition the library notes is always arrangeable. A stricter version, universal_forcing_equiv_unique, applies to the concrete strict realizations used in the main path. Both state the same fact: the forcing isomorphism is not an arbitrary choice among many, but the only structure morphism. The library packages this into a certificate, CanonicalForcingCert, which records that the map exists, preserves zero, preserves step, and is unique.

What the theorem does not claim is just as important. It does not say that the carrier universes themselves are identical, only that there is a unique map between them. It does not assert anything about the physical content of the ledger, only about the arithmetic built on it. And it does not prove that the cost function J(x) = (x + 1/x)/2 - 1 is unique; that is a separate theorem. The canonicity result is a structural fact about arithmetic, not a claim about physics. It is the kind of statement that makes the framework's larger claims possible, because it shows that the arithmetic forced by the ledger is not a matter of convention.

/-- **Uniqueness up to nothing** (general realizations): two equivalences that
both preserve zero and step are equal as functions. -/
theorem forcing_equiv_unique
    (A : ArithmeticOf.{u, v, w, w, w} R) (B : ArithmeticOf.{u', v', w, w, w} S)
    (e₁ e₂ : A.peano.carrier ≃ B.peano.carrier)
    (hz₁ : e₁ A.peano.zero = B.peano.zero)
    (hs₁ : ∀ x, e₁ (A.peano.step x) = B.peano.step (e₁ x))
    (hz₂ : e₂ A.peano.zero = B.peano.zero)
    (hs₂ : ∀ x, e₂ (A.peano.step x) = B.peano.step (e₂ x)) :
    (e₁ : A.peano.carrier → B.peano.carrier) = e₂ := by
  have h1 := forcing_map_unique A B (e₁ : A.peano.carrier → B.peano.carrier) hz₁ hs₁
  have h2 := forcing_map_unique A B (e₂ : A.peano.carrier → B.peano.carrier) hz₂ hs₂
  rw [h1, h2]

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

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

What this page does not claim

The theorem does not assert that two carrier universes are identical, only that a unique map exists between them. It does not claim anything about the physical content of the ledger, only about the arithmetic built on it. It does not prove the uniqueness of the cost function J(x) = (x + 1/x)/2 - 1, which is a separate result.

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: