Foundation Universal Forcing Natural Number Object Realization Orbit Equiv Logic

The forced arithmetic

The natural numbers, 0, 1, 2, and so on, are the first thing any counting system needs. The classical definition, due to William Lawvere in 1963, says a natural-number object is a starting point together with a "next" operation, such that from any other starting point and any other "next" operation there is exactly one way to translate the first system into the second. This universal property is what makes the naturals the canonical counting system: any structure satisfying it is essentially the same as ℕ.

The Recognition Science framework starts from a different place: a ledger, a discrete record of events, whose cost of recognition is forced by logic alone. The framework's library, a machine-checked collection of formal theorems, shows that any such ledger must generate an arithmetic. The declaration realizationOrbit_equiv_logicNat states that this forced arithmetic is a natural-number object in the Lawvere sense, and that it is canonically equivalent to the standard natural numbers. In plain terms: whatever the ledger's underlying material is, the counting it produces is the same counting everyone uses.

The sharpest test is the Boolean realization, where the ledger's carrier has only two elements, false and true. A naive reading says such a ledger cannot count past two. The framework's theorem interpret_eq_parity shows the interpretation map collapses infinitely many steps onto two values, exactly the parity map: even steps land on false, odd on true. Yet the iteration object itself never collapses; it remains the full natural-number object, identical to the one in the continuous realization. The counting survives even when the visible states do not.

This is the formal answer to a standard objection: that the framework smuggled in ℕ by counting iterations. The theorem shows the iteration object is not an extra assumption but the unique structure forced by the ledger's own logic, and it is the same in every realization. The framework's contribution is not a new arithmetic; it is the proof that the arithmetic could not be otherwise.

What the declaration does not claim is just as important. It does not say the natural numbers are physically real, nor that the framework derives the specific values of physical constants from counting alone. It establishes a structural fact about the framework's own constructions: the forced arithmetic is the standard one. The theorem is about the framework's internal logic, not about the external world.

/-- The forced arithmetic of every realization is canonically equivalent to
`LogicNat`. This is the Universal Forcing statement at the natural-number
object level: every Law-of-Logic realization carries the same NNO. -/
noncomputable def realizationOrbit_equiv_logicNat (R : LogicRealization.{0, 0}) :
    R.Orbit ≃ LogicNat :=
  IsNaturalNumberObject.equiv (realizationOrbit_isNNO R) logicNat_isNNO

/-- The Boolean strict-realization interpretation is the parity map.

This is the formal statement that the iteration count survives even when
the orbit-as-set collapses to `{false, true}`. -/
theorem interpret_eq_parity (n : LogicNat) :
    StrictLogicRealization.interpret strictBooleanRealization n =
      Nat.bodd (LogicNat.toNat n) := by
  induction n with
  | identity => rfl
  | step n ih =>
      show xorBool true (StrictLogicRealization.interpret strictBooleanRealization n) =
        Nat.bodd (Nat.succ (LogicNat.toNat n))
      rw [xorBool_true, ih, Nat.bodd_succ]

/-- Despite the carrier collapse, the iteration object is itself a
natural-number object — the same one as in the continuous positive-ratio
realization. -/
def boolean_freeOrbit_isNNO :
    IsNaturalNumberObject
      (N := StrictLogicRealization.FreeOrbit strictBooleanRealization)
      LogicNat.identity LogicNat.step :=
  logicNat_isNNO

What this page does not claim

The natural numbers are physically real or exist independently of the framework. The framework derives specific physical constants from the natural-number object theorem alone. The Boolean realization's carrier set contains more than two elements.

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