Foundation Arithmetic From Logic Embed Le Iff Of One Lt

Order from a single step

Counting is the oldest mathematical act. The natural numbers, 0, 1, 2, 3, and so on, come with a built-in order: 2 is less than 3 because you can reach 3 from 2 by adding one. That simple idea, that one number is smaller than another exactly when a finite number of unit steps connects them, is what the declaration embed_le_iff_of_one_lt pins down inside the Recognition Science framework.

The framework begins with a ledger, a discrete record of events, and a forced cost for each recognition. From that starting point, a proved theorem in the framework's machine-checked library of formal theorems derives a non-trivial generator γ, a positive number not equal to 1, and shows that repeatedly multiplying by γ produces the structure of the natural numbers. The declaration in question, embed_le_iff_of_one_lt, states that this embedded counting structure preserves order: a LogicNat n is less than or equal to m exactly when the real number it embeds to is less than or equal to the real number m embeds to.

Concretely, the framework defines LogicNat with two constructors: identity, representing zero, and step, representing one more iteration of the generator. The order relation is defined the way a schoolchild would define it: n is less than m if there exists a k such that n plus the successor of k equals m. The theorem embed_le_iff_of_one_lt then proves that this order matches the usual order on the real numbers when each LogicNat is mapped to its real value, which is γ raised to the appropriate power. The proof relies on the fact that the embedding is injective, meaning distinct LogicNats map to distinct reals, and that the generator is positive and not equal to 1.

What this establishes is that the order on the natural numbers is not an extra assumption but a consequence of the step structure. The framework derives, rather than assumes, that 0 is less than 1, that 1 is less than 2, and so on. It also proves that the usual properties of order hold: reflexivity, transitivity, and the fact that a number is less than another exactly when it is less than or equal to it and not equal to it. These are theorems in the library, not definitions.

What the declaration does not claim is more modest. It does not claim that the natural numbers exist independently in the physical world; it claims that within the framework, the structure forced by the comparison operator has the order properties of the natural numbers. It does not claim anything about base 10 or base 2 notation; the construction uses only the identity and the step operation. And it does not claim that the real number γ is the golden ratio, which is a separate result in the framework. The declaration is a precise statement about order preservation, nothing more and nothing less.

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

/-- The natural numbers as forced by the Law of Logic.

`identity` represents the zero-cost element (the multiplicative
identity in the orbit). `step` represents one more iteration of the
generator. The two-constructor structure mirrors the orbit
{1, γ, γ², γ³, ...} as the smallest subset of ℝ₊ closed under
multiplication by γ and containing 1. -/
inductive LogicNat : Type
  | identity : LogicNat
  | step     : LogicNat → LogicNat
  deriving DecidableEq, Repr

/-- Strict order on `LogicNat`. -/
def lt (n m : LogicNat) : Prop := ∃ k : LogicNat, n + succ k = m

/-- **Embedding injectivity**: distinct natural numbers map to distinct
points in the orbit. This closes the bridge from the abstract `LogicNat`
to the concrete orbit `{1, γ, γ², ...}` in ℝ₊. -/
theorem embed_injective (γ : Generator) : Function.Injective (embed γ) := by
  intro a b hab
  -- Translate to powers.
  rw [embed_eq_pow, embed_eq_pow] at hab
  -- Take logs.
  have hpos_a : 0 < γ.value ^ (LogicNat.toNat a) := pow_pos γ.pos _
  have hpos_b : 0 < γ.value ^ (LogicNat.toNat b) := pow_pos γ.pos _
  have hlog : Real.log (γ.value ^ (LogicNat.toNat a))
              = Real.log (γ.value ^ (LogicNat.toNat b)) := by
    exact congrArg Real.log hab
  rw [Real.log_pow, Real.log_pow] at hlog
  -- Cancel the non-zero log γ.value.
  have hne := log_generator_ne_zero γ
  have hcast : ((LogicNat.toNat a : ℝ)) = ((LogicNat.toNat b : ℝ)) := by
    have := mul_right_cancel₀ hne hlog
    exact this
  have h_nat : LogicNat.toNat a = LogicNat.toNat b := by exact_mod_cast hcast
  -- Lift back to LogicNat via the equivalence.
  have := congrArg LogicNat.fromNat h_nat
  rw [LogicNat.fromNat_toNat, LogicNat.fromNat_toNat] at this
  exact this

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⟩

What this page does not claim

The declaration does not claim that natural numbers exist independently in the physical world. It does not claim anything about base 10 or base 2 notation. It does not claim that γ is the golden ratio.

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: