Foundation Primitive Recognition Calculus Grow Eta Completion M0a

Completing the rationals

The real numbers are usually introduced as infinite decimals, but there is a more structural way to build them: as limits of sequences of rational numbers. A Cauchy sequence is one where the terms get arbitrarily close to each other as the sequence progresses. The real number is then the equivalence class of all sequences that converge to the same limit. The construction EtaCompletionM0a carries out that idea inside Recognition Science's formal library, but with a twist: the sequences are made of ratio orbits, not plain rationals, and the closeness condition is written in terms of a cross-difference, an integer that measures how far two ratios are apart without ever forming a fraction.

The construction starts with a ledger, a discrete record of events, here a sequence of ratio orbits. A ratio orbit is a rational number equipped with extra structure used by the framework. A regular sequence is one where the cross-difference between any two terms, scaled by their positions, stays bounded by a product of their denominators. This is a precise, integer-only way to say the sequence is Cauchy. Two regular sequences are equivalent when their cross-differences eventually become small relative to the denominators, which is the standard Cauchy equivalence in disguise.

The main object is RealDelta, the quotient of regular sequences by that equivalence. Each regular sequence maps to an element of RealDelta, and two sequences map to the same element exactly when they are equivalent. The construction proves this is well-defined and that the map from ratio orbits into RealDelta is injective: distinct ratio orbits give distinct real numbers. This is the eta completion, the embedding of the rational-like objects into their completion.

In Recognition Science, this construction is a foundational step. The framework derives physical constants from a cost function, and that derivation works with real numbers. This construction provides the real numbers from the ledger of ratio orbits, so the rest of the framework has a rigorous ground to stand on. It is a piece of the plumbing, not a headline result, but it is the kind of plumbing that makes the larger claims possible.

The classical content here is the standard Cauchy completion of the rationals, a construction due to Georg Cantor in the 1870s. The contribution is to do it with integer arithmetic and ratio orbits, avoiding fractions in the definitions. This matters for the framework because it keeps the construction discrete and finitary, in line with the ledger picture, while still producing the continuum of real numbers.

/-- The unit η : ℚδ → ℝδ_pre is injective: no two distinct δ-rationals collapse
in the completion. Together with well-definedness this makes η a genuine
embedding of the rational base into the M0a real line, choice-free. -/
theorem etaQ_injective : Function.Injective etaQ := by
  intro a b h
  induction a using Quot.ind with
  | mk q =>
    induction b using Quot.ind with
    | mk r =>
      have hq : RealDelta.mk (eta q) = RealDelta.mk (eta r) := h
      have hequiv : equiv (eta q) (eta r) := by
        have := Quot.eqvGen_exact hq
        -- Exactness gives `EqvGen`; collapse it with the proved equivalence.
        exact (Equivalence.eqvGen_iff equiv_equivalence).mp this
      exact Quot.sound (crossEq_of_equiv_eta hequiv)

/-- A regular sequence of delta-rationals.

A sequence `(a_n)` is regular when `|a_m - a_n| ≤ 1/(m+1) + 1/(n+1)` for all `m, n`.
Expressed via integer cross-multiplication (avoiding the ℚ display):
`|crossDiff(a_m, a_n)| * (m+1) * (n+1) ≤ (m+n+2) * den(a_m) * den(a_n)`. -/
structure RegularSeq where
  seq : ℕ → RatioOrbit
  regular : ∀ m n : ℕ,
    Int.natAbs (crossDiff (seq m) (seq n)) * (m + 1) * (n + 1) ≤
    (m + n + 2) * (seq m).den.toNat * (seq n).den.toNat

/-- Working equality on regular sequences: their pointwise difference
converges to 0. For every tolerance `1/(k+1)`, eventually
`|s_n - t_n| ≤ 1/(k+1)`. -/
def equiv (s t : RegularSeq) : Prop :=
  ∀ k : ℕ, ∃ N : ℕ, ∀ n : ℕ, n ≥ N →
    Int.natAbs (crossDiff (s.seq n) (t.seq n)) * (k + 1) ≤
    (s.seq n).den.toNat * (t.seq n).den.toNat

What this page does not claim

This construction does not prove the real numbers are unique up to isomorphism. This construction does not define addition or multiplication on RealDelta. This construction does not connect the completion to the forcing chain that derives physical constants.

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/PrimitiveRecognitionCalculus/Grow/EtaCompletionM0a.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: