PRCCauchySeqEventuallyBoundedTarget
plain-language theorem explainer
Names the exact proposition that every PRC Cauchy ledger is eventually trapped in a symmetric positive rational window. Analysts building real multiplication from J-cost Cauchy data cite it as the boundedness half of the product-closure hypotheses. The body is a one-line universal quantification over Cauchy sequences of the raw eventual-boundedness predicate.
Claim. The target proposition asserts: for every PRC Cauchy sequence $u$ (an orbit-indexed rational ledger whose $J$-cost distances eventually fall below every positive rational tolerance), the underlying raw rational ledger is eventually bounded, i.e. there exist a positive PRC rational $B$ and an index $N$ such that for all $n \ge N$ one has $-B < u_n < B$.
background
Primitive Recognition Calculus builds a real complete ordered field from rational ledgers equipped with the $J$-cost distance rather than absolute value. A PRC Cauchy sequence is a map $\mathbb{N}\to\mathrm{PRCRat}$ whose pairwise $J$-cost distances eventually drop below every positive PRC rational tolerance.
Forgetting the Cauchy certificate yields a raw rational ledger. Eventual boundedness of a raw ledger means: some positive PRC rational $B$ and some $N$ exist so that all later terms lie strictly inside the open symmetric interval $(-B,B)$. Membership in such windows is the local analytic setting needed before product estimates can close.
This module packages the exact Prop that every Cauchy ledger satisfies that eventual bound. Downstream multiplication closure and congruence are stated conditionally on this target together with a bounded product-continuity modulus.
proof idea
Definitional, not a proof. The body is the single universal statement $\forall u:\mathrm{PRCCauchySeq},;\mathrm{PRCRawEventuallyBounded}(u.\mathrm{raw})$, wiring the raw eventual-boundedness predicate to every completed Cauchy ledger via the forgetful map that extracts the term sequence.
why it matters
This is the named boundedness half of the real-multiplication interface in Primitive Recognition Calculus. The proved discharge PRCCauchySeqEventuallyBoundedTarget_proved shows every $J$-cost Cauchy ledger is eventually contained in a PRC symmetric rational interval, and the Step 10b certificate records that once boundedness is closed the remaining blocker is only bounded product-continuity.
Conditional theorems PRCRealMulClosureTarget_of_bounded_continuity and PRCRealMulCongruenceTarget_of_bounded_continuity take this target (plus the product-continuity target) as hypotheses and produce product Cauchy closure and product congruence. The conditional certificate structure packages both targets as the reduction of multiplication to boundedness plus continuity. Without this Prop name, the real-field multiplication layer cannot state its remaining obligations cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.