Encyclopedia Foundation Foundation Primitive Recognition Calculus Real Mul Bounded Continuity

ARTICLE 3 claims 2 theorems 1 model

Foundation Primitive Recognition Calculus Real Mul Bounded Continuity

A machine-checked library proves that multiplying real numbers on the recognition ledger works, provided the ledger entries eventually stay within a finite bound.

Verify this page

Bounded continuity and the real ledger

The real numbers are usually built from sequences of rationals that get closer together, called Cauchy sequences. Multiplying two such sequences pointwise produces another sequence, but only if the sequences do not grow without limit. This library states that condition precisely and proves the multiplication works under it.

In the Recognition Science framework, a ledger, a discrete record of events, tracks rational values. A raw rational ledger is a sequence of rationals. The library defines what it means for such a ledger to be eventually bounded: after some finite index, every entry lies strictly between a positive bound and its negative. A Cauchy ledger is one whose entries eventually cluster together; the library's first target states that every Cauchy ledger is eventually bounded.

The core target, called bounded product continuity, is a local analytic fact. It says that on any fixed symmetric interval, if two pairs of rationals are close enough in the cost distance, then their products are also close. The cost distance is the framework's measure of how far a recognition event is from perfect unity. This continuity is the ingredient needed to make multiplication of real ledgers well-defined.

The library then proves two conditional theorems. If every Cauchy ledger is eventually bounded, and if bounded product continuity holds, then the product of two real ledgers is again a real ledger, and the product respects the equivalence that defines real numbers. A final certificate packages these implications: the multiplication targets reduce exactly to eventual boundedness plus bounded product continuity.

In plain language, the library shows that the framework's real numbers can be multiplied consistently, provided the underlying ledgers do not run off to infinity. The proof is machine-checked, meaning a computer verified every step. This is a necessary step toward doing real analysis inside the recognition ledger, not a derivation of a physical constant.

MODEL PRCRawEventuallyBounded · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealMulBoundedContinuity.lean
PRCRawEventuallyBounded · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealMulBoundedContinuity.lean:22 
/-- Eventual PRC-native boundedness for a raw rational ledger. -/
def PRCRawEventuallyBounded (s : PRCRawRatLedger) : Prop :=
  ∃ B : PRCRat, PRCRat.positive B ∧
    ∃ N : Nat, ∀ n : Nat, N ≤ n →
      PRCRat.lt (-B) (s n) ∧ PRCRat.lt (s n) B
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 prc_real_mul_bounded_continuity_conditional_certificate · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealMulBoundedContinuity.lean
prc_real_mul_bounded_continuity_conditional_certificate · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealMulBoundedContinuity.lean:222 
theorem prc_real_mul_bounded_continuity_conditional_certificate :
    PRCRealMulBoundedContinuityConditionalCertificate where
  boundedness_target := rfl
  product_continuity_target := rfl
  mul_closure_from_targets := PRCRealMulClosureTarget_of_bounded_continuity
  mul_congruence_from_targets := PRCRealMulCongruenceTarget_of_bounded_continuity
  mul_operation_from_targets := by
    intro hbounded hcont
    exact ⟨PRCRealNullClosed.mulOf
      (PRCRealMulClosureTarget_of_bounded_continuity hbounded hcont)
      (PRCRealMulCongruenceTarget_of_bounded_continuity hbounded hcont)⟩

What this page does not claim

The library does not prove that every Cauchy ledger is eventually bounded; that remains a target. This library does not derive any physical constant or the fine-structure constant. The bounded product continuity statement is a target definition, not a proved theorem in this file.

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