Foundation Universal Forcing Canonical Iso Peano Equiv

Canonical number systems

Peano arithmetic is the simplest formal system for counting: it has a starting point, zero, and a successor operation that moves from one number to the next. A Peano algebra is any structure carrying exactly those two ingredients. An isomorphism between two such algebras is a bijection that preserves both: it sends zero to zero and commutes with the successor step. The declaration PeanoEquiv packages this notion as a bundled structure: a carrier equivalence together with proofs that it respects zero and step.

In the Recognition Science framework, the cost of recognition is forced by a proved theorem, and from that cost the framework derives arithmetic as a consequence of any realization of the underlying logic. The framework's library of machine-checked formal theorems proves that for any two such realizations, the universal forcing bijection between their forced arithmetics is not merely a set bijection but a Peano homomorphism: it sends the forced zero to the forced zero, and it commutes with the forced step map. This upgrades the earlier invariant from a bare carrier bijection to a structure-preserving isomorphism of Peano algebras.

The key theorem, peanoEquiv_unique, states that any two structure-preserving isomorphisms between the same pair of forced arithmetics have the same underlying function. The isomorphism is therefore canonical: not merely some isomorphism, but the unique one. The certificate UniversalForcingIsoCert quantifies this over all realizations, asserting that for any two realizations there is a canonical Peano-algebra isomorphism between their forced arithmetics, and that isomorphism is unique.

What PeanoEquiv does not claim is equally precise. It does not preserve the ring operations of addition and multiplication, nor the order relation ≤, because the underlying PeanoObject carries only zero and step. The richer ordered-semiring isomorphism remains open work toward the full arithmetic-extraction layer. The framework's canonicality result is a theorem about Peano algebras, not about the full structure of arithmetic.

/-- The universal forcing bijection sends the forced zero to the forced zero. -/
theorem equivOfInitial_map_zero (R : LogicRealization.{u, v}) (S : LogicRealization.{u, w}) :
    (ArithmeticOf.equivOfInitial (forcedArith R) (forcedArith S))
        (forcedArith R).peano.zero
      = (forcedArith S).peano.zero :=
  ((forcedArith R).initial.lift (forcedArith S).peano).map_zero

/-- The universal forcing bijection commutes with the forced step map. -/
theorem equivOfInitial_map_step (R : LogicRealization.{u, v}) (S : LogicRealization.{u, w})
    (x : (forcedArith R).peano.carrier) :
    (ArithmeticOf.equivOfInitial (forcedArith R) (forcedArith S))
        ((forcedArith R).peano.step x)
      = (forcedArith S).peano.step
          ((ArithmeticOf.equivOfInitial (forcedArith R) (forcedArith S)) x) :=
  ((forcedArith R).initial.lift (forcedArith S).peano).map_step x

/-- **Canonicality.**  Any two structure-preserving isomorphisms between the
forced arithmetics of two realizations have the same underlying function.  The
isomorphism furnished by Universal Forcing is therefore the unique one. -/
theorem peanoEquiv_unique (R : LogicRealization.{u, v}) (S : LogicRealization.{u, w})
    (e₁ e₂ : PeanoEquiv (forcedArith R).peano (forcedArith S).peano) :
    (e₁.toEquiv : (forcedArith R).peano.carrier → (forcedArith S).peano.carrier)
      = (e₂.toEquiv : (forcedArith R).peano.carrier → (forcedArith S).peano.carrier) :=
  (forcedArith R).initial.uniq (forcedArith S).peano e₁.toHom e₂.toHom

/-- **Universal Forcing isomorphism certificate.**

For any two Law-of-Logic realizations, there is a canonical structure-preserving
isomorphism between their forced arithmetics, and that isomorphism is unique. -/
structure UniversalForcingIsoCert where
  /-- The canonical Peano-algebra isomorphism between any two forced arithmetics. -/
  iso : ∀ R S : LogicRealization.{0, 0},
    PeanoEquiv (forcedArith R).peano (forcedArith S).peano
  /-- That isomorphism is unique as a structure-preserving map. -/
  unique : ∀ (R S : LogicRealization.{0, 0})
      (e₁ e₂ : PeanoEquiv (forcedArith R).peano (forcedArith S).peano),
      (e₁.toEquiv : (forcedArith R).peano.carrier → (forcedArith S).peano.carrier)
        = e₂.toEquiv

What this page does not claim

The Peano isomorphism preserves the ring operations of addition and multiplication or the order relation. The framework derives the full structure of arithmetic, including ordered-semiring properties, from the Peano-algebra layer. The canonicality theorem applies to structures beyond Peano algebras, such as rings or ordered fields.

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