IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealOrderCongruence
Module proving that the order on primitive recognition reals descends through null-equivalence: if two Cauchy-style representatives are equivalent, their eventual order relations agree. Supplies rational square bounds linking J-cost distance to modulus and order deltas, then packages a certificate that the order-congruence target is discharged. Cited by the PRC kernel and the real-completeness layer when forming a well-ordered quotient.
claimOn the primitive recognition real line, the eventual order $\le$ is congruent under null-equivalence: if $x \sim 0$ and $y \sim 0$ in the raw Cauchy sense, then $x \le y$ eventually if and only if the identified classes satisfy the same relation. Quantitative control is via $J$-cost distance: small modulus implies small squared and absolute differences, with rational square bounds $q^2 < r^2$ used as comparison scaffolding.
background
Primitive Recognition Calculus builds a real line from recognition cost data before classical completeness is assumed. The cost functional is the unique $J$ forced by the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$. Distances derived from $J$ metrize the raw sequences that will become reals.
Null-equivalence identifies sequences that differ by a null (vanishing) defect. For the quotient to carry a partial order, the raw eventual order must be invariant under that identification. The preceding module RealProductContinuity already ensures multiplicative structure behaves continuously; this module handles the order side.
Sibling lemmas give concrete comparison tools: rational square bounds, implications from modulus control on $J$-cost distance to squared and absolute gaps, and transfer of eventual $\le$ across null pairs.
proof idea
The module is a short chain of comparison lemmas, not a single deep induction. First, elementary rational inequalities bound squares. Those feed estimates showing that a small $J$-cost modulus forces small squared and absolute differences of representatives. From the absolute-difference control one obtains that eventual order is preserved when either side is replaced by a null-equivalent sequence. The target proposition is then marked proved and wrapped in a named certificate object for downstream import.
why it matters in Recognition Science
Without order congruence, the PRC real quotient would not be an ordered field candidate, blocking completeness and the kernel interface that later layers import. Downstream modules Kernel and RealCompleteness both import this file, so the certificate is the hand-off that order is well-defined on classes. In the broader Recognition forcing chain this sits under the foundation that eventually supports $D=3$, the eight-tick octave, and the $\phi$-ladder mass formula; locally it is the order half of making recognition reals usable as a continuum.
scope and limits
- Does not construct the real quotient itself; only order congruence on raw data.
- Does not prove multiplicative continuity; that lives in RealProductContinuity.
- Does not establish completeness, least-upper-bound property, or Archimedeanness.
- Does not derive physical constants, $J$-uniqueness, or forcing steps T5–T8.
- Does not address complex or higher-dimensional recognition structures.
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