Foundation Universal Forcing Discrete Realization Discrete Arith Equiv Logic Nat

The discrete arithmetic bridge

Arithmetic is the familiar system of counting numbers: zero, one, two, and so on, with addition and multiplication. The natural numbers, as mathematicians call them, are the same system. The declaration discrete_arith_equiv_logicNat establishes that these two descriptions are not merely similar but identical: the arithmetic that the Recognition Science framework forces out of its basic logic is the natural numbers, with no extra elements and no missing ones.

The framework begins with a ledger, a discrete record of events, and asks what structure must follow. Its machine-checked library of formal theorems shows that the logic of this ledger carries a universal forced arithmetic. The declaration in question is the bridge: it proves that the carrier set of this arithmetic is equivalent to the standard natural numbers. In plain terms, the counting structure that emerges from the framework's logic is the counting structure everyone already uses.

This is a definitional equivalence, not a new discovery about numbers. The declaration does not prove that the natural numbers exist, nor does it add new axioms to arithmetic. It identifies two descriptions within the framework: the arithmetic derived from the ledger's logic, and the standard natural numbers. The equivalence is a structural match, a dictionary between two ways of writing the same thing.

What the declaration does not claim matters as much as what it proves. It does not claim that the framework's logic is the only way to reach the natural numbers, nor that arithmetic is somehow created by the framework. It does not prove any new property of the natural numbers themselves, such as the infinitude of primes or the Goldbach conjecture. It only says: within this framework, the forced arithmetic is the natural numbers, exactly.

The practical consequence is that any theorem proved about the framework's arithmetic applies to ordinary arithmetic, and vice versa. A mathematician can move freely between the two descriptions. The bridge is a convenience, a guarantee of consistency, not a claim about the foundations of mathematics beyond the framework's own scope.

/-- The discrete realization carries the universal forced arithmetic. -/
noncomputable def discrete_arith_equiv_logicNat :
    (arithmeticOf discreteRealization).peano.carrier
      ≃ ArithmeticFromLogic.LogicNat :=
  discreteRealization.orbitEquivLogicNat

/-- The discrete realization carries the universal forced arithmetic. -/
noncomputable def discrete_arith_equiv_logicNat :
    (arithmeticOf discreteRealization).peano.carrier
      ≃ ArithmeticFromLogic.LogicNat :=
  discreteRealization.orbitEquivLogicNat

What this page does not claim

The declaration does not prove that the natural numbers exist independently of the framework. It does not add new axioms or properties to the natural numbers themselves. It does not claim the framework's logic is the only way to derive 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/DiscreteRealization.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: