Encyclopedia Foundation Foundation Primitive Recognition Calculus Real Order Congruence Prcraw Eventuall

ARTICLE 2 claims 2 theorems

Foundation Primitive Recognition Calculus Real Order Congruence Prcraw Eventuall

In building real numbers from recognition sequences, this theorem shows that 'eventually no larger' is a well-defined comparison, not an artifact of how a sequence is represented.

Verify this page

Order survives equivalence

The real numbers are often built from sequences of rationals: two sequences name the same real number when their difference shrinks toward zero. In Recognition Science, the framework constructs its own real numbers from recognition sequences, where each entry records a discrete act of comparison rather than a measured quantity. The theorem PRCRawEventuallyLe_of_null_equiv answers a basic question about that construction: if two sequences represent the same real number, and one sequence is eventually no larger than another, does the same comparison hold for the equivalent sequences?

The answer is yes, and the proof is a formal theorem in the framework's machine-checked library. The statement takes two pairs of sequences, where each pair is null-equivalent, meaning their differences converge to zero. If the first raw sequence is eventually less than or equal to the second raw sequence, then the same eventual ordering holds for the equivalent sequences. This property is called order congruence: the relation 'eventually no larger' respects the equivalence that identifies sequences naming the same real number.

Why this matters: without order congruence, the real numbers built from recognition sequences would have a badly behaved ordering. One sequence could be 'eventually no larger' than another, but an equivalent sequence could fail the comparison, making the order depend on arbitrary representational choices. The theorem guarantees that comparisons are stable under equivalence, so the ordering on the constructed reals is well-defined. The framework's library records this as PRCRealOrderCongruenceTarget_proved, a certificate that the target property holds.

The theorem does not claim that the eventual ordering is total, that every pair of reals is comparable, or that the ordering is transitive. It establishes only the congruence property: equivalence preserves the 'eventually no larger' relation. It also does not assert that the recognition sequences themselves converge in any metric sense, only that the null-equivalence relation behaves correctly with respect to the raw ordering. The framework's construction of real numbers with a well-defined order is a stepping stone, not a full theory of ordered fields.

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
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

What this page does not claim

The theorem does not prove that the eventual ordering is total or transitive. It does not show that recognition sequences converge in a metric sense. It does not establish the full structure of an ordered field on the constructed reals.

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