PRCRealFiniteDiagonalScheduleTarget
plain-language theorem explainer
Packages the finite-rung diagonal scheduling goal: for a representative-Cauchy family of PRC Cauchy ledgers, one pair of index maps meets raw eventual-closeness, row-tail, and representative finite-tail bounds at every unit-fraction tolerance. Completeness authors cite it as the Prop discharged by the finite diagonal schedule theorem and recorded in the Step 10e sharpened certificate. Body is a pure Prop conjunction, not a proof.
Claim. For every family $U:\mathbb{N}\to\mathrm{PRCCauchySeq}$ that is representative-Cauchy, there exist maps $\mathrm{outer},\mathrm{pick}:\mathbb{N}\to\mathbb{N}$ such that, writing $\varepsilon_r=1/(r+1)$: (i) if $m,n\ge\mathrm{outer}(r)$ then the raw ledgers of $U_m$ and $U_n$ are eventually close at $\varepsilon_r$; (ii) for all $i\le r$, $\mathrm{pick}(r)$ is a row-tail bound for $U_i$ at $\varepsilon_r$; (iii) $\mathrm{pick}(r)$ is a representative finite-tail bound for $U$ at $\varepsilon_r$ past $\mathrm{outer}(r)$ through row $r$.
background
In the Primitive Recognition Calculus, a PRC Cauchy sequence is an orbit-indexed rational ledger whose J-cost distance eventually drops below every positive PRC rational tolerance. Completeness work builds reals from such ledgers and needs uniform control on countable families of them.
Tolerances here are the unit fractions $\varepsilon_r=1/(r+1)$, display machinery for the verifier rather than a new primitive. A row-tail bound says an index $N$ is deep enough that one fixed ledger is Cauchy below a given $\varepsilon$. A representative finite-tail bound says that, past an outer representative threshold, every eligible row $i\le r$ stays J-close to the target row $r$ at depth $N$.
The ambient module develops real completeness for PRC: raw Cauchy realization, quotient points, and diagonal tail selection. This definition sits at the finite-rung scheduling layer, before any completed global tail-selection theorem.
proof idea
Definition only: the right-hand side is the Prop that a finite diagonal scheduler must satisfy. It quantifies over representative-Cauchy families $U$, demands two choice functions $\mathrm{outer}$ and $\mathrm{pick}$, and conjoins three constraints at each rung $r$: raw eventual closeness of ledgers past $\mathrm{outer}(r)$ at unit-fraction $\varepsilon_r$; row-tail bounds via $\mathrm{pick}(r)$ on every row $i\le r$; and the representative finite-tail bound tying $\mathrm{outer}(r)$, row $r$, and $\mathrm{pick}(r)$ together. No tactics or lemmas fire at this declaration; discharge lives in the sibling proved theorem, which combines finite row-tail selection with finite representative-tail selection.
why it matters
Names the exact finite diagonal scheduling obligation used to assemble real completeness. The sibling proved theorem discharges it by gluing finite row-tail and representative-tail selection. Downstream, the Step 10e sharpened certificate records raw-ledger realization, the tail-selection diagonal, and representative completeness for the null-closed reals; that certificate's diagonal path depends on this target (via the raw-diagonal and selection chain).
In framework terms this is bookkeeping inside the PRC real-construction ladder, not a forcing-chain landmark (T5–T8). It keeps finite-rung scheduling separate from the still-stronger global tail-selection theorem the doc-comment flags as not yet claimed here. Without a single Prop packaging both row and representative constraints, the completeness certificate would have to restate the conjunction ad hoc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.