PRCRawEventuallyBounded
plain-language theorem explainer
Eventual boundedness for a raw PRC-rational ledger: some positive bound B traps all tail terms strictly inside (-B, B). Analysts building real multiplication from Cauchy ledgers cite it as the exact boundedness predicate. The body is a pure Prop definition (existential tail bound), not a proved theorem.
Claim. A raw rational ledger $s$ is eventually bounded if there exists a positive PRC-rational $B>0$ and an index $N$ such that for every $n\ge N$, $-B < s(n) < B$ in the PRC-rational order.
background
Primitive Recognition Calculus rebuilds the ordered field of reals from ledger data rather than classical Dedekind or Cauchy constructions imported from Mathlib. PRC rationals are quotient classes of ratio orbits (nonzero-denominator cross-multiplication identification). Positivity means a nonnegative signed numerator that is not balanced with zero; the strict order is the internal nonnegative-difference order with nonzero difference.
A raw rational ledger is a sequence of such PRC rationals. Eventual boundedness asks only that the tail sit inside a symmetric open interval $(-B,B)$ for some positive $B$, not that the whole sequence be bounded from the first index. The surrounding module targets multiplication continuity and closure for real multiplication built from Cauchy ledgers, so this predicate is the exact boundedness language those targets quantify over.
Upstream order and positivity infrastructure (PRC-rational lt and positive) supply the atomic comparisons used in the Prop body.
proof idea
Definitional, not a proof. The Prop is the standard $\exists B>0,\exists N,\forall n\ge N$ tail bound, written with PRC-native positivity and strict order on the ledger values. No lemmas are applied; the declaration only names the predicate later targets quantify over.
why it matters
Feeds the exact Cauchy boundedness target: every PRC Cauchy sequence has eventually bounded raw ledger. That target is the first link in the RealMulBoundedContinuity chain (bounded continuity of $J$-cost distance under multiplication, then real-mul closure and congruence certificates conditional on bounded continuity).
In the Recognition foundation stack this is bookkeeping for constructing $\mathbb{R}$ multiplication without smuggling classical completeness APIs. It does not itself touch the forcing chain T5–T8 or the Recognition Composition Law; it sits lower, ensuring Cauchy ledgers stay inside finite PRC bounds so multiplication and continuity statements can be stated PRC-natively.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.