Encyclopedia Foundation Foundation Primitive Recognition Calculus Real Mul Bounded Continuity Prccauchy

ARTICLE 3 claims 1 theorem 2 models

Foundation Primitive Recognition Calculus Real Mul Bounded Continuity Prccauchy

A Cauchy sequence of rational numbers is eventually bounded; the Recognition Science library states this as a target for its primitive ledger sequences.

Verify this page

The boundedness target

A Cauchy sequence of rational numbers has a useful property: after some finite index, every term lies within a fixed interval. This is a standard fact in analysis. The Recognition Science framework restates it for its own primitive objects. The declaration PRCCauchySeqEventuallyBoundedTarget is a formal statement, a target, that every Cauchy sequence in the framework's primitive recognition calculus is eventually bounded.

The framework models a ledger, a discrete record of events, as a sequence of rational numbers. A Cauchy sequence is one where terms get arbitrarily close to each other as the index grows. The target says: for any such sequence, there exists a positive rational bound B and an index N such that for all n at least N, the term s n lies strictly between -B and B. This is the exact boundedness property, stated with strict inequalities.

The library proves a conditional theorem: if this boundedness target holds, and if a separate product-continuity target holds, then the real multiplication closure and congruence targets follow. In plain terms, the framework shows that eventual boundedness plus a continuity condition on multiplication is enough to build a well-behaved real multiplication from the primitive rational ledger. The certificate structure packages these two conditions as the sufficient ingredients.

The declaration does not claim that the boundedness target is proved. It is a target, a statement of what must hold. The library does not yet show that every Cauchy sequence in the primitive calculus is eventually bounded; that remains an open step. The conditional theorems show what follows if the target is established, not that it is established.

MODEL PRCCauchySeqEventuallyBoundedTarget · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealMulBoundedContinuity.lean
PRCCauchySeqEventuallyBoundedTarget · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealMulBoundedContinuity.lean:28 
/-- Exact boundedness target for Cauchy ledgers. -/
def PRCCauchySeqEventuallyBoundedTarget : Prop :=
  ∀ u : PRCCauchySeq, PRCRawEventuallyBounded u.raw
MODEL PRCCauchySeqEventuallyBoundedTarget · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealMulBoundedContinuity.lean
PRCCauchySeqEventuallyBoundedTarget · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealMulBoundedContinuity.lean:28 
/-- Exact boundedness target for Cauchy ledgers. -/
def PRCCauchySeqEventuallyBoundedTarget : Prop :=
  ∀ u : PRCCauchySeq, PRCRawEventuallyBounded u.raw
THEOREM PRCRealMulClosureTarget_of_bounded_continuity · PRCRealMulCongruenceTarget_of_bounded_continuity · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealMulBoundedContinuity.lean
PRCRealMulClosureTarget_of_bounded_continuity · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealMulBoundedContinuity.lean:66 
/-- Conditional proof of product Cauchy closure from eventual boundedness and
bounded product-continuity. -/
theorem PRCRealMulClosureTarget_of_bounded_continuity
    (hbounded : PRCCauchySeqEventuallyBoundedTarget)
    (hmul_cont : PRCJCostDistanceMulBoundedContinuityTarget) :
    PRCRealMulClosureTarget := by
  intro u v eps heps
  rcases hbounded u with ⟨Bu, hBu_pos, NuB, hNuB⟩
  rcases hbounded v with ⟨Bv, hBv_pos, NvB, hNvB⟩
  let B : PRCRat := Bu + Bv + 1
  have hB_pos : PRCRat.positive B := by
    rw [PRCRat.positive_iff_toRat_pos]
    have hBu : (0 : ℚ) < Bu.toRat := (PRCRat.positive_iff_toRat_pos Bu).mp hBu_pos
    have hBv : (0 : ℚ) < Bv.toRat := (PRCRat.positive_iff_toRat_pos Bv).mp hBv_pos
    simp [B]
    nlinarith
  have hBu_le_B : Bu.toRat ≤ B.toRat := by
    have hBv : (0 : ℚ) < Bv.toRat := (PRCRat.positive_iff_toRat_pos Bv).mp hBv_pos
    simp [B]
    nlinarith
  have hBv_le_B : Bv.toRat ≤ B.toRat := by
    have hBu : (0 : ℚ) < Bu.toRat := (PRCRat.positive_iff_toRat_pos Bu).mp hBu_pos
    simp [B]
    nlinarith
  rcases hmul_cont eps B heps hB_pos with ⟨delta, hdelta_pos, hdelta⟩
  rcases u.cauchy delta hdelta_pos with ⟨NuC, hNuC⟩
  rcases v.cauchy delta hdelta_pos with ⟨NvC, hNvC⟩
  let N := max (max NuB NvB) (max NuC NvC)
  refine ⟨N, ?_⟩
  intro m n hm hn
  have hNuB_m : NuB ≤ m := le_trans (le_trans (Nat.le_max_left NuB NvB)
    (Nat.le_max_left (max NuB NvB) (max NuC NvC))) hm
  have hNuB_n : NuB ≤ n := le_trans (le_trans (Nat.le_max_left NuB NvB)
    (Nat.le_max_left (max NuB NvB) (max NuC NvC))) hn
  have hNvB_m : NvB ≤ m := le_trans (le_trans (Nat.le_max_right NuB NvB)
    (Nat.le_max_left (max NuB NvB) (max NuC NvC))) hm
  have hNvB_n : NvB ≤ n := le_trans (le_trans (Nat.le_max_right NuB NvB)
    (Nat.le_max_left (max NuB NvB) (max NuC NvC))) hn
  have hNuC_m : NuC ≤ m := le_trans (le_trans (Nat.le_max_left NuC NvC)
    (Nat.le_max_right (max NuB NvB) (max NuC NvC))) hm
  have hNuC_n : NuC ≤ n := le_trans (le_trans (Nat.le_max_left NuC NvC)
    (Nat.le_max_right (max NuB NvB) (max NuC NvC))) hn
  have hNvC_m : NvC ≤ m := le_trans (le_trans (Nat.le_max_right NuC NvC)
    (Nat.le_max_right (max NuB NvB) (max NuC NvC))) hm
  have hNvC_n : NvC ≤ n := le_trans (le_trans (Nat.le_max_right NuC NvC)
    (Nat.le_max_right (max NuB NvB) (max NuC NvC))) hn
  have hu_m_small : PRCRat.InBound B (u.term m) :=
    PRCRat.InBound_mono hBu_le_B (hNuB m hNuB_m)
  have hu_n_small : PRCRat.InBound B (u.term n) :=
    PRCRat.InBound_mono hBu_le_B (hNuB n hNuB_n)
  have hv_m_small : PRCRat.InBound B (v.term m) :=
    PRCRat.InBound_mono hBv_le_B (hNvB m hNvB_m)
  have hv_n_small : PRCRat.InBound B (v.term n) :=
    PRCRat.InBound_mono hBv_le_B (hNvB n hNvB_n)
  exact hdelta (u.term m) (u.term n) (v.term m) (v.term n)
    hu_m_small hu_n_small hv_m_small hv_n_small
    (hNuC m n hNuC_m hNuC_n)
    (hNvC m n hNvC_m hNvC_n)
PRCRealMulCongruenceTarget_of_bounded_continuity · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealMulBoundedContinuity.lean:125 
/-- Conditional proof of product congruence from eventual boundedness and
bounded product-continuity. -/
theorem PRCRealMulCongruenceTarget_of_bounded_continuity
    (hbounded : PRCCauchySeqEventuallyBoundedTarget)
    (hmul_cont : PRCJCostDistanceMulBoundedContinuityTarget) :
    PRCRealMulCongruenceTarget := by
  intro u u' v v' huu hvv eps heps
  rcases hbounded u with ⟨Bu, hBu_pos, NuB, hNuB⟩
  rcases hbounded u' with ⟨Bu', hBu'_pos, Nu'B, hNu'B⟩
  rcases hbounded v with ⟨Bv, hBv_pos, NvB, hNvB⟩
  rcases hbounded v' with ⟨Bv', hBv'_pos, Nv'B, hNv'B⟩
  let B : PRCRat := Bu + Bu' + Bv + Bv' + 1
  have hB_pos : PRCRat.positive B := by
    rw [PRCRat.positive_iff_toRat_pos]
    have hBu : (0 : ℚ) < Bu.toRat := (PRCRat.positive_iff_toRat_pos Bu).mp hBu_pos
    have hBu' : (0 : ℚ) < Bu'.toRat := (PRCRat.positive_iff_toRat_pos Bu').mp hBu'_pos
    have hBv : (0 : ℚ) < Bv.toRat := (PRCRat.positive_iff_toRat_pos Bv).mp hBv_pos
    have hBv' : (0 : ℚ) < Bv'.toRat := (PRCRat.positive_iff_toRat_pos Bv').mp hBv'_pos
    simp [B]
    nlinarith
  have hBu_le_B : Bu.toRat ≤ B.toRat := by
    have hBu' : (0 : ℚ) < Bu'.toRat := (PRCRat.positive_iff_toRat_pos Bu').mp hBu'_pos
    have hBv : (0 : ℚ) < Bv.toRat := (PRCRat.positive_iff_toRat_pos Bv).mp hBv_pos
    have hBv' : (0 : ℚ) < Bv'.toRat := (PRCRat.positive_iff_toRat_pos Bv').mp hBv'_pos
    simp [B]
    nlinarith
  have hBu'_le_B : Bu'.toRat ≤ B.toRat := by
    have hBu : (0 : ℚ) < Bu.toRat := (PRCRat.positive_iff_toRat_pos Bu).mp hBu_pos
    have hBv : (0 : ℚ) < Bv.toRat := (PRCRat.positive_iff_toRat_pos Bv).mp hBv_pos
    have hBv' : (0 : ℚ) < Bv'.toRat := (PRCRat.positive_iff_toRat_pos Bv').mp hBv'_pos
    simp [B]
    nlinarith
  have hBv_le_B : Bv.toRat ≤ B.toRat := by
    have hBu : (0 : ℚ) < Bu.toRat := (PRCRat.positive_iff_toRat_pos Bu).mp hBu_pos
    have hBu' : (0 : ℚ) < Bu'.toRat := (PRCRat.positive_iff_toRat_pos Bu').mp hBu'_pos
    have hBv' : (0 : ℚ) < Bv'.toRat := (PRCRat.positive_iff_toRat_pos Bv').mp hBv'_pos
    simp [B]
    nlinarith
  have hBv'_le_B : Bv'.toRat ≤ B.toRat := by
    have hBu : (0 : ℚ) < Bu.toRat := (PRCRat.positive_iff_toRat_pos Bu).mp hBu_pos
    have hBu' : (0 : ℚ) < Bu'.toRat := (PRCRat.positive_iff_toRat_pos Bu').mp hBu'_pos
    have hBv : (0 : ℚ) < Bv.toRat := (PRCRat.positive_iff_toRat_pos Bv).mp hBv_pos
    simp [B]
    nlinarith
  rcases hmul_cont eps B heps hB_pos with ⟨delta, hdelta_pos, hdelta⟩
  rcases huu delta hdelta_pos with ⟨NuC, hNuC⟩
  rcases hvv delta hdelta_pos with ⟨NvC, hNvC⟩
  let N := max (max (max NuB Nu'B) (max NvB Nv'B)) (max NuC NvC)
  refine ⟨N, ?_⟩
  intro n hn
  have hNuB_n : NuB ≤ n := le_trans
    (le_trans (Nat.le_max_left NuB Nu'B) (Nat.le_max_left (max NuB Nu'B) (max NvB Nv'B)))
    (le_trans (Nat.le_max_left (max (max NuB Nu'B) (max NvB Nv'B)) (max NuC NvC)) hn)
  have hNu'B_n : Nu'B ≤ n := le_trans
    (le_trans (Nat.le_max_right NuB Nu'B) (Nat.le_max_left (max NuB Nu'B) (max NvB Nv'B)))
    (le_trans (Nat.le_max_left (max (max NuB Nu'B) (max NvB Nv'B)) (max NuC NvC)) hn)
  have hNvB_n : NvB ≤ n := le_trans
    (le_trans (Nat.le_max_left NvB Nv'B) (Nat.le_max_right (max NuB Nu'B) (max NvB Nv'B)))
    (le_trans (Nat.le_max_left (max (max NuB Nu'B) (max NvB Nv'B)) (max NuC NvC)) hn)
  have hNv'B_n : Nv'B ≤ n := le_trans
    (le_trans (Nat.le_max_right NvB Nv'B) (Nat.le_max_right (max NuB Nu'B) (max NvB Nv'B)))
    (le_trans (Nat.le_max_left (max (max NuB Nu'B) (max NvB Nv'B)) (max NuC NvC)) hn)
  have hNuC_n : NuC ≤ n :=
    le_trans (Nat.le_max_left NuC NvC)
      (le_trans (Nat.le_max_right (max (max NuB Nu'B) (max NvB Nv'B)) (max NuC NvC)) hn)
  have hNvC_n : NvC ≤ n :=
    le_trans (Nat.le_max_right NuC NvC)
      (le_trans (Nat.le_max_right (max (max NuB Nu'B) (max NvB Nv'B)) (max NuC NvC)) hn)
  exact hdelta (u.term n) (u'.term n) (v.term n) (v'.term n)
    (PRCRat.InBound_mono hBu_le_B (hNuB n hNuB_n))
    (PRCRat.InBound_mono hBu'_le_B (hNu'B n hNu'B_n))
    (PRCRat.InBound_mono hBv_le_B (hNvB n hNvB_n))
    (PRCRat.InBound_mono hBv'_le_B (hNv'B n hNv'B_n))
    (hNuC n hNuC_n)
    (hNvC n hNvC_n)

What this page does not claim

The declaration does not prove that every primitive Cauchy sequence is eventually bounded. The declaration does not define what a Cauchy sequence is in the primitive calculus. The declaration does not establish the product-continuity target.

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/RealMulBoundedContinuity.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