Foundation Primitive Recognition Calculus Real Boundedness Modulus Prccauchy Seq

The boundedness certificate

A Cauchy sequence is a list of numbers that eventually gets arbitrarily close to itself: past some point, any two entries are within any distance you name. In the Recognition Science framework, the notion of distance is replaced by a cost function J(x) = (x + 1/x)/2 - 1, which measures how hard it is to recognize one rational number as another. The declaration PRCCauchySeqEventuallyBoundedTarget_proved establishes that any sequence of rational numbers that is Cauchy with respect to this cost function is eventually bounded: there exists an interval, symmetric around zero, outside of which only finitely many entries of the sequence appear.

The proof works by selecting a fixed small threshold, the rational number 1/8, and showing that if the cost distance between two rational numbers is below this threshold, then their ordinary difference has square less than one. This is the content of the theorem PRCJCostDistance_sq_diff_lt_one_of_lt_boundedness_delta. From this, the proof derives that a cost-Cauchy sequence cannot escape to infinity: because its entries eventually lie within cost distance 1/8 of each other, their ordinary values are confined to a bounded interval. The result is recorded as a theorem in the machine-checked library of formal theorems, with the certificate structure PRCRealBoundednessModulusCertificate collecting the needed ingredients.

This boundedness result is a technical step in a larger construction: defining the real numbers as equivalence classes of cost-Cauchy sequences of rationals. The certificate also states that the remaining obstacle to defining multiplication on these reals is a separate condition, called bounded product-continuity, which is not proved here. The declaration does not claim that the real numbers are complete, that multiplication is defined, or that the cost function itself is the unique one satisfying the framework's axioms; those are separate results.

/-- A J-cost Cauchy ledger is eventually contained in a PRC symmetric rational
interval. -/
theorem PRCCauchySeqEventuallyBoundedTarget_proved :
    PRCCauchySeqEventuallyBoundedTarget := by
  intro u
  rcases u.cauchy PRCBoundednessDelta PRCBoundednessDelta_positive with
    ⟨N, hN⟩
  let anchor : PRCRat := u.term N
  let two : PRCRat := (1 : PRCRat) + (1 : PRCRat)
  let B : PRCRat := anchor * anchor + two
  have hB_pos : PRCRat.positive B := by
    rw [PRCRat.positive_iff_toRat_pos]
    have hsq : (0 : ℚ) ≤ anchor.toRat * anchor.toRat :=
      mul_self_nonneg anchor.toRat
    simp [B, two]
    nlinarith
  refine ⟨B, hB_pos, N, ?_⟩
  intro n hn
  have hdist : PRCRat.lt (PRCJCostDistance (u.term n) anchor) PRCBoundednessDelta := by
    simpa [anchor] using hN n N hn (Nat.le_refl N)
  have hsquare :
      ((u.term n).toRat - anchor.toRat) *
          ((u.term n).toRat - anchor.toRat) < 1 :=
    PRCJCostDistance_sq_diff_lt_one_of_lt_boundedness_delta hdist
  let x : ℚ := (u.term n).toRat
  let q : ℚ := anchor.toRat
  have hsquare_xq : (x - q) * (x - q) < 1 := by
    simpa [x, q] using hsquare
  have hdiff_lt_one : x - q < 1 := by
    nlinarith [mul_self_nonneg ((x - q) - 1)]
  have hdiff_gt_neg_one : -1 < x - q := by
    nlinarith [mul_self_nonneg ((x - q) + 1)]
  constructor
  · rw [PRCRat.lt_iff_toRat_lt]
    simp [B, two, anchor]
    nlinarith [mul_self_nonneg (2 * q + 1)]
  · rw [PRCRat.lt_iff_toRat_lt]
    simp [B, two, anchor]
    nlinarith [mul_self_nonneg (2 * q - 1)]

/-- Small PRC J-cost distance at the fixed threshold forces the ordinary
rational display increment to have square below one. -/
theorem PRCJCostDistance_sq_diff_lt_one_of_lt_boundedness_delta
    {a b : PRCRat}
    (hsmall : PRCRat.lt (PRCJCostDistance a b) PRCBoundednessDelta) :
    (a.toRat - b.toRat) * (a.toRat - b.toRat) < 1 := by
  rw [PRCRat.lt_iff_toRat_lt] at hsmall
  rw [PRCJCostDistance_toRat, PRCJCostDistanceRatDisplay_as_increment,
    PRCBoundednessDelta_toRat] at hsmall
  exact PRCJCostDistanceIncrementDisplay_sq_lt_one hsmall

/-- Step 10b closure certificate: eventual boundedness is proved, so the
remaining multiplication blocker is only bounded product-continuity. -/
structure PRCRealBoundednessModulusCertificate : Prop where
  boundedness_delta_positive : PRCRat.positive PRCBoundednessDelta
  distance_sq_bound :
    ∀ a b : PRCRat,
      PRCRat.lt (PRCJCostDistance a b) PRCBoundednessDelta →
        (a.toRat - b.toRat) * (a.toRat - b.toRat) < 1
  eventual_boundedness : PRCCauchySeqEventuallyBoundedTarget
  mul_closure_from_product_continuity :
    PRCJCostDistanceMulBoundedContinuityTarget → PRCRealMulClosureTarget
  mul_congruence_from_product_continuity :
    PRCJCostDistanceMulBoundedContinuityTarget → PRCRealMulCongruenceTarget

What this page does not claim

The real numbers are complete under the cost-based Cauchy condition. Multiplication on the cost-based reals is defined or closed. The cost function J is the unique function satisfying the framework's axioms.

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/RealBoundednessModulus.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: