Encyclopedia Foundation Foundation Primitive Recognition Calculus Real Mul Bounded Continuity Prcrat

ARTICLE 4 claims 4 theorems

Foundation Primitive Recognition Calculus Real Mul Bounded Continuity Prcrat

Multiplying infinite sequences in a framework where recognition costs are forced needs a guarantee that the product stays finite; this page explains that guarantee.

Verify this page

The bounded product

In the Recognition Science framework, real numbers are built from infinite sequences of rational numbers that settle down, the way a decimal expansion settles. Multiplying two such sequences term by term is natural, but there is a catch: the product of two sequences that each stay within a finite bound also stays within a bound, and proving that requires a precise, machine-checked argument. The declaration PRCRat (a rational number in the framework's own arithmetic, with its own ordering and bounds) supplies the vocabulary for that argument, and the surrounding theorems show exactly what must be true for multiplication to work cleanly.

The central target is a statement about continuity. It says: if you have two rational numbers a and b, and you perturb each by a small amount (small in the framework's cost-based distance), then the product a times b changes by an amount that can be made as small as you like, provided all four numbers stay inside a fixed symmetric interval [-B, B]. This is the standard epsilon-delta definition of continuity, but applied to the framework's own notion of distance, which is derived from the forced cost function J. The theorem PRCRealMulClosureTarget_of_bounded_continuity then shows that, given two assumptions, the product of two Cauchy sequences (sequences that settle) is itself a Cauchy sequence. Those two assumptions are: first, that every Cauchy sequence is eventually bounded (stays within some finite bound after some point), and second, that the product-continuity statement above holds.

A second theorem, PRCRealMulCongruenceTarget_of_bounded_continuity, proves the analogous result for congruence: if two sequences are equivalent (they settle to the same real number), then their products with a third sequence are also equivalent. Together, these two theorems give the framework a well-defined multiplication on real numbers, conditional on the two assumptions. The certificate structure PRCRealMulBoundedContinuityConditionalCertificate packages all of this into a single object: it records the two targets as hypotheses and the two theorems as conclusions, and the final theorem prc_real_mul_bounded_continuity_conditional_certificate proves that the certificate holds, with the closure and congruence results following from the two assumptions.

What this does not claim is important. The certificate is conditional: it does not prove that every Cauchy sequence is eventually bounded, nor that the product-continuity statement holds. Those are left as targets, named PRCCauchySeqEventuallyBoundedTarget and PRCJCostDistanceMulBoundedContinuityTarget. The framework has not yet established these from its first principles; it has shown that if they hold, then multiplication on real numbers is well-defined. Nor does this page claim that the framework's real numbers are the same as classical real numbers; that comparison is a separate matter. The value here is architectural: it isolates exactly what is needed for multiplication to work, so that the remaining work is a clear, finite list of targets rather than an open-ended search.

THEOREM PRCRealMulClosureTarget_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)
THEOREM PRCRealMulCongruenceTarget_of_bounded_continuity · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealMulBoundedContinuity.lean
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)
THEOREM PRCRealMulBoundedContinuityConditionalCertificate · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealMulBoundedContinuity.lean
PRCRealMulBoundedContinuityConditionalCertificate · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealMulBoundedContinuity.lean:201 
/-- Conditional certificate: the multiplication targets reduce to eventual
boundedness plus bounded product continuity. -/
structure PRCRealMulBoundedContinuityConditionalCertificate : Prop where
  boundedness_target :
    PRCCauchySeqEventuallyBoundedTarget = PRCCauchySeqEventuallyBoundedTarget
  product_continuity_target :
    PRCJCostDistanceMulBoundedContinuityTarget =
      PRCJCostDistanceMulBoundedContinuityTarget
  mul_closure_from_targets :
    PRCCauchySeqEventuallyBoundedTarget →
      PRCJCostDistanceMulBoundedContinuityTarget →
        PRCRealMulClosureTarget
  mul_congruence_from_targets :
    PRCCauchySeqEventuallyBoundedTarget →
      PRCJCostDistanceMulBoundedContinuityTarget →
        PRCRealMulCongruenceTarget
  mul_operation_from_targets :
    PRCCauchySeqEventuallyBoundedTarget →
      PRCJCostDistanceMulBoundedContinuityTarget →
        Nonempty (PRCRealNullClosed → PRCRealNullClosed → PRCRealNullClosed)
THEOREM 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

What this page does not claim

The certificate does not prove eventual boundedness or product-continuity; those remain open targets. The framework's real numbers are not claimed to be identical to classical real numbers here. The page does not claim that multiplication is defined unconditionally; it is conditional on the two stated assumptions.

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