PRCRealCompletenessTarget_proved
plain-language theorem explainer
Every Cauchy sequence of Cauchy-ledger representatives on the internal null quotient has a Cauchy-ledger representative limit. Completeness auditors of the Primitive Recognition Calculus real construction cite this as the discharged blocker. The proof is a one-line term that identifies the completeness target with the already-proved diagonal-selection target.
Claim. For every sequence $U:\mathbb{N}\to\mathrm{PRCCauchySeq}$ that is Cauchy in the representative sense, there exists a Cauchy ledger $L$ that is a representative limit of $U$.
background
The Primitive Recognition Calculus builds an internal real carrier as a null quotient of Cauchy ledgers. Completeness of that carrier is not taken from Mathlib; it is an explicit Prop-level blocker on representative sequences.
PRCRealCompletenessTarget is that blocker: every sequence $U$ of Cauchy ledgers that is itself representative-Cauchy admits some Cauchy ledger $L$ serving as a representative limit. Upstream, the same Prop is identified with the diagonal-selection target: a Cauchy-of-Cauchy diagonal construction that picks a single ledger limit from a raw diagonal ledger. The module sits on the real-order-congruence layer and packages the internal completeness claim before promotion to a complete ordered field.
proof idea
One-line term proof. Apply PRCRealCompletenessTarget_of_diagonal_selection, whose body is exact hdiag: the diagonal-selection target is definitionally the sharpened completeness target. Feed PRCRealDiagonalSelectionTarget_proved, which itself comes from the raw-diagonal-ledger target. No new arithmetic is done here; the theorem only closes the completeness Prop once diagonal selection is in hand.
why it matters
This is the discharged form of the exact completeness blocker for the internal null quotient. Downstream it feeds prc_real_completeness_sharpened_certificate, which bundles raw Cauchy realization, quotient-point, and diagonal-selection facts into a single sharpened certificate, and prc_real_complete_ordered_field_promoted_certificate, which promotes the carrier (with rat embedding, add closure, and congruence) toward a complete ordered field. In the Recognition foundation stack this is the analytic step that makes the PRC real usable as a complete ordered scalar, not merely an ordered field of Cauchy classes. It does not itself force phi, the eight-tick octave, or $D=3$; those live in the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.