PRCRawCauchyQuotientPointTarget_proved
plain-language theorem explainer
Every raw rational Cauchy ledger determines a point of the final null-distance quotient of Cauchy sequences. Completeness-certificate authors cite this when wiring the PRC real carrier. The proof realizes the ledger as a Cauchy sequence, then applies the quotient map for the null-distance setoid built from proved transitivity.
Claim. For every raw rational ledger $s$ that is Cauchy, the final null-distance quotient of Cauchy ledgers is nonempty at the class of $s$: there exists a point of $\mathrm{PRCRealNullClosed}$ representing $s$.
background
In the Primitive Recognition Calculus, candidate reals are built from raw rational ledgers that satisfy a Cauchy condition. A raw Cauchy ledger is first realized as an explicit Cauchy sequence object; the final real carrier is then the quotient of those sequences by null distance (two sequences identified when their J-cost separation vanishes in the limit).
Null equivalence is already known to be reflexive and symmetric; the upstream result that null distance is transitive supplies the missing setoid law. That transitivity is obtained from the J-cost distance triangle-modulus theorem, so the setoid constructor applies directly.
Locally this module packages the completeness targets for that quotient construction: realization of raw Cauchy data, passage to a quotient point, and later diagonal/tail selection for internal limits.
proof idea
Term-mode after intro s hs. Apply the already-proved raw Cauchy realization target to obtain a Cauchy-sequence witness $u$ with the given ledger as its term. Form the setoid on Cauchy sequences via the null-distance setoid constructor fed by the proved null-distance transitivity theorem. Return the nonempty witness as the quotient class Quot.mk of that $u$. No further Cauchy or distance estimates are needed here; the work is pure packaging of realization plus quotient.
why it matters
This discharges the raw_cauchy_quotient_point field of the sharpened PRC real-completeness certificate in the same module. That certificate aggregates realization, quotient-point existence, and diagonal selection so the PRC real carrier is usable as a complete ordered continuum built only from recognition ledgers and J-cost null distance.
In the broader foundation stack this is part of constructing the continuum from the recognition calculus rather than importing classical reals as a black box. It sits downstream of null-distance transitivity (itself from the J-cost triangle modulus) and upstream of any completeness or limit arguments that need every raw Cauchy ledger to name an actual point of the quotient. It does not itself force $\varphi$, the eight-tick octave, or $D=3$; those live in the unified forcing chain. It closes a named completeness blocker so later analytic structure can sit on a proved carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.