IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealOrderCongruence
Order on primitive-recognition reals is congruent under null-equivalence: equivalent Cauchy-style representatives induce the same comparisons. Anyone assembling the ordered-field layer of PRC reals cites this. The module bounds J-cost distances via rational square estimates, lifts raw eventual order across null classes, and packages a proved congruence certificate.
claimIf $x \sim x'$ and $y \sim y'$ under the null-equivalence used to form primitive recognition reals, then the raw eventual order satisfies $x \le y$ if and only if $x' \le y'$. Thus $\le$ descends to a well-defined order on the quotient. Supporting bounds relate squared J-cost distances to modulus and order-delta controls.
background
Primitive Recognition Calculus builds a real line from recognition data rather than from classical Dedekind or Cauchy postulates alone. Representatives carry a raw eventual order and a null-equivalence (sequences that become arbitrarily close in the recognition metric). For the quotient to be an ordered field, that raw order must be congruent: it must be invariant when either side is replaced by a null-equivalent representative.
The natural comparison tool is the J-cost distance induced by the unique cost $J(x)=(x+x^{-1})/2-1$ from the forcing chain. Continuity of products (imported from the preceding RealProductContinuity module) supplies the algebraic control needed to pass inequalities through multiplication and inversion on positive cones.
This module therefore sits between product continuity and the completeness/kernel layer: it turns metric smallness into order stability on equivalence classes.
proof idea
The argument is lemma-driven, not a single monolithic proof. Rational square bounds control when $p^2 < q^2$ for positive rationals, feeding estimates that a small modulus forces the squared J-cost distance between two representatives below a prescribed threshold. Absolute-difference forms of those estimates convert modulus control into order-delta control.
A separate lemma shows that null-equivalence preserves the raw eventual $\le$ relation. Those pieces discharge a named congruence target, which is then wrapped as an explicit certificate object recording that the target is proved.
why it matters in Recognition Science
Without order congruence the PRC real quotient cannot carry a well-defined $\le$, so every later statement about ordered completeness, least upper bounds, or ordered-field axioms would be ill-typed. Downstream, RealCompleteness imports this module to finish the ordered complete field structure; Kernel imports it as part of the consolidated PRC interface.
In the broader Recognition framework this is infrastructure rather than a forcing-chain landmark: it does not re-derive $J$, $\varphi$, the eight-tick octave, or $D=3$, but it makes the real line those landmarks live on rigorously ordered. The certificate pattern matches other PRC modules that expose a single proved-target token for upstream assembly.
scope and limits
- Does not construct the reals or define null-equivalence; assumes those from earlier PRC modules.
- Does not prove completeness, lub existence, or Archimedeanness; only order congruence on the quotient.
- Does not re-derive J-uniqueness, phi, or dimensional forcing (T5–T8).
- Does not address complex or non-Archimedean extensions of the recognition line.
- Does not by itself install field operations; product continuity is imported, not re-proved here.
used by (2)
depends on (1)
declarations in this module (7)
-
theorem
rat_sq_lt_sq_bounds -
theorem
PRCJCostDistance_sq_diff_lt_of_lt_modulus -
theorem
PRCJCostDistance_abs_diff_lt_of_lt_order_delta -
theorem
PRCRawEventuallyLe_of_null_equiv -
theorem
PRCRealOrderCongruenceTarget_proved -
structure
PRCRealOrderCongruenceCertificate -
theorem
prc_real_order_congruence_certificate