Foundation Universal Forcing Strict Invariance Strict Peano Surface

The forced arithmetic surface

Peano arithmetic is the standard set of axioms for the natural numbers: zero, successor, and induction. The framework's machine-checked library of formal theorems proves that any strict realization of its logic, meaning any structure that satisfies the framework's native law data, carries a Peano surface: an arithmetic structure that obeys those axioms. The theorem strict_peano_surface states this directly: for every strict realization R, the arithmetic derived from R's native law data satisfies ArithmeticOf.PeanoSurface. In plain words, the framework forces arithmetic, not as an assumption but as a consequence of its own logical structure.

More strongly, the library shows that this arithmetic is unique up to canonical equivalence. The declaration strict_universal_forcing constructs, for any two strict realizations R and S, an equivalence between their Peano carriers. The docstring calls this "Strict Universal Forcing": all derived free orbits are canonically equivalent. The anchor strict_arith_universal_initial ties each realization's arithmetic to LogicNat, the framework's canonical natural-number object. So the claim is not merely that arithmetic exists, but that every strict realization's arithmetic is the same arithmetic, in a precise sense.

What this does not claim: it does not say that the framework derives Peano arithmetic from nothing. The theorem presupposes StrictLogicRealization, a structure with native law data. It does not claim that arbitrary logical systems force arithmetic; the theorem is restricted to strict realizations. It also does not claim that the Peano surface is unique in the sense of having no other models; it claims canonical equivalence among the arithmetic structures derived from strict realizations. The theorem is a statement about the framework's internal consistency, not about the foundations of mathematics at large.

In the framework's account, this result is a load-bearing step: it shows that the arithmetic used throughout the framework's derivations, including the forcing chain that leads to constants and dimensions, is not an ad hoc choice but a forced structure. The practical upshot for a reader is that when the framework speaks of numbers, it speaks of a specific, canonically determined arithmetic, one that any strict realization must reproduce.

/-- The Peano surface for every strict realization. -/
theorem strict_peano_surface (R : StrictLogicRealization) :
    ArithmeticOf.PeanoSurface (StrictLogicRealization.arith R) :=
  StrictLogicRealization.peano_surface R

/-- **Strict Universal Forcing.**

For any two strict Law-of-Logic realizations, the arithmetic derived from
their native law data is canonically equivalent. -/
noncomputable def strict_universal_forcing (R S : StrictLogicRealization) :
    (StrictLogicRealization.arith R).peano.carrier
      ≃ (StrictLogicRealization.arith S).peano.carrier :=
  ArithmeticOf.equivOfInitial (StrictLogicRealization.arith R)
    (StrictLogicRealization.arith S)

/-- Every strict realization's derived forced arithmetic is canonically
equivalent to `LogicNat`. -/
def strict_arith_universal_initial (R : StrictLogicRealization) :
    (StrictLogicRealization.arith R).peano.carrier ≃ ArithmeticFromLogic.LogicNat :=
  (StrictLogicRealization.toLightweight R).orbitEquivLogicNat

What this page does not claim

The theorem does not derive Peano arithmetic from no premises at all; it presupposes a StrictLogicRealization. It does not claim that every logical system forces arithmetic, only strict realizations. It does not claim uniqueness of the Peano model in the sense of categoricity; it claims canonical equivalence among derived arithmetic structures.

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/Strict/Invariance.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: