Foundation Universal Forcing Strict Realization Free Orbit

The free orbit

In the Recognition Science framework, a realization is a mathematical structure that supplies the basic operations of comparison, composition, and identity, together with a distinguished generator. The framework's Universal Forcing theorem shows that any such structure, if it satisfies the right axioms, must contain an arithmetic that is essentially the natural numbers. The earlier, lightweight version of the theorem allowed a realization to carry its own internal orbit, a pre-supplied set of iterates that the theorem would then use. That left a loophole: the arithmetic could be imported rather than derived from the structural axioms.

The declaration FreeOrbit closes that loophole. It defines the orbit of a strict realization to be, uniformly, the object LogicNat, which is the framework's own construction of the natural numbers from the primitive generator and composition operation. In plain language: a strict realization cannot bring its own counting sequence; it must use the one that the framework builds from the native data. The accompanying function interpret maps this free orbit into the realization's carrier by primitive recursion: the identity element is the base case, and each successor step composes the generator with the previous result. Theorems interpret_zero and interpret_step state these two reduction rules, and they hold by definitional equality, meaning they are true simply because of how the terms are defined.

What this establishes is that the counting numbers are not an optional extra in a strict realization. They are forced: any strict realization, whatever its carrier, has an arithmetic canonically equivalent to LogicNat, as shown by the definition arith_equiv_logicNat. The universal forcing theorem then extends this to show that the arithmetic of any two strict realizations are equivalent, and the Peano surface, the structure of successor and induction, is inherited from the derived free orbit. The practical effect is that the framework's arithmetic is uniform and unavoidable, not a choice the modeler makes.

What FreeOrbit does not claim is just as important. It does not claim that the natural numbers are the only possible arithmetic in any absolute sense; it claims that within this framework, under the strict realization interface, they are the only one derived from the axioms. It does not claim that the generator or composition operation are unique, only that the orbit built from them is. And it does not claim that the framework's arithmetic matches the arithmetic of ordinary mathematics in every respect; the equivalence is to the framework's own LogicNat, not to an external standard. The declaration is a structural guarantee, not a philosophical statement about the nature of numbers.

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

@[simp] theorem interpret_zero (R : StrictLogicRealization) :
    interpret R LogicNat.zero = R.one := rfl

@[simp] theorem interpret_step (R : StrictLogicRealization) (n : FreeOrbit R) :
    interpret R (LogicNat.succ n) = R.compose R.generator (interpret R n) := rfl

/-- Every strict realization has forced arithmetic canonically equivalent to
`LogicNat`. -/
def arith_equiv_logicNat (R : StrictLogicRealization) :
    (arith R).peano.carrier ≃ LogicNat :=
  (toLightweight R).orbitEquivLogicNat

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

/-- The Peano surface is inherited from the derived free orbit. -/
theorem peano_surface (R : StrictLogicRealization) :
    ArithmeticOf.PeanoSurface (arith R) :=
  UniversalForcing.peano_surface (toLightweight R)

What this page does not claim

The natural numbers are the only possible arithmetic in any absolute sense. The generator or composition operation are unique. The framework's arithmetic matches ordinary arithmetic in every respect. The free orbit is a physical claim about counting in the 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/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: