PRCRealOrderCongruenceTarget
plain-language theorem explainer
The order relation on raw rational ledgers is well-defined on the null-distance quotient of PRC Cauchy sequences: if two pairs of ledgers are pairwise null-equivalent, eventual non-strict order holds for one pair exactly when it holds for the other. Anyone building the ordered-field structure on the PRC real completion cites this as the exact congruence blocker. It is a pure Prop target, discharged later by a dedicated certificate theorem.
Claim. For all PRC Cauchy sequences $u,u',v,v'$, if $u$ is null-equivalent to $u'$ and $v$ is null-equivalent to $v'$, then the raw ledger of $u$ is eventually non-strictly below the raw ledger of $v$ if and only if the same holds for $u'$ and $v'$.
background
In the Primitive Recognition Calculus, reals are built from Cauchy sequences of PRC rationals. A PRC Cauchy sequence is an orbit-indexed rational ledger whose J-cost distance eventually drops below every positive PRC rational tolerance. Two such sequences are null-equivalent when their termwise J-cost distance itself eventually falls below every positive tolerance; that relation is the intended kernel of the real quotient.
The candidate order is not imposed on quotient classes directly. First one forgets a Cauchy ledger to its raw term map, then asks whether $u_n < v_n + \varepsilon$ eventually holds for every positive rational $\varepsilon$. That is the pointwise non-strict order candidate on raw ledgers.
This module packages the exact blockers needed before the null quotient can carry a complete ordered-field structure. The present definition isolates the congruence demand for that order: the eventual comparison must be insensitive to replacing either argument by a null-equivalent ledger.
proof idea
No proof body: this is a bare Prop definition packing a four-variable universal statement. The mathematical content is the biconditional that eventual raw order is invariant under pairwise null-equivalence. Discharge happens downstream in the certificate theorem, which splits the biconditional and applies the one-sided transfer lemma for eventual order under null equivalence in each direction.
why it matters
Without order congruence, the null-distance quotient cannot inherit a well-defined $\le$, so the complete ordered-field layer stalls. Downstream, the target is a field of the order-congruence certificate and appears in the promoted Step 10 certificate for the internal null quotient. It is also bundled among the exact blockers for the next real-completion phase (alongside add/mul/neg closure and congruence targets).
In the Recognition forcing chain this sits in the foundation layer that constructs the real carrier before constants, the phi-ladder, or continuum physics are stated. Closing it is a packaging step toward a Mathlib-facing complete ordered field, not a new physical law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.