Foundation Primitive Recognition Calculus Real Completeness Prcreal Raw Diagonal

The diagonal ledger

In mathematics, a real number is often built from a sequence of rational numbers that get closer together, a Cauchy sequence. A list of such sequences is a common device in analysis. The declaration PRCRealRawDiagonalLedgerTarget_of_tail_selection, a theorem in the framework's machine-checked library of formal theorems, concerns such a list. It states that if each sequence in the list is Cauchy, and the list itself is coherent in a precise sense, then one can select one term from each sequence, forming a new diagonal sequence that is itself Cauchy and that approaches the same limit as the original list. This is a constructive version of a classical diagonal argument, adapted to the framework's primitive objects.

The proof works by a tail selection. For each sequence, one chooses a term far enough along that the remaining tail is within a prescribed tolerance. The theorem shows these choices can be made consistently across the entire list, so the resulting diagonal sequence inherits the Cauchy property and the limit. The declaration is not a standalone result; it is a step in a chain that establishes completeness for the framework's real numbers, meaning every Cauchy list has a limit within the system. The theorem PRCRealRawDiagonalLedgerTarget_proved confirms the target, and it is used to prove a further diagonal selection theorem.

The declaration does not claim that the diagonal sequence is unique, nor that it is computable in any practical sense. It asserts existence of a selection, not a specific algorithm. It also does not claim that the framework's real numbers are the same as classical real numbers, only that this particular completeness property holds within the framework's own construction. The theorem is a formal statement about the framework's objects, not a claim about how real numbers behave in conventional mathematics.

In the broader Recognition Science program, this result supports the construction of real numbers from primitive recognition events, which are discrete records of distinctions. The diagonal ledger is a way to take a limit of such records. The theorem is a technical but necessary piece: it shows that the framework's notion of a real number is closed under taking limits of lists, a property that any useful number system must have.

/-- An explicit tail-selection diagonal is enough to build the raw diagonal
ledger target. -/
theorem PRCRealRawDiagonalLedgerTarget_of_tail_selection
    (htail : PRCRealTailSelectionTarget) :
    PRCRealRawDiagonalLedgerTarget := by
  intro U hU
  rcases htail U hU with ⟨pick, hs_cauchy, hs_limit⟩
  exact ⟨fun n => (U n).term (pick n), hs_cauchy, hs_limit⟩

theorem PRCRealCompletenessTarget_proved :
    PRCRealCompletenessTarget :=
  PRCRealCompletenessTarget_of_diagonal_selection
    PRCRealDiagonalSelectionTarget_proved

theorem PRCRealRawDiagonalLedgerTarget_proved :
    PRCRealRawDiagonalLedgerTarget :=
  PRCRealRawDiagonalLedgerTarget_of_tail_selection
    PRCRealTailSelectionTarget_proved

theorem PRCRealDiagonalSelectionTarget_proved :
    PRCRealDiagonalSelectionTarget :=
  PRCRealDiagonalSelectionTarget_of_raw_diagonal_ledger
    PRCRealRawDiagonalLedgerTarget_proved

What this page does not claim

The diagonal sequence is unique or computable by a specific algorithm. The framework's real numbers are identical to classical real numbers. The theorem applies to lists that are not coherent in the required sense.

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: