Foundation Arithmetic Of Logic Nat Lift Unique Fun

The unique lift

The natural numbers, 0, 1, 2, and so on, are the most basic counting system in mathematics. A Peano algebra is a formal way to describe such a system: it is a collection of objects with a distinguished starting point, usually called zero, and a rule for moving from one object to the next, usually called the successor or step function. The classical theorem about these structures is that they are all essentially the same: given any two Peano algebras, there is exactly one way to translate the counting of one into the counting of the other while preserving the starting point and the step rule. This is the principle of mathematical induction in disguise.

The Recognition Science framework builds its own version of the natural numbers, called LogicNat, from a primitive notion of a ledger, a discrete record of events. The framework's machine-checked library of formal theorems proves that this LogicNat is a Peano algebra. The declaration logicNatLift_unique_fun is the precise statement of uniqueness for this structure: for any other Peano algebra B, any structure-preserving map from LogicNat to B must be exactly the one the framework constructs, called the lift. The proof is a direct induction on the structure of LogicNat, showing that the map is forced step by step: it must send the starting point to B's starting point, and each successor must go to the successor of the image of the previous element.

This uniqueness is the technical heart of what the framework calls Universal Forcing. Because LogicNat is an initial object in the category of Peano algebras, any other counting structure that satisfies the same axioms is uniquely isomorphic to it. The framework uses this to argue that arithmetic is not an arbitrary choice but is forced by the structure of its own logic. The theorem establishes that the framework's natural numbers are a canonical starting point, and that any other valid counting system is just a relabeling of the same underlying structure.

What the theorem does not claim is equally important. It does not say that the framework's LogicNat is the only possible set of natural numbers in all of mathematics; it says that within the framework's axioms, any Peano algebra is uniquely isomorphic to it. It does not prove that the framework's logic is the true or only foundation for mathematics. It does not derive any specific arithmetic facts, such as 2 + 2 = 4, from the ledger; it only establishes the uniqueness of the structure that would support such facts. The theorem is a statement about the internal consistency and determinacy of the framework's own construction, not a claim about the external world.

private theorem logicNatLift_unique_fun (B : PeanoObject)
    (f : PeanoObject.Hom logicNatPeano B) :
    f.toFun = (logicNatLift B).toFun := by
  funext n
  induction n with
  | identity =>
      exact f.map_zero
  | step n ih =>
      calc
        f.toFun (LogicNat.step n) = B.step (f.toFun n) := f.map_step n
        _ = B.step ((logicNatLift B).toFun n) := by rw [ih]
        _ = (logicNatLift B).toFun (LogicNat.step n) := rfl

private theorem logicNatLift_unique_fun (B : PeanoObject)
    (f : PeanoObject.Hom logicNatPeano B) :
    f.toFun = (logicNatLift B).toFun := by
  funext n
  induction n with
  | identity =>
      exact f.map_zero
  | step n ih =>
      calc
        f.toFun (LogicNat.step n) = B.step (f.toFun n) := f.map_step n
        _ = B.step ((logicNatLift B).toFun n) := by rw [ih]
        _ = (logicNatLift B).toFun (LogicNat.step n) := rfl

What this page does not claim

The theorem does not claim that LogicNat is the only possible set of natural numbers in all of mathematics. It does not prove that the framework's logic is the true or only foundation for mathematics. It does not derive any specific arithmetic facts, such as 2 + 2 = 4, from the ledger.

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