Encyclopedia Foundation Foundation Distinction To Arithmetic Arithmetic Of Distinction Carrier Countable

ARTICLE 4 claims 4 theorems

Foundation Distinction To Arithmetic Arithmetic Of Distinction Carrier Countable

From the bare fact that two things differ, a machine-checked proof derives the natural numbers, and no more.

Verify this page

The countable arithmetic

In mathematics, a distinction is simply a carrier with two distinguishable points, written x ≠ y. The Recognition Science framework proves that from this minimal seed, a full initial Peano arithmetic follows: a structure with a zero, a successor function, and induction, equivalent to the natural numbers. The declaration arithmeticOfDistinction_carrier_countable establishes that this forced arithmetic's carrier is countable, meaning it can be put in one-to-one correspondence with the natural numbers. This is a theorem in the framework's machine-checked library of formal theorems, with no unproved assumptions beyond the standard logical axioms.

The proof works by constructing a named object, arithmeticOfDistinction, from any distinction, and then showing this object's carrier is equivalent to LogicNat, the framework's canonical countable arithmetic. The theorem then uses this equivalence to transfer countability from LogicNat to the forced arithmetic. The result is that a distinction forces exactly the countable initial Peano object, no more. The framework's library also proves the forced arithmetic carries the full Peano surface: zero is never a successor, the successor function is injective, and induction holds.

In Recognition Science, this is the δ-native lower fact: the continuum is not forced from countable distinction certificates. The theorem real_not_forced_from_distinction shows that no countable certificate system can faithfully cover the real numbers. The real line enters only through a completion or display interface, not from distinction alone. This means the framework's arithmetic of distinction lands at LogicNat, never at the reals.

The framework also proves canonicity: between any two distinctions, there exists a unique zero/step-preserving map between their forced arithmetics. This map is determined by the distinction data alone, with no representational freedom. The theorem distinction_forcing_map_unique states that any such map equals the forcing map, and distinction_arithmetic_universal_objective bundles existence and uniqueness into one statement.

What this does not claim: it does not claim that the real numbers can be derived from distinction alone, nor that the natural numbers are the only possible arithmetic. It does not claim that the framework's theorems replace conventional mathematics; rather, they reproduce the natural numbers as a forced consequence of a minimal distinction. The theorem is a precise statement about what follows from a countable seed, and the framework is explicit that the continuum requires additional structure beyond distinction.

THEOREM arithmeticOfDistinction_carrier_countable · IndisputableMonolith/Foundation/DistinctionToArithmetic.lean
arithmeticOfDistinction_carrier_countable · IndisputableMonolith/Foundation/DistinctionToArithmetic.lean:92 
/-- 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
THEOREM arithmeticOfDistinction_peanoSurface · IndisputableMonolith/Foundation/DistinctionToArithmetic.lean
arithmeticOfDistinction_peanoSurface · IndisputableMonolith/Foundation/DistinctionToArithmetic.lean:79 
/-- 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)
THEOREM real_not_forced_from_distinction · IndisputableMonolith/Foundation/DistinctionToArithmetic.lean
real_not_forced_from_distinction · IndisputableMonolith/Foundation/DistinctionToArithmetic.lean:174 
/-- **ℝ 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
THEOREM distinction_forcing_map_unique · distinction_arithmetic_universal_objective · IndisputableMonolith/Foundation/DistinctionToArithmetic.lean
distinction_forcing_map_unique · IndisputableMonolith/Foundation/DistinctionToArithmetic.lean:128 
/-- **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
distinction_arithmetic_universal_objective · IndisputableMonolith/Foundation/DistinctionToArithmetic.lean:144 
/-- **The Universal-Forcing objective on the distinction primitive.** For any two
distinctions, there is a structure-preserving equivalence between their forced
arithmetics that is *the unique* zero/step-preserving map: existence plus
canonicity in one statement. -/
theorem distinction_arithmetic_universal_objective
    {K L : Type u} [DecidableEq K] [DecidableEq L]
    {x y : K} {a b : L} (hxy : x ≠ y) (hab : a ≠ b) :
    ∃ e : (arithmeticOfDistinction x y hxy).peano.carrier ≃
            (arithmeticOfDistinction a b hab).peano.carrier,
      e (arithmeticOfDistinction x y hxy).peano.zero =
          (arithmeticOfDistinction a b hab).peano.zero
      ∧ (∀ p, e ((arithmeticOfDistinction x y hxy).peano.step p) =
            (arithmeticOfDistinction a b hab).peano.step (e p))
      ∧ (∀ f : (arithmeticOfDistinction x y hxy).peano.carrier →
              (arithmeticOfDistinction a b hab).peano.carrier,
            f (arithmeticOfDistinction x y hxy).peano.zero =
                (arithmeticOfDistinction a b hab).peano.zero →
            (∀ p, f ((arithmeticOfDistinction x y hxy).peano.step p) =
                  (arithmeticOfDistinction a b hab).peano.step (f p)) →
            f = e.toFun) :=
  ArithmeticOf.universal_objective
    (arithmeticOfDistinction x y hxy) (arithmeticOfDistinction a b hab)

What this page does not claim

The real numbers can be derived from distinction alone. The natural numbers are the only possible arithmetic structure. The framework's theorems replace conventional mathematics.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND