Foundation Universal Forcing Strict Invariance Strict Arith Universal Initial

The universal arithmetic

The natural numbers, 0, 1, 2, 3, and so on, are the counting numbers everyone learns first. A ledger, a discrete record of events, needs them to count its entries. The question at stake is whether different ways of building a logical system from scratch could produce different number systems, or whether the counting numbers are forced to be the same no matter how the system is constructed.

The framework's machine-checked library of formal theorems answers this for a specific class of systems it calls strict realizations. A strict realization is a logical structure built from the native law-of-logic data, meaning the basic rules of reasoning themselves, with no extra assumptions added. The declaration strict_arith_universal_initial establishes that for any such strict realization, the arithmetic derived from its native law data is canonically equivalent to a fixed reference system called LogicNat. In plain terms: every strict realization generates the same natural numbers, and the equivalence between them is canonical, meaning it is unique and natural rather than chosen arbitrarily.

The companion declaration strict_universal_forcing extends this to any two strict realizations. It proves that the arithmetic derived from one strict realization is canonically equivalent to the arithmetic derived from any other. This is the universal forcing result: the counting numbers are not a matter of design choice within the framework. Once the strict law-of-logic data is fixed, the natural numbers are forced, and every strict realization agrees on them.

What this does not claim is important. It does not claim that all logical systems whatsoever produce the same arithmetic. The result is scoped to strict realizations, which satisfy specific conditions in the framework. It does not claim that the natural numbers are the only arithmetic structure possible, only that within this class of systems they are unique up to canonical equivalence. It also does not claim anything about the physical world directly; it is a theorem about the framework's logical structures, not an empirical statement about counting in the universe.

The consequence is that the framework's arithmetic is not an arbitrary choice. When the framework later builds physics on top of this arithmetic, the natural numbers it uses are the ones forced by the logic itself, not a convenient selection. This gives the framework's subsequent constructions a fixed foundation: the counting numbers are the same for every strict realization, so any result built on them inherits that universality.

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

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

What this page does not claim

All logical systems whatsoever produce the same arithmetic. The natural numbers are the only arithmetic structure possible. Any empirical claim about counting in the physical universe.

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: