PRCRealFiniteDiagonalScheduleTarget_proved
plain-language theorem explainer
A single finite diagonal scheduler exists for any representative-Cauchy family of PRC Cauchy sequences: one pick function meets both finite row-tail and finite representative-tail bounds at every unit-fraction tolerance rung, together with an outer index that forces pairwise raw eventual closeness. Completeness and tail-selection arguments cite this as the finite-rung merge step. The proof takes the two separate finite selectors and diagonalizes them by pointwise max, then applies the two monotonicity lemmas.
Claim. For every family $U:\mathbb{N}\to\mathrm{PRCCauchySeq}$ that is representative-Cauchy, there exist $outer,pick:\mathbb{N}\to\mathbb{N}$ such that (i) whenever $outer(r)\le m,n$, the raw sequences of $U_m$ and $U_n$ are eventually close at tolerance $1/(r+1)$; (ii) for all $i\le r$, the $i$-th row satisfies the finite row-tail bound at that tolerance with threshold $pick(r)$; (iii) the representative finite tail bound holds at every rung $r$ with the same $pick(r)$.
background
This module builds a constructive real-completeness layer for the Primitive Recognition Calculus: Cauchy sequences of recognition data, unit-fraction tolerances, and finite tail bounds that schedule how far out one must look before a given tolerance is met.
PRCUnitFraction r is the positive rational tolerance $1/(r+1)$. A family $U$ is representative-Cauchy when, at every positive rational $\varepsilon$, some outer index forces pairwise raw eventual closeness of the selected representatives. Finite row-tail selection supplies, for each rung $r$, a pick large enough that every row $i\le r$ obeys the row-tail bound at that tolerance. Finite representative-tail selection does the same for the representative bound, and also returns the outer index from the representative-Cauchy hypothesis.
The target here is still finite-rung scheduling: one raw choice function that satisfies both families of finite constraints simultaneously. It is not yet the completed global tail-selection theorem.
proof idea
Term-mode construction. From the row selector, obtain rowPick witnessing finite row-tail bounds for every rung. From the representative selector (fed the representative-Cauchy hypothesis on $U$), obtain outer and repPick.
Set pick r := max(rowPick r, repPick r). The outer clause is inherited unchanged. For the row clause, Nat.le_max_left plus PRCRowTailBound_mono lifts the row bound from rowPick r to the larger threshold. For the representative clause, Nat.le_max_right plus PRCRepresentativeFiniteTailBound_mono lifts the representative bound likewise.
why it matters
This is the finite diagonal merge that lets later theorems treat row and representative constraints as a single schedule. Downstream, PRCRealTailSelectionTarget_proved immediately unpacks this result and keeps the merged pick (discarding outer for the global tail-selection interface). The sharpened completeness certificate prc_real_completeness_sharpened_certificate sits further up the same module stack, packaging raw Cauchy realization, quotient points, and diagonal selection into one certificate object.
In the Recognition foundation, real completeness is the analytic substrate under ledger limits and Cauchy-style recognition data; this lemma closes the finite-rung half of that story before the global tail-selection step. It does not itself invoke the forcing chain (T5–T8) or the mass ladder; it is pure PRC real-analysis scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.