PRCCauchySeqEventuallyBoundedTarget_proved
plain-language theorem explainer
Every J-cost Cauchy sequence of PRC rationals is eventually trapped in a positive symmetric rational interval. Builders of the PRC real completion cite this to clear eventual boundedness before product continuity and field promotion. The proof anchors past the Cauchy modulus for a fixed positive delta, converts the J-distance bound into a squared rational difference less than one, and expands to explicit bounds.
Claim. Every Cauchy sequence $u$ of PRC rationals under the $J$-cost distance is eventually bounded: there exist a positive PRC rational $B$ and an index $N$ such that for all $n \ge N$, the term $u_n$ lies in the open symmetric interval $(-B,B)$.
background
Primitive Recognition Calculus (PRC) rebuilds arithmetic and analysis from recognition primitives before promoting a real carrier. Sequences live in PRC rationals (PRCRat), ordered and compared via an internal strict order that mirrors the usual rational order after the toRat embedding.
The metric is the $J$-cost distance on those rationals. A fixed positive threshold (the boundedness delta) is chosen small enough that any pair closer than the delta in $J$-distance has squared ordinary difference strictly less than one. That comparison is the content of the sibling lemma relating $J$-distance below the delta to a unit square bound on the embedded difference.
The local target is eventual containment of a Cauchy ledger in a PRC-symmetric rational interval. The module sits in the foundation stack that discharges analytic closure obligations (addition, multiplication, completeness) needed to promote a complete ordered field of PRC reals.
proof idea
Introduce the Cauchy sequence $u$. Apply the Cauchy property at the fixed positive boundedness delta to obtain an index $N$ past which all pairs of terms are $J$-closer than the delta. Anchor at the $N$-th term and set the bound $B := \mathrm{anchor}^2 + 2$.
Positivity of $B$ is immediate after embedding to $\mathbb{Q}$: a square is nonnegative and adding two keeps the value positive (nlinarith).
For $n \ge N$, the Cauchy witness gives $J$-distance from $u_n$ to the anchor below the delta. The sibling square-difference lemma turns that into $(x-q)^2 < 1$ on the embedded rationals. Two short nlinarith steps with nonnegativity of shifted squares yield $-1 < x-q < 1$. Expanding against $B = q^2+2$ then proves both $-B < u_n$ and $u_n < B$ after rewriting the PRC order via toRat.
why it matters
Eventual boundedness is the missing half of multiplication closure for Cauchy ledgers: once terms sit in a fixed rational box, bounded product continuity finishes the product of two Cauchy sequences. The product-continuity certificate uses this theorem exactly that way, feeding PRCRealMulClosureTarget_of_bounded_continuity.
It is also packaged into the real boundedness-modulus certificate (delta positivity plus the square bound) and into the promoted complete-ordered-field certificate that assembles carrier, embedding, and closure facts. The inline note after the proof marks this as Step 10b closure: eventual boundedness is done, so the remaining multiplication blocker is only bounded product continuity.
In the broader Recognition stack this is infrastructure, not a physics landmark: it clears an analytic obligation on the way from the forcing chain's arithmetic layer toward a usable real continuum on which mass ladders and constants can be stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.