Encyclopedia Foundation Foundation Primitive Recognition Calculus Real Order Congruence

ARTICLE 3 claims 2 theorems 1 model

Foundation Primitive Recognition Calculus Real Order Congruence

Real order congruence is a consistency condition: it guarantees that the ordering of real numbers does not depend on which approximating sequence you use to represent them.

Verify this page

Real order congruence

Real numbers are often defined as limits of sequences of rational numbers. A single real number can be represented by many different sequences. Real order congruence is the property that makes this representation well-behaved: if one sequence is eventually less than or equal to another, then any two equivalent sequences (sequences that converge to the same limit) must preserve that ordering. In plain terms, the ordering of real numbers does not depend on which approximating sequence you choose.

This property is not automatic. It must be proved for any particular construction of the real numbers. In the Recognition Science framework, the real numbers are built from a primitive recognition calculus, a discrete ledger of rational-valued recognition events. The framework's machine-checked library of formal theorems proves that real order congruence holds for this construction. The proof works by showing that the ordering relation is preserved under the equivalence relation that identifies sequences converging to the same real number.

The theorem PRCRealOrderCongruenceTarget_proved establishes this congruence directly. It states that if two pairs of sequences are null-equivalent (meaning they converge to the same limit), then the eventual ordering of one pair implies the eventual ordering of the other. The proof uses a helper theorem, PRCRawEventuallyLe_of_null_equiv, which shows that the raw ordering relation is invariant under null equivalence. This invariance is the core of the congruence property.

Why does this matter? Without real order congruence, the real numbers would be ill-defined: different representations of the same number could lead to different ordering conclusions. The framework's proof ensures that its construction of the real numbers is sound. This is a foundational step, not a computational one. It does not tell you how to compute with real numbers; it tells you that the framework's definition of them is consistent.

MODEL PRCRealOrderCongruenceCertificate · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealOrderCongruence.lean
PRCRealOrderCongruenceCertificate · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealOrderCongruence.lean:197 
structure PRCRealOrderCongruenceCertificate : Prop where
  order_congruence : PRCRealOrderCongruenceTarget
THEOREM PRCRealOrderCongruenceTarget_proved · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealOrderCongruence.lean
PRCRealOrderCongruenceTarget_proved · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealOrderCongruence.lean:187 
theorem PRCRealOrderCongruenceTarget_proved :
    PRCRealOrderCongruenceTarget := by
  intro u u' v v' huu hvv
  constructor
  · intro hle
    exact PRCRawEventuallyLe_of_null_equiv huu hvv hle
  · intro hle
    exact PRCRawEventuallyLe_of_null_equiv
      (PRCNullEquivalent.symm huu) (PRCNullEquivalent.symm hvv) hle
THEOREM PRCRawEventuallyLe_of_null_equiv · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealOrderCongruence.lean
PRCRawEventuallyLe_of_null_equiv · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealOrderCongruence.lean:92 
theorem PRCRawEventuallyLe_of_null_equiv
    {u u' v v' : PRCCauchySeq}
    (huu : PRCNullEquivalent u u')
    (hvv : PRCNullEquivalent v v')
    (hle : PRCRawEventuallyLe u.raw v.raw) :
    PRCRawEventuallyLe u'.raw v'.raw := by
  intro eps heps
  let two : PRCRat := (1 : PRCRat) + (1 : PRCRat)
  let four : PRCRat := two * two
  let gamma : PRCRat := eps * (four⁻¹)
  let eta : PRCRat := gamma * gamma
  let delta : PRCRat := (eta * eta) * ((four * ((1 : PRCRat) + eta))⁻¹)
  have heps_pos : 0 < eps.toRat :=
    (PRCRat.positive_iff_toRat_pos eps).mp heps
  have htwo : two.toRat = (2 : ℚ) := by
    dsimp [two]
    change (PRCRat.add PRCRat.one PRCRat.one).toRat = (2 : ℚ)
    rw [PRCRat.toRat_add, PRCRat.one_toRat]
    norm_num
  have hfour : four.toRat = (4 : ℚ) := by
    dsimp [four]
    change (PRCRat.mul two two).toRat = (4 : ℚ)
    rw [PRCRat.toRat_mul]
    norm_num [htwo]
  have hgamma_toRat : gamma.toRat = eps.toRat / 4 := by
    dsimp [gamma]
    rw [PRCRat.toRat_mul, PRCRat.toRat_recip, hfour]
    ring
  have hgamma_pos_rat : 0 < gamma.toRat := by
    rw [hgamma_toRat]
    positivity
  have hgamma_pos : PRCRat.positive gamma := by
    rw [PRCRat.positive_iff_toRat_pos]
    exact hgamma_pos_rat
  have heta_toRat : eta.toRat = gamma.toRat * gamma.toRat := by
    simp [eta, PRCRat.toRat_mul]
  have heta_pos_rat : 0 < eta.toRat := by
    rw [heta_toRat]
    nlinarith
  have h_one_add_eta :
      (((1 : PRCRat) + eta).toRat) = 1 + eta.toRat := by
    change (PRCRat.add PRCRat.one eta).toRat = 1 + eta.toRat
    rw [PRCRat.toRat_add, PRCRat.one_toRat]
  have hdelta_toRat :
      delta.toRat =
        eta.toRat * eta.toRat / (4 * (1 + eta.toRat)) := by
    dsimp [delta]
    simp [PRCRat.toRat_mul, PRCRat.toRat_recip, PRCRat.toRat_add,
      PRCRat.one_toRat, hfour]
    have hden_pos : (0 : ℚ) < 4 * (1 + eta.toRat) := by positivity
    field_simp [ne_of_gt hden_pos]
  have hdelta_pos_rat : 0 < delta.toRat := by
    rw [hdelta_toRat]
    positivity
  have hdelta_pos : PRCRat.positive delta := by
    rw [PRCRat.positive_iff_toRat_pos]
    exact hdelta_pos_rat
  rcases huu delta hdelta_pos with ⟨Nu, hNu⟩
  rcases hvv delta hdelta_pos with ⟨Nv, hNv⟩
  rcases hle gamma hgamma_pos with ⟨Nle, hNle⟩
  refine ⟨max (max Nu Nv) Nle, ?_⟩
  intro n hn
  have hNu_n : Nu ≤ n :=
    le_trans (Nat.le_max_left Nu Nv)
      (le_trans (Nat.le_max_left (max Nu Nv) Nle) hn)
  have hNv_n : Nv ≤ n :=
    le_trans (Nat.le_max_right Nu Nv)
      (le_trans (Nat.le_max_left (max Nu Nv) Nle) hn)
  have hNle_n : Nle ≤ n :=
    le_trans (Nat.le_max_right (max Nu Nv) Nle) hn
  have hu_close := PRCJCostDistance_abs_diff_lt_of_lt_order_delta
    (a := u.term n) (b := u'.term n) (gamma := gamma) (delta := delta)
    hgamma_pos hdelta_pos (by simp [hdelta_toRat, heta_toRat])
    (hNu n hNu_n)
  have hv_close := PRCJCostDistance_abs_diff_lt_of_lt_order_delta
    (a := v.term n) (b := v'.term n) (gamma := gamma) (delta := delta)
    hgamma_pos hdelta_pos (by simp [hdelta_toRat, heta_toRat])
    (hNv n hNv_n)
  have hu'_lt : (u'.term n).toRat < (u.term n).toRat + gamma.toRat := by
    rcases hu_close with ⟨hlo, _hhi⟩
    nlinarith
  have hv_lt : (v.term n).toRat < (v'.term n).toRat + gamma.toRat := by
    rcases hv_close with ⟨hlo, _hhi⟩
    nlinarith
  have huv_lt : (u.term n).toRat < (v.term n).toRat + gamma.toRat := by
    have hle_n := hNle n hNle_n
    rw [PRCRat.lt_iff_toRat_lt] at hle_n
    simpa [PRCCauchySeq.raw, PRCRat.toRat_add] using hle_n
  rw [PRCRat.lt_iff_toRat_lt]
  simp [PRCCauchySeq.raw, PRCRat.toRat_add]
  have hthree_gamma_lt_eps : 3 * gamma.toRat < eps.toRat := by
    rw [hgamma_toRat]
    nlinarith
  nlinarith

What this page does not claim

This does not claim that real order congruence is a new mathematical discovery; it is a standard property proved for a specific construction. This does not claim that the framework's construction of real numbers is the only one or that it is simpler than classical constructions.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealOrderCongruence.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND