PRCRawEventuallyLe_of_null_equiv
plain-language theorem explainer
Null-equivalent Cauchy sequences preserve the raw eventual order: if u ~ u' and v ~ v' and the raw sequence of u is eventually ≤ that of v, then the same holds for u' and v'. Anyone building the ordered field of PRC reals from Cauchy sequences cites this for well-definedness of ≤ on equivalence classes. The proof shrinks the tolerance through auxiliary positive rationals and applies a J-cost absolute-difference bound at each large index.
Claim. Let $u,u',v,v'$ be PRC Cauchy sequences. If $u$ is null-equivalent to $u'$, $v$ is null-equivalent to $v'$, and the raw sequence of $u$ is eventually less-or-equal to the raw sequence of $v$, then the raw sequence of $u'$ is eventually less-or-equal to the raw sequence of $v'$.
background
Primitive Recognition Calculus builds a real line from Cauchy sequences of PRC rationals, then quotients by null equivalence (pairs of sequences whose J-cost distance tends to zero). The raw eventual order PRCRawEventuallyLe is the pre-quotient comparison: for every positive rational tolerance $\varepsilon$, past some index $N$ one has $u_n < v_n + \varepsilon$ in the embedded rationals.
Null equivalence alone does not automatically transport inequalities, because each pair $(u,u')$ and $(v,v')$ only becomes close after its own $N$, and the comparison tolerance must absorb both perturbations. The module therefore isolates congruence of the raw order under null equivalence before lifting ≤ to equivalence classes.
Upstream support includes the PRC rational embedding toRat, positivity transfer positive_iff_toRat_pos, and the sibling bound PRCJCostDistance_abs_diff_lt_of_lt_order_delta, which converts a small J-cost distance into a two-sided rational absolute gap controlled by a chosen $\gamma$.
proof idea
Fix a positive rational tolerance $\varepsilon$. Build auxiliaries $\gamma = \varepsilon/4$, $\eta = \gamma^2$, and a still smaller positive $\delta$ polynomial in $\eta$ so that the J-cost absolute-difference lemma applies with room to spare. From null equivalence of $u\sim u'$ and $v\sim v'$ at scale $\delta$, and from the given eventual inequality at scale $\gamma$, take $N$ larger than all three witness indices.
For $n\ge N$, apply PRCJCostDistance_abs_diff_lt_of_lt_order_delta to the pairs $(u_n,u'_n)$ and $(v_n,v'_n)$ to get $|u_n-u'_n|<\gamma$ and $|v_n-v'_n|<\gamma$ after toRat. Combine with $u_n < v_n+\gamma$ by ordinary rational arithmetic (nlinarith) to conclude $u'_n < v'_n+\varepsilon$. The max-of-indices bookkeeping uses ordinary Nat.le_max_* and le_trans.
why it matters
This is the left-to-right half of order congruence for PRC reals. The sole downstream consumer PRCRealOrderCongruenceTarget_proved packages both directions into the target proposition that null equivalence preserves eventual ≤, which is exactly what is needed to descend the preorder to the quotient and obtain a well-defined ordered field structure.
In the Recognition foundation stack this sits inside the Primitive Recognition Calculus real-construction layer: before mass ladders, eight-tick structure, or forcing-chain landmarks (T5–T8) can speak about continuum quantities, the ordered reals must be congruence-correct. Closing this lemma removes a scaffolding risk that ≤ on Cauchy classes would depend on representatives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.