Foundation Arithmetic From Logic Lt Iff Le And Ne

The order relation

The natural numbers come with a familiar ordering: 3 is less than 5, 5 is not less than 5, and 5 is less than 7. The Recognition Science framework builds its own copy of the natural numbers, called LogicNat, from a discrete record of events called a ledger. The framework's library, a machine-checked collection of formal theorems, proves that this copy orders itself the same way. The theorem lt_iff_le_and_ne states that one number is less than another exactly when it is at most that number and they are not equal.

That statement sounds like a definition, but in the framework it is a proved consequence of how the numbers are built. The construction starts with an identity element, representing the zero-cost state, and a step operation that moves to the next number. The order relation is defined by addition: a is at most b when some number k satisfies a + k = b. Strictly less means the gap is at least one full step. The theorem then shows that the two notions, at most and not equal, combine to give exactly the strict ordering.

The result matters because it ties the framework's abstract construction to ordinary arithmetic. A reader who knows that 3 < 5 and 3 ≠ 5 can now see that the framework's numbers satisfy the same pattern. The theorem also connects to the standard natural numbers: the framework proves that its order agrees with the usual one through the translation map toNat. So the ordering is not an arbitrary choice; it is forced by the structure.

What the theorem does not do is introduce a new kind of ordering. It does not define a partial order, a total order, or any exotic comparison. It merely confirms that the strict order, defined through addition, is the familiar one: less than means at most and not equal. The framework also proves related facts, such as that zero is at most every number and that every number is less than its successor, which together make the ordering behave like the counting numbers everyone learns in school.

theorem lt_iff_le_and_ne {a b : LogicNat} : a < b ↔ a ≤ b ∧ a ≠ b := by
  constructor
  · rintro ⟨k, hk⟩
    refine ⟨⟨succ k, hk⟩, ?_⟩
    intro hab
    rw [hab] at hk
    -- b + succ k = b means succ k = 0 by additive cancellation; impossible.
    have := congrArg toNat hk
    rw [toNat_add, toNat_succ] at this
    omega
  · rintro ⟨⟨k, hk⟩, hne⟩
    -- a + k = b, a ≠ b, so k ≠ 0; k = succ k' for some k'.
    cases k with
    | identity =>
      exfalso
      apply hne
      simpa using hk
    | step k' => exact ⟨k', hk⟩

@[simp] theorem le_def (n m : LogicNat) : n ≤ m ↔ ∃ k, n + k = m := Iff.rfl

theorem toNat_le (a b : LogicNat) : a ≤ b ↔ toNat a ≤ toNat b := by
  constructor
  · rintro ⟨k, hk⟩
    have := congrArg toNat hk
    rw [toNat_add] at this
    omega
  · intro h
    refine ⟨fromNat (toNat b - toNat a), ?_⟩
    have hroundtrip : ∀ n : LogicNat, fromNat (toNat n) = n := fromNat_toNat
    -- toNat (a + fromNat (toNat b - toNat a)) = toNat a + (toNat b - toNat a) = toNat b
    have hadd : toNat (a + fromNat (toNat b - toNat a)) = toNat b := by
      rw [toNat_add, toNat_fromNat]
      omega
    -- Apply equivNat injectivity
    have : a + fromNat (toNat b - toNat a) = b := by
      have h1 := congrArg fromNat hadd
      rw [hroundtrip, hroundtrip] at h1
      exact h1
    exact this

What this page does not claim

The theorem does not introduce a new ordering concept beyond the standard less-than relation. The theorem does not prove that the framework's natural numbers are the only possible construction. The theorem does not establish any property of the real numbers or the cost function J.

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