PRCRawCauchyQuotientPointTarget
plain-language theorem explainer
Every raw rational Cauchy ledger determines a point of the final null-distance quotient carrier of PRC reals. Completeness certificates and the Step 10e sharpened certificate cite this target as the raw-to-quotient existence obligation. The declaration is a Prop-shaped definition: a quantified existence claim, not a proved theorem.
Claim. For every raw rational ledger $s:\mathbb{N}\to\mathrm{PRCRat}$ that is Cauchy in the $J$-cost distance, the final null-distance quotient carrier of PRC reals is nonempty.
background
In the Primitive Recognition Calculus, a raw rational ledger is simply a sequence $\mathbb{N}\to\mathrm{PRCRat}$ with no Cauchy proof attached. The Cauchy predicate on such ledgers uses the same $J$-cost distance as the ordinary PRC Cauchy sequences: for every positive rational $\varepsilon$ there is $N$ so that all pairs of terms beyond $N$ have $J$-cost distance less than $\varepsilon$.
The final real carrier is the null-distance quotient of Cauchy ledgers. Upstream, PRCRealNullClosed is defined as that quotient once null-distance is known to be a transitive equivalence. The local module packages completeness targets that turn raw Cauchy data into points of this closed carrier.
This definition records the existence half of that passage: a Cauchy raw ledger should force the quotient to be inhabited (in practice, by the class of a realization of that ledger).
proof idea
Definitional Prop only. The body is the universal statement $\forall s,\ \mathrm{Cauchy}(s)\to\mathrm{Nonempty}(\mathrm{PRCRealNullClosed})$. No tactics or lemmas are applied here; the sibling theorem discharges it by realizing $s$ as a Cauchy sequence and packing the class under the null-distance setoid.
why it matters
This target is one field of the Step 10e sharpened completeness certificate (PRCRealCompletenessSharpenedCertificate), which bundles raw-ledger realization, quotient-point existence, diagonal selection, and representative completeness for the closed PRC real carrier. The proved sibling fills the field by constructing the quotient class of a realization of $s$.
In the Recognition foundation stack, completeness of the real carrier is the analytic substrate under later forcing (ordered field, continuum structure) that supports the T0–T8 chain. Without a raw Cauchy ledger landing in the null-distance quotient, the closed real type would not be known to receive the sequences that define limits and the continuum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.