PRCRealCompletenessTarget_sharpened
plain-language theorem explainer
The internal completeness blocker for the PRC null-quotient reals is definitionally the concrete Cauchy-of-Cauchy diagonal: every representative-Cauchy sequence of Cauchy ledgers has a Cauchy-ledger limit. Completeness auditors and the Step 10e certificate cite this sharpened form. The proof is pure reflexivity once that Prop is the target definition.
Claim. The completeness target for the internal null-quotient reals is identical to the statement that for every sequence $U$ of Cauchy ledgers, if $U$ is Cauchy at the representative level, then there exists a Cauchy ledger $L$ that is a representative limit of $U$.
background
Primitive Recognition Calculus builds an internal real carrier from rational ledgers. A Cauchy ledger is a rational sequence with a Cauchy modulus; the closed carrier PRCRealNullClosed is the quotient of those ledgers by null distance (ledgers that agree in the limit).
Completeness of that quotient is blocked by a single Prop: every Cauchy sequence of ledger representatives must itself admit a ledger representative as limit (a diagonal Cauchy-of-Cauchy statement). Upstream, that Prop is named as the exact blocker for completeness of the internal null quotient.
The local module packages realization, quotient-point, and diagonal-selection facts that discharge pieces of that blocker. The present declaration records that the blocker has been sharpened to the concrete diagonal form rather than an abstract completeness slogan.
proof idea
One-line term proof by rfl. Both sides of the equality are the same definitional Prop (the universal quantifier over representative-Cauchy sequences of Cauchy ledgers asserting existence of a representative limit). No lemmas are applied; the sharpening is that the target is already that concrete diagonal statement.
why it matters
Feeds the Step 10e package prc_real_completeness_sharpened_certificate, which bundles raw-Cauchy realization, raw-Cauchy quotient points, and diagonal selection from the raw diagonal ledger. Downstream that certificate is the bookkeeping object that the full internal completeness story hangs on.
In the Recognition foundation stack this is the ordered-field completeness step for the PRC real carrier: without a representative limit for Cauchy-of-Cauchy data, the null quotient cannot serve as a complete ordered field. It sits under the broader forcing and emergence chain (finite 8-tick register, Clifford bridge) by supplying the analytic completeness half once the algebraic carrier exists.
It does not itself close every open completeness obligation; it locks the target shape so later certificates can cite one fixed Prop.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.