Encyclopedia Foundation Foundation Primitive Recognition Calculus Real Mul Bounded Continuity Prcraw Eve

ARTICLE 2 claims 1 theorem 1 open

Foundation Primitive Recognition Calculus Real Mul Bounded Continuity Prcraw Eve

A Cauchy sequence of rational numbers eventually stays inside a finite interval; this property is what lets multiplication of real numbers be defined consistently.

Verify this page

Eventual boundedness

A sequence of rational numbers is eventually bounded if, after some finite point, every term lies strictly between two fixed rational bounds, one negative and one positive. The definition is a standard one: there exists a positive rational B and a natural number N such that for every n at least N, the term s n satisfies -B < s n < B. The Recognition Science library states this as a property of a raw rational ledger, its name for a sequence of rational numbers that records a process of recognition events.

This property matters because a Cauchy sequence, one whose terms get arbitrarily close to each other as the index grows, is not automatically bounded in the same way. Eventual boundedness is a separate condition that must be supplied or shown. The library defines a target statement, PRCCauchySeqEventuallyBoundedTarget, which asserts that every Cauchy sequence in its formal system is eventually bounded. This is not shown in the pack; it is stated as a target, a goal for later work.

The reason the target matters is multiplication. To define multiplication of real numbers as equivalence classes of Cauchy sequences, one must show that the product of two sequences is again Cauchy and that the result does not depend on which representative sequence is chosen. Both steps require a continuity condition on the cost-based distance function, and that continuity is only available on bounded windows. The library establishes two conditional theorems: if every Cauchy sequence is eventually bounded, and if the cost distance is continuous on bounded windows, then multiplication is closed and well-defined. A third theorem packages these into a single conditional certificate.

In Recognition Science, the eventual boundedness target is therefore a load-bearing premise. The library does not claim that every Cauchy sequence in its system is eventually bounded; that remains a stated target. It does not claim that the continuity condition holds unconditionally. What it does claim, as a theorem, is the conditional chain: eventual boundedness plus bounded continuity implies the multiplication of real numbers is properly defined.

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 pack does not prove that every Cauchy sequence is eventually bounded. The pack does not prove the bounded product-continuity condition. The pack does not show that multiplication is closed and well-defined unconditionally.

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