Foundation Distinction To Arithmetic Distinction Forces Arithmetic Of

The forced arithmetic

In mathematics, a distinction is the simplest possible piece of information: a carrier set with two points that are not equal. Recognition Science asks what structure such a bare distinction forces into existence. The answer, proved in its machine-checked library of formal theorems, is that any distinction forces a full initial Peano arithmetic: an object with a zero, a successor step, and induction, the same countable arithmetic that underlies the natural numbers.

The key theorem, distinction_forces_arithmeticOf, states that from the proposition that a carrier K has two distinct points, there exists a named distinction whose forced arithmetic carrier is canonically equivalent to LogicNat, the framework's countable initial Peano object. The carrier is provably countable, and it carries the complete Peano surface: zero is never a successor, the successor is injective, and induction holds. This is not a bare isomorphism; the theorem proves canonicity. Between any two distinctions, there is a unique zero and successor preserving map between their forced arithmetics. The map is determined by the distinction data alone, with no representational freedom.

The framework models this as a ledger: a discrete record of events where each entry is either zero or a successor of a previous entry. The theorem proves that such a ledger, forced from the mere existence of two distinguishable points, must be the countable initial Peano arithmetic. This is the lower bound of what distinction forces. The upper bound is equally sharp: the real line is not forced from any countable certificate system. A theorem, real_not_forced_from_distinction, proves that no countable set of certificates can faithfully cover the continuum. So the forced arithmetic lands exactly at LogicNat, never at the real numbers. The continuum enters only through a separate completion or display interface, not from distinction alone.

What this changes is the status of arithmetic in the framework. Arithmetic is not assumed as a primitive; it is derived from the simplest possible input, the existence of two different things. The derivation is unique, and it stops exactly at the countable. This gives a precise sense in which the natural numbers are the inevitable arithmetic of any world that contains a distinction, and in which the real numbers require an additional step beyond that distinction.

/-- **Distinction forces an initial Peano arithmetic.** From the bare proposition
that `K` has two distinct points, there is a named distinction whose forced
arithmetic carrier is canonically `LogicNat`. -/
theorem distinction_forces_arithmeticOf
    {K : Type u} [DecidableEq K] (h : ∃ x y : K, x ≠ y) :
    ∃ (x y : K) (hxy : x ≠ y),
      Nonempty ((arithmeticOfDistinction x y hxy).peano.carrier ≃ LogicNat) := by
  obtain ⟨x, y, hxy⟩ := h
  exact ⟨x, y, hxy, ⟨arithmeticOfDistinction_carrier_equiv_logicNat x y hxy⟩⟩

/-- The distinction-forced arithmetic carrier is **countable**: it is `LogicNat`,
which is equivalent to `ℕ`. This is the δ-native lower fact: a distinction forces
exactly the countable initial Peano object, no more. -/
theorem arithmeticOfDistinction_carrier_countable
    {K : Type u} [DecidableEq K] (x y : K) (hxy : x ≠ y) :
    Countable (arithmeticOfDistinction x y hxy).peano.carrier := by
  haveI : Countable LogicNat := Countable.of_equiv Nat LogicNat.equivNat.symm
  exact Countable.of_equiv LogicNat
    (arithmeticOfDistinction_carrier_equiv_logicNat x y hxy).symm

/-- The distinction-forced arithmetic carries the Peano surface: its zero is never
a step, its step is injective, and it satisfies induction. -/
theorem arithmeticOfDistinction_peanoSurface
    {K : Type u} [DecidableEq K] (x y : K) (hxy : x ≠ y) :
    ArithmeticOf.PeanoSurface (arithmeticOfDistinction x y hxy) :=
  UniversalForcing.peano_surface (logicRealizationOfDistinction K x y hxy)

/-- **Canonicity for distinctions.** Any zero/step-preserving function between the
forced arithmetics of two distinctions *is* the forcing map. The map is determined
by the distinction data alone, with no representational freedom. -/
theorem distinction_forcing_map_unique
    {K L : Type u} [DecidableEq K] [DecidableEq L]
    {x y : K} {a b : L} (hxy : x ≠ y) (hab : a ≠ b)
    (f : (arithmeticOfDistinction x y hxy).peano.carrier →
          (arithmeticOfDistinction a b hab).peano.carrier)
    (hz : f (arithmeticOfDistinction x y hxy).peano.zero =
            (arithmeticOfDistinction a b hab).peano.zero)
    (hs : ∀ p, f ((arithmeticOfDistinction x y hxy).peano.step p) =
            (arithmeticOfDistinction a b hab).peano.step (f p)) :
    f = (distinction_forcing_map hxy hab).toFun :=
  ArithmeticOf.forcing_map_unique
    (arithmeticOfDistinction x y hxy) (arithmeticOfDistinction a b hab) f hz hs

/-- **ℝ is not forced from a distinction.** No countable certificate system
faithfully covers ℝ. Restated from `RealLineNonNativity.real_not_faithfully_certifiable`
to sit beside the distinction-forced (countable) arithmetic and make the
unification explicit: distinction forces `LogicNat`, never `ℝ`. -/
theorem real_not_forced_from_distinction
    {Cert : Type} [Countable Cert] (assign : ℝ → Cert) :
    ¬ PrimitiveRecognitionCalculus.RealLineNonNativity.Faithful assign :=
  PrimitiveRecognitionCalculus.RealLineNonNativity.real_not_faithfully_certifiable assign

What this page does not claim

The theorem does not derive the real numbers from a distinction. The theorem does not prove that arithmetic is unique in any sense other than the canonicity of the zero and successor preserving map. The theorem does not claim that the Peano surface is the only structure a distinction can force.

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