PRCRealFiniteRepresentativeTailSelectionTarget
plain-language theorem explainer
States the exact finite representative scheduler needed for the PRC real diagonal: given a Cauchy sequence of Cauchy ledgers, there exist outer and pick schedules so that each unit-fraction tolerance rung has a representative threshold and a raw depth realizing all finite tail comparisons up to that rung. Completeness and diagonal-selection authors cite it as the Prop target. It is a pure definition of that target proposition, discharged later by a choose-based proof.
Claim. For every sequence $U$ of PRC Cauchy sequences that is Cauchy as a sequence of null-quotient representatives, there exist schedules $\mathrm{outer},\mathrm{pick}:\mathbb{N}\to\mathbb{N}$ such that: (i) for every rung $r$ and all $m,n\ge\mathrm{outer}(r)$, the raw ledgers of $U_m$ and $U_n$ are eventually $J$-close at tolerance $1/(r+1)$; (ii) for every $r$, the raw index $\mathrm{pick}(r)$ is deep enough that every eligible representative row $i$ with $\mathrm{outer}(r)\le i\le r$ is $J$-close to row $r$ at that depth, again at tolerance $1/(r+1)$.
background
Primitive Recognition Calculus builds reals from orbit-indexed rational ledgers equipped with the $J$-cost distance. A PRC Cauchy sequence is a completed ledger whose $J$-distances eventually fall below every positive PRC rational tolerance. Unit fractions $1/(n+1)$ serve only as a cofinal tolerance schedule for the completeness argument, not as new primitives.
Quantitative closeness of two raw ledgers at fixed tolerance is eventual $J$-closeness past some depth. A sequence of such Cauchy ledgers is representative-Cauchy when its representative tails become eventually close at every positive tolerance. The finite-tail bound then says: once an outer representative threshold is crossed, a single raw depth makes every eligible row $i\le r$ close to the target row $r$.
This module packages the completeness targets for the PRC real null-closed field. The present definition isolates the exact finite scheduler the diagonal construction needs before any existence proof is given.
proof idea
Definition only: the body is the proposition itself, not a proof. It packages two conjuncts under a double existential over schedules outer and pick. The first conjunct is universal eventual raw closeness of pairs of representatives past outer r at unit-fraction tolerance $r$. The second is the finite representative-tail bound at those same parameters. Discharge is deferred to the sibling theorem that chooses outer from representative-Cauchyness at each unit fraction, then chooses pick from the finite-tail bound.
why it matters
This target is the precise interface between representative-Cauchyness and the diagonal ledger used to prove PRC real completeness. Downstream, the proved form feeds the raw-diagonal-from-tail-selection arrow inside the Step 10e sharpened certificate, which records closed raw-ledger realization, the tail-selection diagonal, and representative completeness for the null-closed PRC reals.
In the Recognition foundation stack this sits under the construction of a complete ordered field from recognition ledgers, prior to forcing-chain landmarks (T5 $J$-uniqueness, T6 $\varphi$, T7 eight-tick, T8 $D=3$). Without a finite scheduler that works rung-by-rung at unit fractions, the diagonal selection target cannot be reduced to raw Cauchy data. The definition therefore pins the contract that the completeness certificate must discharge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.