PRCRealOrderCongruenceTarget_proved
plain-language theorem explainer
The eventual order on Cauchy ledgers is invariant under null-equivalence: if u ~ u' and v ~ v' in the J-cost null relation, then u is eventually ≤ v if and only if u' is eventually ≤ v'. Anyone building the ordered real quotient from recognition Cauchy data cites this. The proof is a two-direction application of the one-sided transfer lemma, using symmetry of null-equivalence on the reverse arrow.
Claim. For all Cauchy ledgers $u,u',v,v'$, if $u$ is null-equivalent to $u'$ and $v$ is null-equivalent to $v'$ (J-cost distance eventually smaller than every positive rational), then the raw eventual order $u \le_{\mathrm{ev}} v$ holds if and only if $u' \le_{\mathrm{ev}} v'$.
background
In the Primitive Recognition Calculus, reals are assembled from Cauchy ledgers of rational terms, with closeness measured by the J-cost distance rather than absolute value. Null-equivalence is the intended kernel of the quotient: two ledgers are null-equivalent when, for every positive rational $\varepsilon$, their J-cost distance is eventually $< \varepsilon$. That relation is meant to become equality in the completed real line once transitivity is secured from the J-cost surface.
The raw eventual order compares two sequences by asking whether, from some index on, every term of the first is $\le$ the corresponding term of the second. For this order to descend to the null-distance quotient, it must be insensitive to replacing either argument by a null-equivalent ledger. The target proposition packages exactly that congruence (both directions of the biconditional).
The one-sided transfer lemma already shows that null-equivalence preserves eventual $\le$ in the forward direction. Null-equivalence is symmetric, so the reverse direction is the same lemma after swapping representatives.
proof idea
Term-mode proof by introducing the four ledgers and the two null-equivalence hypotheses, then splitting the biconditional.
Left-to-right: apply the one-sided transfer lemma directly to the given null-equivalences and the assumed eventual order.
Right-to-left: apply the same transfer lemma to the symmetric null-equivalences (swap each pair) and the assumed eventual order on the primed ledgers. No further arithmetic is needed; congruence is pure transport along the kernel.
why it matters
This closes the exact blocker for order descending to the null-distance quotient. The local certificate packages the proved target as the order-congruence field of the order-congruence certificate. Downstream, the promoted complete-ordered-field certificate consumes the same fact (alongside add-closure and add-congruence) when assembling the real carrier, rational embedding, and field operations on the null-closed quotient.
In the Recognition foundation stack this is infrastructure, not a physics law: it lets the ordered continuum arise from J-cost Cauchy data so later forcing steps (T5 J-uniqueness, T6 $\phi$, T7 eight-tick, T8 $D=3$) can sit on a completed ordered field rather than on raw sequences. Without order congruence, inequalities and completeness statements would not be well-defined on equivalence classes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.