Foundation Primitive Recognition Calculus Real Completeness Prcreal Completeness

The diagonal selection theorem

A real number is often defined as a limit of a sequence of rational numbers that get arbitrarily close to each other. A Cauchy sequence is such a sequence. A space is complete when every Cauchy sequence has a limit inside the space. The real numbers are complete; the rationals are not. This completeness is what lets calculus work, because it guarantees that limits exist when they should.

The theorem PRCRealCompletenessTarget_of_diagonal_selection establishes completeness in a specific constructive setting. It says that if a certain diagonal selection property holds, then completeness follows. The diagonal selection property states: given any sequence of Cauchy sequences, where each row is itself a Cauchy sequence and the rows get close to each other, you can pick one term from each row, forming a diagonal sequence, and that diagonal sequence is itself a Cauchy sequence that converges to the same limit as the rows. The theorem proves that this diagonal selection property is sufficient for completeness.

The proof is direct. The theorem takes the diagonal selection property as a hypothesis and concludes completeness. It does not construct the diagonal or prove the selection property itself. Those are separate theorems in the framework's machine-checked library of formal theorems. The declaration PRCRealCompletenessTarget_proved combines this theorem with a proof of the diagonal selection property to establish completeness in full.

The theorem does not claim that the real numbers are the only complete ordered field, nor does it claim that this construction is the standard one. It does not claim that every Cauchy sequence has a computable limit, only that a limit exists in the framework's model. It does not claim that the diagonal selection property is necessary for completeness, only that it is sufficient.

/-- The diagonal selection target is exactly the sharpened completeness target. -/
theorem PRCRealCompletenessTarget_of_diagonal_selection
    (hdiag : PRCRealDiagonalSelectionTarget) :
    PRCRealCompletenessTarget := by
  exact hdiag

/-- Named diagonal selection blocker for internal completeness. It asks for an
actual Cauchy ledger limit for every representative-Cauchy sequence of Cauchy
ledgers. -/
def PRCRealDiagonalSelectionTarget : Prop :=
  ∀ U : Nat → PRCCauchySeq,
    PRCRealRepresentativeCauchy U →
      ∃ L : PRCCauchySeq, PRCRealRepresentativeLimit U L

/-- The diagonal selection target is exactly the sharpened completeness target. -/
theorem PRCRealCompletenessTarget_of_diagonal_selection
    (hdiag : PRCRealDiagonalSelectionTarget) :
    PRCRealCompletenessTarget := by
  exact hdiag

What this page does not claim

This theorem does not prove that the real numbers are the only complete ordered field. This theorem does not claim that every Cauchy sequence has a computable limit. This theorem does not claim that the diagonal selection property is necessary for completeness.

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