PRCRealRepresentativeLimit
plain-language theorem explainer
Defines when a Cauchy ledger L is a representative limit of a sequence U of Cauchy ledgers: for every positive PRC-rational eps, the raw ledgers of U_n and L are eventually eps-close. Completeness and diagonal-selection targets cite this predicate as the exact limit clause. The body is a direct Prop abbreviation, not a proved statement.
Claim. A Cauchy ledger $L$ is a representative limit of a sequence $(U_n)$ of Cauchy ledgers if, for every positive PRC-rational $\varepsilon$, there exists $N$ such that for all $n \ge N$ the raw rational ledgers of $U_n$ and $L$ are eventually $\varepsilon$-close.
background
Primitive Recognition Calculus builds an internal real line from distinction arithmetic: integers and rationals arise as orbit quotients (PRC rationals are nonzero-denominator ratio-orbit classes identified by cross-multiplication), then Cauchy sequences of those rationals form Cauchy ledgers. Raw ledgers sit underneath the null-quotient identification that will become the reals.
Eventual closeness of raw ledgers is the concrete metric predicate used before quotienting: two raw sequences agree within a positive rational tolerance from some index onward. The local module packages the ordered-field and completeness interface for this internal construction; the present definition is the limit clause of that interface.
Upstream, PRC rationals and Cauchy-sequence types supply the carriers; the completeness story later asks that every representative-Cauchy sequence of ledgers admit a ledger limit in exactly this sense.
proof idea
Definitional abbreviation only. The predicate expands to a standard $\varepsilon$-$N$ limit statement quantified over positive PRC rationals, with closeness checked on raw ledgers via the existing eventual-closeness relation. No lemmas are applied and no tactics run.
why it matters
This is the exact limit clause inside the internal completeness blocker. Downstream, both PRCRealCompletenessTarget and PRCRealDiagonalSelectionTarget are universal statements that every representative-Cauchy sequence of Cauchy ledgers admits some ledger $L$ satisfying this predicate. The raw-diagonal packaging theorem discharges the quotient-level target by building such an $L$ from a raw diagonal ledger.
In the Recognition foundation stack, completeness of the null quotient is the step that turns the Cauchy-ledger calculus into an ordered complete field usable by later forcing and continuum constructions. The definition itself proves nothing; it names the diagonal theorem's conclusion so the open completeness target can be stated without inline $\varepsilon$-$N$ noise.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.