Foundation Distinction To Arithmetic

The Distinction Bridge

In mathematics, a distinction is the simplest possible piece of information: the assertion that two objects, call them x and y, are not the same. Recognition Science asks how much structure such a bare difference can force. The answer, proved in a machine-checked library of formal theorems, is that a single distinction forces an entire arithmetic: the natural numbers 0, 1, 2, 3, and so on, with all their usual properties. The real numbers, by contrast, are not forced; they enter only through a separate act of completion.

The classical background is Peano arithmetic, the standard axiomatization of the natural numbers. Its defining features are a zero, a successor function that adds one, the rule that zero is not a successor, the rule that distinct numbers have distinct successors, and the principle of induction. The framework's theorem constructs, from any carrier set K with two distinct points, an object that satisfies all five of these conditions. The construction is not an assumption; it is a proved theorem, checked by a computer, with no project-specific axioms.

The key result, distinction_forces_arithmetic, states that from the bare proposition that K has two distinct points, there exists a named arithmetic whose carrier is canonically equivalent to LogicNat, the framework's countable initial Peano object. The word "canonical" carries real weight: the theorem distinction_forcing_map_unique proves that between the arithmetics forced by any two distinctions, there is exactly one structure-preserving map. No representational freedom remains. This is canonicity, not mere isomorphism.

The framework's library also states the upper bound of what a distinction can do. The theorem real_not_forced_from_distinction proves that no countable certificate system can faithfully cover the real line. Since the forced arithmetic is countable, the continuum is strictly beyond its reach. The real numbers are not native to distinction; they appear only through a completion or display interface, a separate layer of the framework.

What this changes is the starting point of arithmetic. The natural numbers are not assumed as a primitive; they are derived from the prior fact that two things can differ. The derivation is complete, machine-checked, and unique. The continuum, by contrast, remains a target of a different kind, one that distinction alone cannot reach.

/-- 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)

/-- **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⟩⟩

/-- **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 real numbers are not derived from a distinction; they require a separate completion step. The module does not prove that the natural numbers are the only possible arithmetic, only that the forced one is canonical. The theorem does not establish that any carrier with two distinct points is itself countable.

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: