Foundation Arithmetic From Logic Embed Lt Iff Of One Lt

The embedding theorem

The natural numbers are the familiar counting numbers 0, 1, 2, 3, and so on. In the Recognition Science framework, these numbers are not assumed as a starting point. Instead, the framework derives them from a comparison operator, a rule that decides which of two positive real numbers is larger. The key idea is that the orbit of a single nontrivial generator, the set {1, γ, γ², γ³, ...}, has exactly two constructors: being at the identity element 1, or taking one more step. That two-constructor structure is the natural-number structure, and the framework makes it an inductive type called LogicNat.

The declaration embed_lt_iff_of_one_lt establishes a precise correspondence between this derived structure and the ordinary natural numbers. It proves that the embedding function, which maps each LogicNat to a positive real number, preserves the less-than relation. In plain language: if one derived number is less than another in the LogicNat ordering, then its embedded real value is less than the other's embedded real value, and conversely. The theorem is stated as: n < m if and only if embed γ n < embed γ m, for any positive real generator γ not equal to 1.

This matters because it shows the derived arithmetic behaves like the familiar one. The framework's natural numbers are not a strange shadow of the real numbers; they embed into the positive reals in a way that respects order. The proof also shows the embedding is injective, meaning distinct derived numbers map to distinct real numbers. Combined with the order preservation, this gives a faithful copy of the natural numbers inside the positive reals, built from nothing but the comparison operator and the step operation.

In Recognition Science, this is part of a larger chain: the Law of Logic forces a cost function, which forces a generator, which forces the natural numbers, which then force arithmetic. The declaration is one link in that chain, showing that the derived ordering matches the real ordering. It does not claim that the framework has invented new numbers or a new arithmetic. It claims that the familiar natural numbers, with their usual order, can be reconstructed from a more primitive starting point.

The theorem is machine-checked, meaning a computer program has verified every step of the proof. The framework's library of formal theorems contains this result as a proved statement, not as a conjecture or an assumption. The proof relies only on the standard axioms of the underlying type theory, with no framework-specific axioms added.

theorem lt_iff_succ_le {n m : LogicNat} : n < m ↔ succ n ≤ m := by
  constructor
  · rintro ⟨k, hk⟩
    refine ⟨k, ?_⟩
    show succ n + k = m
    rw [succ_add]
    show succ (n + k) = m
    rw [← add_succ]
    -- need n + succ k = m, but we have n + succ k = m via hk; succ_add transforms
    -- Wait: hk : n + succ k = m, and succ (n + k) = n + succ k by add_succ. So succ (n + k) = m.
    exact hk
  · rintro ⟨k, hk⟩
    refine ⟨k, ?_⟩
    show n + succ k = m
    rw [add_succ]
    show succ (n + k) = m
    rw [← succ_add]
    exact hk

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

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

What this page does not claim

Not a claim that the framework has invented new numbers or a new arithmetic. Not a claim that the embedding covers all positive real numbers, only the orbit of the generator. Not a claim that the comparison operator itself is derived from anything more primitive; it is a starting point.

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: