Foundation Universal Forcing Order Realization Int Orbit Interpret

The integer reading

The declaration intOrbitInterpret is a translation rule. It takes a natural number, the kind of counting step used in the framework's internal arithmetic, and reads it as the same number in the usual integer system. The map sends 0 to 0, 1 to 1, 2 to 2, and so on. Nothing is lost and nothing is added: the definition is the identity embedding of the nonnegative numbers into the integers.

This sits inside a larger construction called orderRealization, a concrete model of the framework's notion of a ledger, a discrete record of events. The model uses a simple cost rule: comparing two integers costs 0 if they are equal and 1 otherwise. The library proves this cost is symmetric, meaning the cost of going from a to b is the same as from b to a. The integer reading is the carrier for this model, the set of objects the cost acts on.

What the declaration establishes is modest but precise. It shows that the framework's abstract counting steps can be carried by ordinary integers without changing their meaning. The library also proves that this ordered model carries the universal forced arithmetic, meaning any other model in the framework has a structure-preserving map from this one. That is a formal statement about how this concrete example relates to every other example.

What it does not claim is more important than what it does. The declaration does not say that the integers are the only possible carrier, nor that this model is the framework's preferred one. It does not assert that the integers themselves are forced by the framework's axioms. It is one realization among many, a working example that lets the framework's abstract machinery run on a familiar number system. The definition is a tool, not a conclusion.

/-- Interpret `LogicNat` as nonnegative integers. -/
def intOrbitInterpret (n : LogicNat) : ℤ :=
  (LogicNat.toNat n : ℤ)

theorem intCost_symm (a b : ℤ) : intCost a b = intCost b a := by
  by_cases h : a = b
  · subst h; simp [intCost]
  · have h' : b ≠ a := by intro hb; exact h hb.symm
    simp [intCost, h, h']

/-- Ordered realization carries the universal forced arithmetic. -/
noncomputable def order_arithmetic_invariant (R : LogicRealization.{0, 0}) :
    (arithmeticOf orderRealization).peano.carrier ≃ (arithmeticOf R).peano.carrier :=
  ArithmeticOf.equivOfInitial (arithmeticOf orderRealization) (arithmeticOf R)

What this page does not claim

The integers are the only possible carrier for the framework's arithmetic. The framework forces the integers themselves as a mathematical object. This declaration establishes anything about the physical interpretation of the framework.

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