PRCRealOrderCongruenceCertificate
plain-language theorem explainer
Certificate that the eventual order on PRC Cauchy sequences descends to the null-distance quotient. Anyone assembling the internal reals as an ordered field cites this bundle. It is a one-field Prop structure whose sole obligation is the order-congruence target (null-equivalent pairs preserve eventual inequality both ways).
Claim. A certificate asserting: whenever two pairs of PRC Cauchy sequences are null-equivalent ($u \sim u'$ and $v \sim v'$), the raw eventual order holds for $(u,v)$ if and only if it holds for $(u',v')$. Equivalently, eventual $\le$ is well-defined on the null-distance quotient.
background
In the Primitive Recognition Calculus (PRC) layer, candidate reals are Cauchy sequences of rationals (or rat-like data) equipped with a null-distance relation: two sequences are null-equivalent when their difference is eventually smaller than every positive rational scale. The raw order is eventual inequality of the underlying sequences, not yet a relation on equivalence classes.
The upstream target states the exact blocker for that descent: null-equivalence of both arguments must preserve eventual $\le$ in both directions. Without it, the quotient cannot carry a well-defined partial order, and the complete ordered-field packaging cannot start.
This module sits after product-continuity work and before the promoted complete ordered-field certificate. Locally it only packages the order-congruence obligation as a named Prop structure.
proof idea
No proof body: this is a Prop-valued structure definition with a single field. Inhabiting it means supplying a proof of the order-congruence target (null-equivalence preserves raw eventual $\le$). The sibling theorem that fills the certificate simply assigns the already-proved target to that field.
why it matters
Order congruence is a gate on the path from raw PRC Cauchy data to an internal ordered field. Downstream, the promoted Step-10 certificate requires closed operations and congruence surfaces on the null quotient; this certificate is the order half of that surface. The same object is wired into the first-pass PRC kernel bundle as part of the analytic specification chain (K7/A2 style packaging, not yet full inevitability).
In the broader Recognition stack this is foundation plumbing rather than a T0–T8 forcing step: it makes the real carrier usable so later mass, $\phi$-ladder, and continuum arguments can sit on a genuine ordered field rather than on sequence representatives. The companion theorem that constructs the certificate discharges the blocker named in the target's doc-comment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.