PRCRawEventuallyLe
plain-language theorem explainer
Pointwise non-strict order candidate on raw rational ledgers: u is eventually at most v when every positive rational epsilon admits a tail on which u_n is strictly below v_n + eps. Used to equip PRC reals with an order and to prove that order is invariant under null-distance equivalence. Pure definitional Prop with no proof obligations.
Claim. For raw rational ledgers $u,v:\mathbb{N}\to R$ (sequences of PRC rationals), declare $u\preceq v$ if and only if for every positive rational $\varepsilon$ there exists $N\in\mathbb{N}$ such that for all $n\ge N$ one has $u(n)<v(n)+\varepsilon$.
background
In the Primitive Recognition Calculus, rationals (PRCRat) are ratio-orbit quotient classes. A raw completed-orbit rational ledger is simply a sequence $\mathbb{N}\to\mathrm{PRCRat}$, before any Cauchy certificate is attached. The module builds a complete ordered field from these ledgers by Cauchy completion and null-distance quotienting.
The classical real order on Cauchy sequences is not the pointwise order: two sequences may cross infinitely often yet represent the same real, or one may sit strictly below the other only in the limit. The standard fix is an eventually-mod-epsilon comparison: $u\le v$ means $\limsup(u_n-v_n)\le 0$, phrased here with the internal strict order and positivity predicates on PRC rationals.
Upstream, strict order and positivity on PRCRat come from the integer/rational layer (nonnegative nonzero difference of signed orbits). Sibling predicates cover Cauchy-ness and null-equivalence of raw ledgers; this definition supplies the order side of that package.
proof idea
Definitional abbreviation only. The body is the standard quantified formula: universal over positive rational epsilons, existential tail index $N$, then pointwise strict inequality $u,n < v,n + \varepsilon$ for all $n\ge N$. No lemmas are applied; unfolding is the entire content.
why it matters
This is the raw order relation that must descend to the null-distance quotient if PRC reals are to be an ordered field. Downstream, PRCRealOrderCongruenceTarget packages exactly that congruence obligation: null-equivalent Cauchy pairs must agree on whether their raw ledgers satisfy the eventually-le relation. The companion theorem PRCRawEventuallyLe_of_null_equiv discharges one direction of that invariance.
In the broader Recognition stack this sits in the foundation layer that reconstructs $\mathbb{R}$ from recognition orbits, before J-cost geometry and the forcing chain (T5 J-uniqueness onward) are interpreted over a complete ordered field. Without a well-defined order on the completion, comparison of costs, thresholds such as the Berry bound $\varphi^{-1}$, and ladder inequalities cannot be stated internally.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.