Encyclopedia Foundation Foundation Primitive Recognition Calculus Real Order Congruence Prcreal Order Co

ARTICLE 3 claims 2 theorems 1 model

Foundation Primitive Recognition Calculus Real Order Congruence Prcreal Order Co

When two descriptions of the same real number are interchangeable, the order between numbers must stay the same; this theorem proves that it does.

Verify this page

Order that survives identification

The real numbers are often built as limits of rational sequences, but a single real number has many different sequences converging to it. The framework's recognition calculus, its discrete record of events, treats two sequences as the same real number when their difference tends to zero. The question is whether this identification respects the usual ordering: if one sequence is eventually below another, does that remain true after swapping in equivalent sequences?

The declaration PRCRealOrderCongruenceTarget_proved answers yes. It establishes that the order relation on the framework's real numbers is congruent with the equivalence relation that defines them. If two sequences are equivalent, then one is eventually at most the other exactly when their replacements are too. The proof uses two supporting facts: the order relation survives replacement by equivalent sequences in both directions, and the equivalence relation is symmetric. The result is a machine-checked theorem in the framework's library of formal theorems, with the certificate structure PRCRealOrderCongruenceCertificate recording the proof as a single object.

This matters because it closes a gap that can silently break a construction of the reals. Without order congruence, two descriptions of the same number could disagree about which of two numbers is smaller, making comparisons meaningless. The theorem guarantees that the framework's real numbers carry a well-defined order, so any later result that relies on comparing numbers can proceed safely.

In Recognition Science, this is one step in building the real numbers from the primitive recognition calculus. The framework models reality as a ledger of recognition events, and this theorem ensures that the order on the resulting real numbers is stable under the identification of equivalent sequences. It does not, however, claim that the real numbers are the only structure that satisfies this property, nor does it say anything about how the order behaves under arithmetic operations such as addition or multiplication.

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
MODEL PRCRealOrderCongruenceCertificate · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealOrderCongruence.lean
PRCRealOrderCongruenceCertificate · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealOrderCongruence.lean:197 
structure PRCRealOrderCongruenceCertificate : Prop where
  order_congruence : PRCRealOrderCongruenceTarget

What this page does not claim

The theorem does not claim that order congruence holds for arithmetic operations like addition or multiplication. The theorem does not claim that the framework's real numbers are the only structure satisfying this order congruence property. The theorem does not claim anything about the uniqueness or existence of the real numbers themselves.

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