PRCRealCompletenessTarget
plain-language theorem explainer
Exact Prop target for completeness of the internal null quotient of PRC reals: every Cauchy sequence of Cauchy-ledger representatives has a Cauchy-ledger representative limit (the diagonal theorem). Completeness certificates and the promoted ordered-field layer cite it as the blocker they discharge. The body is the quantified statement itself; no proof lives here.
Claim. For every sequence $(U_n)_{n\in\mathbb{N}}$ of PRC Cauchy ledgers that is Cauchy as a sequence of null-quotient representatives, there exists a PRC Cauchy ledger $L$ that is a representative limit of $(U_n)$.
background
Primitive Recognition Calculus builds an internal real line from rational ledgers and the J-cost distance. A PRC Cauchy sequence is an orbit-indexed rational ledger whose pairwise J-cost distances eventually fall below every positive PRC rational tolerance.
The null quotient identifies ledgers that are eventually close at every positive tolerance. A sequence of Cauchy ledgers is representative-Cauchy when its raw tails are eventually close in that sense; a ledger $L$ is a representative limit when each tail of the sequence is eventually close to $L$.
This module packages the exact Prop blockers for the next real-completion phase (add/mul closure, congruence, completeness). The present definition is the completeness blocker for that null quotient.
proof idea
Definition of a Prop, not a proved theorem. The body is the single quantified statement: for all sequences of PRC Cauchy ledgers that satisfy the representative-Cauchy predicate, there exists a PRC Cauchy ledger satisfying the representative-limit predicate. No tactics or lemmas are applied; downstream theorems prove or equate this target.
why it matters
Exact blocker for completeness of the internal null quotient (doc-comment: the diagonal theorem). Downstream, PRCRealCompletenessTarget_of_diagonal_selection identifies it with the diagonal-selection target, and PRCRealCompletenessTarget_proved discharges it via that selection. The Step 10e sharpened certificate records representative-completeness for the closed null quotient; the promoted ordered-field certificate packages carrier, rat embedding, and closed operations on top.
In the Recognition foundation this is the analytic half of building a complete ordered field from ledger geometry and J-cost, before Mathlib typeclass packaging. It does not itself invoke T5–T8 or the mass ladder; it supplies the real-analytic substrate those layers assume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.