Foundation Primitive Recognition Calculus Real Boundedness Modulus Prc Real Boun

The boundedness certificate

In mathematics, a Cauchy sequence is a sequence where terms get arbitrarily close to each other as the sequence progresses. A fundamental fact about real numbers is that every Cauchy sequence of rational numbers converges to a real number. Before that convergence can be established, one must first show that such a sequence is bounded: that all its terms eventually lie within some fixed interval. This boundedness is a necessary stepping stone in the standard construction of the real numbers from rationals.

The declaration prc_real_boundedness_modulus_certificate is a formal certificate inside the Recognition Science framework's machine-checked library of formal theorems. It packages together four facts. First, it states that a specific rational threshold, one eighth, is positive. Second, it proves that if the framework's cost distance between two rational numbers is smaller than this threshold, then the square of their ordinary difference is less than one. Third, it records that a J-cost Cauchy sequence is eventually bounded within a symmetric rational interval. Fourth, it states that if a certain product-continuity condition holds, then multiplication on the resulting real numbers is both closed and well-defined.

The certificate itself is a single theorem that assembles these components. Its role is to close a specific gap in a larger construction: after proving eventual boundedness, the only remaining obstacle to defining real multiplication is a bounded product-continuity property. The certificate makes this remaining step explicit and isolated.

In Recognition Science, the framework models recognition events as discrete records in a ledger, and the cost of recognition is forced by a proved theorem. This certificate is part of the framework's internal development of real numbers from its primitive recognition calculus, not a claim about physical measurements. It establishes a technical precondition within that formal system.

What the certificate does not claim is equally important. It does not assert that the product-continuity condition actually holds; that remains a separate target. It does not construct the real numbers themselves, only a boundedness certificate that is one ingredient. And it makes no empirical or physical prediction. It is a formal, internal statement about the framework's own rational arithmetic and cost function.

theorem PRCBoundednessDelta_positive :
    PRCRat.positive PRCBoundednessDelta := by
  rw [PRCRat.positive_iff_toRat_pos, PRCBoundednessDelta_toRat]
  norm_num

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

/-- 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)]

/-- 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 certificate does not prove the product-continuity condition it references. The certificate does not construct the real numbers, only a boundedness precondition. The certificate makes no empirical or physical prediction.

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: