Foundation Ordered Logic Realization Ordered Arithmetic Invariant

The arithmetic invariant

Natural numbers are the counting numbers: 0, 1, 2, 3, and so on, with the usual order and arithmetic. A recognition event is a discrete record of a comparison, such as checking whether two items are equal. The framework's declaration ordered_arithmetic_invariant establishes a precise structural fact: the natural numbers, with their order and arithmetic, are the same regardless of which recognition ledger is used to construct them. It proves that any valid recognition ledger yields a copy of the natural numbers that is structurally identical to the one built from the simplest possible ledger, where equality costs 0 and inequality costs 1.

The proof works by showing that the arithmetic recovered from any recognition ledger is equivalent to the arithmetic recovered from the canonical ordered realization. This canonical realization assigns a cost of 0 when two numbers are equal and 1 when they differ, which is the minimal possible cost structure. The declaration then constructs an equivalence between the natural numbers as recovered from this canonical ledger and the natural numbers as recovered from any other ledger. A companion theorem, ordered_faithful, confirms that this recovery is faithful: distinct natural numbers remain distinct, and the successor function never collapses two numbers into one.

In Recognition Science, the framework models logic and arithmetic as emerging from recognition costs rather than being assumed as primitive. The declaration ordered_arithmetic_invariant is a central piece of that modeling choice: it shows that the framework's construction of arithmetic is stable, not dependent on which specific ledger is chosen. The natural numbers are not an accident of one particular cost function; they are invariant across all valid recognition ledgers. This means the framework's arithmetic is stable and well-defined, providing a foundation for further results that build on natural-number arithmetic.

The declaration does not claim that natural numbers are physically real or that the framework proves the existence of numbers in the external world. It establishes an internal structural equivalence within the framework's formal system. It also does not claim that all possible recognition ledgers yield the same arithmetic; the theorem applies to ledgers that satisfy the framework's conditions for being a valid logic realization. Finally, it does not claim that arithmetic is the only structure that can be recovered from recognition, nor does it address whether the natural numbers are unique in any broader mathematical sense.

/-- Ordered arithmetic is invariant with every realization. -/
noncomputable def ordered_arithmetic_invariant (R : LogicRealization.{0, 0}) :
    (UniversalForcing.arithmeticOf natOrderedRealization).peano.carrier
      ≃ (UniversalForcing.arithmeticOf R).peano.carrier :=
  ArithmeticOf.equivOfInitial
    (UniversalForcing.arithmeticOf natOrderedRealization)
    (UniversalForcing.arithmeticOf R)

/-- The ordered realization interprets arithmetic faithfully. -/
theorem ordered_faithful :
    LogicRealization.FaithfulArithmeticInterpretation natOrderedRealization where
  injective := by
    intro a b h
    exact (ArithmeticFromLogic.LogicNat.eq_iff_toNat_eq).mpr h
  zero_step_noncollapse := by
    intro n h
    have hnat := congrArg id h
    simp [natOrderedRealization] at hnat
    exact Nat.succ_ne_zero _ hnat.symm

/-- Equality cost on `Nat`. -/
def natCost (m n : Nat) : Nat :=
  if m = n then 0 else 1

What this page does not claim

The declaration does not claim that natural numbers exist physically or independently of the framework. It does not claim that every possible ledger yields the same arithmetic; only those satisfying the framework's logic realization conditions. It does not claim that arithmetic is the only structure recoverable from recognition.

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