PRCRealRepresentativeCauchy
plain-language theorem explainer
Defines the Cauchy condition for a sequence of PRC Cauchy ledgers viewed as null-quotient representatives: for every positive PRC rational tolerance, tails of the sequence are eventually close at the raw ledger level. Completeness blockers and diagonal/tail-selection targets cite this as the hypothesis on input sequences. The body is a direct Prop encoding of that uniform eventual-closeness quantifier chain.
Claim. A sequence $U$ of Cauchy ledgers is representative-Cauchy when, for every positive PRC rational $\varepsilon$, there exists $N$ such that for all $m,n \ge N$ the raw rational ledgers of $U_m$ and $U_n$ are eventually close within $\varepsilon$.
background
Primitive Recognition Calculus builds an internal real line from rational ledgers before any external $\mathbb{R}$ is assumed. PRC rationals are ratio-orbit quotient classes (cross-multiplication identification). A Cauchy ledger is a raw rational sequence that is Cauchy for the PRC $J$-cost distance, then packaged up to null equivalence.
Representative closeness is checked on the underlying raw ledgers via eventual closeness at a positive PRC tolerance: positivity of a ratio orbit means a nonnegative unbalanced signed numerator over a nonzero orbit denominator. The module sits in the real-completeness layer that aims to show the null quotient of Cauchy ledgers is a complete ordered field.
Upstream scaffolding supplies the rational field, Cauchy-sequence type, and raw eventual-closeness relation used in the quantifiers; RS-native units and gap constants appear only as ambient imports, not in the predicate itself.
proof idea
Definitional encoding, not a proved statement. The Prop is the standard $\varepsilon$-$N$ Cauchy schema lifted to sequences of Cauchy ledgers: universal quantification over positive PRC rationals, existential threshold $N$, then pairwise raw eventual closeness of the representatives $U_m$ and $U_n$ for indices past $N$. No lemmas are applied; the body names the raw closeness predicate on the .raw projections of the Cauchy-ledger package.
why it matters
This predicate is the standing hypothesis on every internal completeness blocker in the PRC real construction. Downstream targets that quantify over representative-Cauchy sequences include the diagonal selection target (existence of a Cauchy-ledger limit), the raw diagonal ledger target (construct the raw rational limit ledger and prove Cauchy plus limit), the tail-selection target (choose deep enough raw indices so the diagonal is made of actual terms), and the finite diagonal/representative-tail schedulers at unit-fraction rungs.
In the same module, the completeness target is exactly: every representative-Cauchy sequence of Cauchy ledgers has a representative limit. Closing those targets would finish the internal completeness half of the ordered-field package that underwrites later Recognition calculus (forcing chain analysis over a complete scalar field). The definition itself does not invoke T5–T8 or the RCL; it is pure foundation plumbing for that later use.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.