Foundation Universal Forcing Strict Realization Arith

The forced arithmetic

The natural numbers, 0, 1, 2, 3, and so on, are the counting numbers everyone meets first. They satisfy the Peano axioms: there is a starting point, every number has a successor, and different numbers have different successors. The declaration arith in the Recognition Science library proves that any structure meeting a small set of logical requirements must contain a copy of these counting numbers. The requirements are plain: the structure must support comparison, composition, an identity element, and a nontrivial generator. No counting data is supplied in advance.

The proof works by removing a loophole. An earlier version of the framework allowed a realization to carry its own internal orbit, a pre-chosen sequence of objects. The strict version forbids that. A strict realization supplies only the native comparison, composition, identity, invariance, and non-triviality data. From just those ingredients, the framework derives a free orbit uniformly as a ledger, a discrete record of repeated steps. The derived ledger is then interpreted in the realization's carrier by primitive recursion: the identity maps to the identity element, and each step composes the generator with the previous interpretation. This gives a canonical copy of the natural numbers inside every strict realization.

The key result is that this copy is unique up to isomorphism. Any two strict realizations have arithmetic carriers that are equivalent, and each is equivalent to the standard natural numbers. This is a forcing result: the arithmetic is not chosen, it is forced by the logical laws. The theorem is checked by a machine, meaning every step of the proof is verified by a computer program that allows no gaps. The declaration arith itself is the definition that extracts this arithmetic from a strict realization, and the equivalence theorem arith_equiv_logicNat states that the extracted arithmetic is canonically the same as the natural numbers.

What this does not claim is important. It does not claim that the natural numbers are the only possible arithmetic, nor that this proof constructs the usual arithmetic with addition and multiplication as we know them. It establishes a carrier set with a Peano structure, a starting point and a successor function. The full arithmetic operations, such as addition and multiplication, are built on top of this structure in the library, but the declaration arith itself is about the underlying carrier and its equivalence to the natural numbers. It also does not claim that any physical system is a strict realization; it claims only that if a system satisfies the logical requirements, then it must contain this arithmetic structure.

In Recognition Science, this result matters because it shows that arithmetic is not an assumption but a consequence. The framework's starting point is that reality keeps a ledger of recognition events, and the cost of recognition is forced. The strict realization theorem shows that the counting structure itself is forced by the same logical laws. This is one step in a chain that the framework uses to derive physical constants and the structure of space. The declaration arith is a load-bearing piece of that chain, establishing that the natural numbers are not a free choice but a logical necessity.

/-- Strict forced arithmetic is the arithmetic extracted from the derived
lightweight realization. -/
def arith (R : StrictLogicRealization) : ArithmeticOf (toLightweight R) :=
  arithmeticOf (toLightweight R)

/-- The strict free orbit is uniformly the `LogicNat` iteration object. -/
abbrev FreeOrbit (_R : StrictLogicRealization) : Type :=
  LogicNat

/-- Universal forcing for strict realizations. -/
noncomputable def universal_forcing (R S : StrictLogicRealization) :
    (arith R).peano.carrier ≃ (arith S).peano.carrier :=
  ArithmeticOf.equivOfInitial (arith R) (arith S)

What this page does not claim

The declaration does not construct the full arithmetic operations of addition and multiplication. The theorem does not claim that any particular physical system is a strict realization. The result does not prove that the natural numbers are the only possible arithmetic.

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