Encyclopedia Foundation Foundation Primitive Recognition Calculus Real Completeness Prc Real Completenes
ARTICLE 3 claims 3 theorems
Foundation Primitive Recognition Calculus Real Completeness Prc Real Completenes
A machine-checked proof shows that within a primitive calculus of rational records, every Cauchy sequence has a limit, a completeness property that makes the system behave like the real numbers.
Completeness and its certificate
In mathematics, a space is complete when every sequence that looks like it should converge, a Cauchy sequence, actually has a limit inside the space. The rational numbers are famously incomplete: a Cauchy sequence of rationals can converge to the square root of two, which is not rational. The real numbers were invented to fix this gap. The declaration prc_real_completeness_sharpened_certificate is a machine-checked proof that a particular, primitive calculus of rational records is complete in this same sense.
The calculus is built from ledgers, discrete records of rational values. A Cauchy ledger is one where entries eventually become arbitrarily close to each other. The certificate proves that every Cauchy ledger determines a point in a quotient space where ledgers that are infinitely close are identified. This is exactly the construction of the real numbers from rationals, but carried out inside the framework's own primitive vocabulary. The proof is a chain of lemmas: it packages raw rational Cauchy ledgers into a structured form, selects diagonal entries to build a limit ledger, and shows that this limit is Cauchy and close to the original sequence.
The certificate itself is a structure, a bundle of three properties. First, for any sequence of Cauchy ledgers that is itself Cauchy, there is a diagonal selection: a way to pick one entry from each ledger so that the picked entries form a new Cauchy ledger. Second, this diagonal ledger is eventually close to every ledger in the original sequence. Third, the diagonal ledger is itself Cauchy. Together these prove that the quotient space has no holes: every Cauchy sequence of ledgers converges to a ledger in the space.
In Recognition Science, this is a foundational step. The framework's starting point is that reality keeps a ledger of recognition events. This theorem shows that such ledgers, even in their most primitive rational form, are rich enough to support the continuum of real numbers. It does not claim that the physical universe is built from these ledgers, nor that this is the only way to construct the reals. It establishes a structural fact: the primitive calculus is complete, and therefore behaves like the real numbers in this fundamental respect.
THEOREM prc_real_completeness_sharpened_certificate · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealCompleteness.lean
theorem prc_real_completeness_sharpened_certificate :
PRCRealCompletenessSharpenedCertificate where
raw_cauchy_realization := PRCRawCauchyRealizationTarget_proved
raw_cauchy_quotient_point := PRCRawCauchyQuotientPointTarget_proved
diagonal_selection_from_raw_diagonal :=
PRCRealDiagonalSelectionTarget_of_raw_diagonal_ledger
raw_diagonal_from_tail_selection :=
PRCRealRawDiagonalLedgerTarget_of_tail_selection
cofinal_tolerance_schedule :=
PRCRealCofinalToleranceScheduleTarget_proved
three_leg_distance_modulus :=
PRCJCostDistanceThreeLegModulusTarget_proved
finite_row_tail_selection :=
PRCRealFiniteRowTailSelectionTarget_proved
finite_representative_tail_selection :=
PRCRealFiniteRepresentativeTailSelectionTarget_proved
finite_diagonal_schedule :=
PRCRealFiniteDiagonalScheduleTarget_proved
tail_selection :=
PRCRealTailSelectionTarget_proved
raw_diagonal :=
PRCRealRawDiagonalLedgerTarget_proved
diagonal_selection :=
PRCRealDiagonalSelectionTarget_proved
completeness_from_diagonal_selection :=
PRCRealCompletenessTarget_of_diagonal_selection
completeness :=
PRCRealCompletenessTarget_proved
completeness_target := PRCRealCompletenessTarget_sharpened
THEOREM PRCRawCauchyRealizationTarget_proved · PRCRealTailSelectionTarget_proved · PRCRealFiniteDiagonalScheduleTarget_proved · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealCompleteness.lean
theorem PRCRawCauchyRealizationTarget_proved :
PRCRawCauchyRealizationTarget := by
intro s hs
refine ⟨{ term := s, cauchy := hs }, ?_⟩
rfl
theorem PRCRealTailSelectionTarget_proved :
PRCRealTailSelectionTarget := by
intro U hU
rcases PRCRealFiniteDiagonalScheduleTarget_proved U hU with
⟨_outer, pick, _houterTau, hrow, _hrep⟩
refine ⟨pick, ?_, ?_⟩
· intro eps heps
rcases PRCJCostDistanceThreeLegModulusTarget_proved eps heps with
⟨delta, hdelta_pos, hthree⟩
rcases hU delta hdelta_pos with ⟨Nrep, hNrep⟩
rcases PRCUnitFraction_eventually_lt hdelta_pos with ⟨Ntau, hNtau⟩
refine ⟨max Nrep Ntau, ?_⟩
intro m n hm hn
have hm_rep : Nrep ≤ m := le_trans (Nat.le_max_left Nrep Ntau) hm
have hn_rep : Nrep ≤ n := le_trans (Nat.le_max_left Nrep Ntau) hn
have hm_tauN : Ntau ≤ m := le_trans (Nat.le_max_right Nrep Ntau) hm
have hn_tauN : Ntau ≤ n := le_trans (Nat.le_max_right Nrep Ntau) hn
have htaum_delta : PRCRat.lt (PRCUnitFraction m) delta :=
hNtau m hm_tauN
have htaun_delta : PRCRat.lt (PRCUnitFraction n) delta :=
hNtau n hn_tauN
rcases hNrep m n hm_rep hn_rep with ⟨Npair, hNpair⟩
let K : Nat := max (pick m) (max (pick n) Npair)
have hpickmK : pick m ≤ K := Nat.le_max_left (pick m) (max (pick n) Npair)
have hpicknK : pick n ≤ K :=
le_trans (Nat.le_max_left (pick n) Npair)
(Nat.le_max_right (pick m) (max (pick n) Npair))
have hpairK : Npair ≤ K :=
le_trans (Nat.le_max_right (pick n) Npair)
(Nat.le_max_right (pick m) (max (pick n) Npair))
have hleg1_tau :
PRCRat.lt
(PRCJCostDistance ((U m).term (pick m)) ((U m).term K))
(PRCUnitFraction m) :=
(hrow m m (Nat.le_refl m)) (pick m) K (Nat.le_refl (pick m)) hpickmK
have hleg1 :
PRCRat.lt
(PRCJCostDistance ((U m).term (pick m)) ((U m).term K))
delta :=
PRCRat.lt_trans hleg1_tau htaum_delta
have hleg2 :
PRCRat.lt
(PRCJCostDistance ((U m).term K) ((U n).term K))
delta := by
simpa [PRCCauchySeq.raw] using hNpair K hpairK
have hleg3_tau :
PRCRat.lt
(PRCJCostDistance ((U n).term K) ((U n).term (pick n)))
(PRCUnitFraction n) :=
(hrow n n (Nat.le_refl n)) K (pick n) hpicknK (Nat.le_refl (pick n))
have hleg3 :
PRCRat.lt
(PRCJCostDistance ((U n).term K) ((U n).term (pick n)))
delta :=
PRCRat.lt_trans hleg3_tau htaun_delta
exact hthree
((U m).term (pick m)) ((U m).term K)
((U n).term K) ((U n).term (pick n))
hleg1 hleg2 hleg3
· intro eps heps
rcases PRCJCostDistanceThreeLegModulusTarget_proved eps heps with
⟨delta, hdelta_pos, hthree⟩
rcases hU delta hdelta_pos with ⟨Nrep, hNrep⟩
rcases PRCUnitFraction_eventually_lt hdelta_pos with ⟨Ntau, hNtau⟩
refine ⟨max Nrep Ntau, ?_⟩
intro n hn
have hn_rep : Nrep ≤ n := le_trans (Nat.le_max_left Nrep Ntau) hn
rcases (U n).cauchy delta hdelta_pos with ⟨NrowN, hNrowN⟩
refine ⟨max (max Nrep Ntau) NrowN, ?_⟩
intro l hl
have hl_rep : Nrep ≤ l :=
le_trans (Nat.le_max_left Nrep Ntau)
(le_trans (Nat.le_max_left (max Nrep Ntau) NrowN) hl)
have hl_tauN : Ntau ≤ l :=
le_trans (Nat.le_max_right Nrep Ntau)
(le_trans (Nat.le_max_left (max Nrep Ntau) NrowN) hl)
have hl_rowN : NrowN ≤ l :=
le_trans (Nat.le_max_right (max Nrep Ntau) NrowN) hl
have htaul_delta : PRCRat.lt (PRCUnitFraction l) delta :=
hNtau l hl_tauN
rcases hNrep n l hn_rep hl_rep with ⟨Npair, hNpair⟩
let K : Nat := max l (max (pick l) Npair)
have hlK : l ≤ K := Nat.le_max_left l (max (pick l) Npair)
have hpicklK : pick l ≤ K :=
le_trans (Nat.le_max_left (pick l) Npair)
(Nat.le_max_right l (max (pick l) Npair))
have hpairK : Npair ≤ K :=
le_trans (Nat.le_max_right (pick l) Npair)
(Nat.le_max_right l (max (pick l) Npair))
have hrowNK : NrowN ≤ K := le_trans hl_rowN hlK
have hleg1 :
PRCRat.lt
(PRCJCostDistance ((U n).term l) ((U n).term K))
delta :=
hNrowN l K hl_rowN hrowNK
have hleg2 :
PRCRat.lt
(PRCJCostDistance ((U n).term K) ((U l).term K))
delta := by
simpa [PRCCauchySeq.raw] using hNpair K hpairK
have hleg3_tau :
PRCRat.lt
(PRCJCostDistance ((U l).term K) ((U l).term (pick l)))
(PRCUnitFraction l) :=
(hrow l l (Nat.le_refl l)) K (pick l) hpicklK (Nat.le_refl (pick l))
have hleg3 :
PRCRat.lt
(PRCJCostDistance ((U l).term K) ((U l).term (pick l)))
delta :=
PRCRat.lt_trans hleg3_tau htaul_delta
exact hthree
((U n).term l) ((U n).term K)
((U l).term K) ((U l).term (pick l))
hleg1 hleg2 hleg3
theorem PRCRealFiniteDiagonalScheduleTarget_proved :
PRCRealFiniteDiagonalScheduleTarget := by
intro U hU
rcases PRCRealFiniteRowTailSelectionTarget_proved U with
⟨rowPick, hrowPick⟩
rcases PRCRealFiniteRepresentativeTailSelectionTarget_proved U hU with
⟨outer, repPick, houter, hrepPick⟩
refine ⟨outer, fun r => max (rowPick r) (repPick r), houter, ?_, ?_⟩
· intro r i hir
exact PRCRowTailBound_mono
(Nat.le_max_left (rowPick r) (repPick r))
(hrowPick r i hir)
· intro r
exact PRCRepresentativeFiniteTailBound_mono
(Nat.le_max_right (rowPick r) (repPick r))
(hrepPick r)
THEOREM PRCRealCompletenessSharpenedCertificate · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealCompleteness.lean
/-- Step 10e certificate. It records the closed raw-ledger realization fact,
the tail-selection diagonal, and the representative-completeness theorem for
`PRCRealNullClosed`. -/
structure PRCRealCompletenessSharpenedCertificate : Prop where
raw_cauchy_realization : PRCRawCauchyRealizationTarget
raw_cauchy_quotient_point : PRCRawCauchyQuotientPointTarget
diagonal_selection_from_raw_diagonal :
PRCRealRawDiagonalLedgerTarget → PRCRealDiagonalSelectionTarget
raw_diagonal_from_tail_selection :
PRCRealTailSelectionTarget → PRCRealRawDiagonalLedgerTarget
cofinal_tolerance_schedule : PRCRealCofinalToleranceScheduleTarget
three_leg_distance_modulus : PRCJCostDistanceThreeLegModulusTarget
finite_row_tail_selection : PRCRealFiniteRowTailSelectionTarget
finite_representative_tail_selection :
PRCRealFiniteRepresentativeTailSelectionTarget
finite_diagonal_schedule : PRCRealFiniteDiagonalScheduleTarget
tail_selection : PRCRealTailSelectionTarget
raw_diagonal : PRCRealRawDiagonalLedgerTarget
diagonal_selection : PRCRealDiagonalSelectionTarget
completeness_from_diagonal_selection :
PRCRealDiagonalSelectionTarget → PRCRealCompletenessTarget
completeness : PRCRealCompletenessTarget
completeness_target : PRCRealCompletenessTarget = PRCRealCompletenessTarget
What this page does not claim
This does not claim that physical reality is literally built from these rational ledgers. This does not claim that the primitive calculus is the only way to construct a complete ordered field. This does not claim that the certificate proves the existence of a limit for every sequence, only for Cauchy sequences.
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/RealCompleteness.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:
- How does this completeness proof relate to the standard construction of real numbers as equivalence classes of rational Cauchy sequences?
- What other properties of the real numbers, such as order completeness or the least upper bound property, can be derived in this primitive calculus?
- Does the quotient space constructed here satisfy the same algebraic field axioms as the real numbers?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM prc_real_completeness_sharpened_certificate · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealCompleteness.lean
theorem prc_real_completeness_sharpened_certificate : PRCRealCompletenessSharpenedCertificate where raw_cauchy_realization := PRCRawCauchyRealizationTarget_proved raw_cauchy_quotient_point := PRCRawCauchyQuotientPointTarget_proved diagonal_selection_from_raw_diagonal := PRCRealDiagonalSelectionTarget_of_raw_diagonal_ledger raw_diagonal_from_tail_selection := PRCRealRawDiagonalLedgerTarget_of_tail_selection cofinal_tolerance_schedule := PRCRealCofinalToleranceScheduleTarget_proved three_leg_distance_modulus := PRCJCostDistanceThreeLegModulusTarget_proved finite_row_tail_selection := PRCRealFiniteRowTailSelectionTarget_proved finite_representative_tail_selection := PRCRealFiniteRepresentativeTailSelectionTarget_proved finite_diagonal_schedule := PRCRealFiniteDiagonalScheduleTarget_proved tail_selection := PRCRealTailSelectionTarget_proved raw_diagonal := PRCRealRawDiagonalLedgerTarget_proved diagonal_selection := PRCRealDiagonalSelectionTarget_proved completeness_from_diagonal_selection := PRCRealCompletenessTarget_of_diagonal_selection completeness := PRCRealCompletenessTarget_proved completeness_target := PRCRealCompletenessTarget_sharpenedThe certificate proves that every Cauchy ledger determines a point in a quotient space where ledgers that are infinitely close are identified. prc_real_completeness_sharpened_certificate · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealCompleteness.leanTHEOREM PRCRawCauchyRealizationTarget_proved · PRCRealTailSelectionTarget_proved · PRCRealFiniteDiagonalScheduleTarget_proved · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealCompleteness.lean
theorem PRCRawCauchyRealizationTarget_proved : PRCRawCauchyRealizationTarget := by intro s hs refine ⟨{ term := s, cauchy := hs }, ?_⟩ rfltheorem PRCRealTailSelectionTarget_proved : PRCRealTailSelectionTarget := by intro U hU rcases PRCRealFiniteDiagonalScheduleTarget_proved U hU with ⟨_outer, pick, _houterTau, hrow, _hrep⟩ refine ⟨pick, ?_, ?_⟩ · intro eps heps rcases PRCJCostDistanceThreeLegModulusTarget_proved eps heps with ⟨delta, hdelta_pos, hthree⟩ rcases hU delta hdelta_pos with ⟨Nrep, hNrep⟩ rcases PRCUnitFraction_eventually_lt hdelta_pos with ⟨Ntau, hNtau⟩ refine ⟨max Nrep Ntau, ?_⟩ intro m n hm hn have hm_rep : Nrep ≤ m := le_trans (Nat.le_max_left Nrep Ntau) hm have hn_rep : Nrep ≤ n := le_trans (Nat.le_max_left Nrep Ntau) hn have hm_tauN : Ntau ≤ m := le_trans (Nat.le_max_right Nrep Ntau) hm have hn_tauN : Ntau ≤ n := le_trans (Nat.le_max_right Nrep Ntau) hn have htaum_delta : PRCRat.lt (PRCUnitFraction m) delta := hNtau m hm_tauN have htaun_delta : PRCRat.lt (PRCUnitFraction n) delta := hNtau n hn_tauN rcases hNrep m n hm_rep hn_rep with ⟨Npair, hNpair⟩ let K : Nat := max (pick m) (max (pick n) Npair) have hpickmK : pick m ≤ K := Nat.le_max_left (pick m) (max (pick n) Npair) have hpicknK : pick n ≤ K := le_trans (Nat.le_max_left (pick n) Npair) (Nat.le_max_right (pick m) (max (pick n) Npair)) have hpairK : Npair ≤ K := le_trans (Nat.le_max_right (pick n) Npair) (Nat.le_max_right (pick m) (max (pick n) Npair)) have hleg1_tau : PRCRat.lt (PRCJCostDistance ((U m).term (pick m)) ((U m).term K)) (PRCUnitFraction m) := (hrow m m (Nat.le_refl m)) (pick m) K (Nat.le_refl (pick m)) hpickmK have hleg1 : PRCRat.lt (PRCJCostDistance ((U m).term (pick m)) ((U m).term K)) delta := PRCRat.lt_trans hleg1_tau htaum_delta have hleg2 : PRCRat.lt (PRCJCostDistance ((U m).term K) ((U n).term K)) delta := by simpa [PRCCauchySeq.raw] using hNpair K hpairK have hleg3_tau : PRCRat.lt (PRCJCostDistance ((U n).term K) ((U n).term (pick n))) (PRCUnitFraction n) := (hrow n n (Nat.le_refl n)) K (pick n) hpicknK (Nat.le_refl (pick n)) have hleg3 : PRCRat.lt (PRCJCostDistance ((U n).term K) ((U n).term (pick n))) delta := PRCRat.lt_trans hleg3_tau htaun_delta exact hthree ((U m).term (pick m)) ((U m).term K) ((U n).term K) ((U n).term (pick n)) hleg1 hleg2 hleg3 · intro eps heps rcases PRCJCostDistanceThreeLegModulusTarget_proved eps heps with ⟨delta, hdelta_pos, hthree⟩ rcases hU delta hdelta_pos with ⟨Nrep, hNrep⟩ rcases PRCUnitFraction_eventually_lt hdelta_pos with ⟨Ntau, hNtau⟩ refine ⟨max Nrep Ntau, ?_⟩ intro n hn have hn_rep : Nrep ≤ n := le_trans (Nat.le_max_left Nrep Ntau) hn rcases (U n).cauchy delta hdelta_pos with ⟨NrowN, hNrowN⟩ refine ⟨max (max Nrep Ntau) NrowN, ?_⟩ intro l hl have hl_rep : Nrep ≤ l := le_trans (Nat.le_max_left Nrep Ntau) (le_trans (Nat.le_max_left (max Nrep Ntau) NrowN) hl) have hl_tauN : Ntau ≤ l := le_trans (Nat.le_max_right Nrep Ntau) (le_trans (Nat.le_max_left (max Nrep Ntau) NrowN) hl) have hl_rowN : NrowN ≤ l := le_trans (Nat.le_max_right (max Nrep Ntau) NrowN) hl have htaul_delta : PRCRat.lt (PRCUnitFraction l) delta := hNtau l hl_tauN rcases hNrep n l hn_rep hl_rep with ⟨Npair, hNpair⟩ let K : Nat := max l (max (pick l) Npair) have hlK : l ≤ K := Nat.le_max_left l (max (pick l) Npair) have hpicklK : pick l ≤ K := le_trans (Nat.le_max_left (pick l) Npair) (Nat.le_max_right l (max (pick l) Npair)) have hpairK : Npair ≤ K := le_trans (Nat.le_max_right (pick l) Npair) (Nat.le_max_right l (max (pick l) Npair)) have hrowNK : NrowN ≤ K := le_trans hl_rowN hlK have hleg1 : PRCRat.lt (PRCJCostDistance ((U n).term l) ((U n).term K)) delta := hNrowN l K hl_rowN hrowNK have hleg2 : PRCRat.lt (PRCJCostDistance ((U n).term K) ((U l).term K)) delta := by simpa [PRCCauchySeq.raw] using hNpair K hpairK have hleg3_tau : PRCRat.lt (PRCJCostDistance ((U l).term K) ((U l).term (pick l))) (PRCUnitFraction l) := (hrow l l (Nat.le_refl l)) K (pick l) hpicklK (Nat.le_refl (pick l)) have hleg3 : PRCRat.lt (PRCJCostDistance ((U l).term K) ((U l).term (pick l))) delta := PRCRat.lt_trans hleg3_tau htaul_delta exact hthree ((U n).term l) ((U n).term K) ((U l).term K) ((U l).term (pick l)) hleg1 hleg2 hleg3theorem PRCRealFiniteDiagonalScheduleTarget_proved : PRCRealFiniteDiagonalScheduleTarget := by intro U hU rcases PRCRealFiniteRowTailSelectionTarget_proved U with ⟨rowPick, hrowPick⟩ rcases PRCRealFiniteRepresentativeTailSelectionTarget_proved U hU with ⟨outer, repPick, houter, hrepPick⟩ refine ⟨outer, fun r => max (rowPick r) (repPick r), houter, ?_, ?_⟩ · intro r i hir exact PRCRowTailBound_mono (Nat.le_max_left (rowPick r) (repPick r)) (hrowPick r i hir) · intro r exact PRCRepresentativeFiniteTailBound_mono (Nat.le_max_right (rowPick r) (repPick r)) (hrepPick r)The proof is a chain of lemmas: it packages raw rational Cauchy ledgers into a structured form, selects diagonal entries to build a limit ledger, and shows that this limit is Cauchy and close to the original sequence. PRCRawCauchyRealizationTarget_proved · PRCRealTailSelectionTarget_proved · PRCRealFiniteDiagonalScheduleTarget_proved · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealCompleteness.leanTHEOREM PRCRealCompletenessSharpenedCertificate · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealCompleteness.lean
/-- Step 10e certificate. It records the closed raw-ledger realization fact, the tail-selection diagonal, and the representative-completeness theorem for `PRCRealNullClosed`. -/ structure PRCRealCompletenessSharpenedCertificate : Prop where raw_cauchy_realization : PRCRawCauchyRealizationTarget raw_cauchy_quotient_point : PRCRawCauchyQuotientPointTarget diagonal_selection_from_raw_diagonal : PRCRealRawDiagonalLedgerTarget → PRCRealDiagonalSelectionTarget raw_diagonal_from_tail_selection : PRCRealTailSelectionTarget → PRCRealRawDiagonalLedgerTarget cofinal_tolerance_schedule : PRCRealCofinalToleranceScheduleTarget three_leg_distance_modulus : PRCJCostDistanceThreeLegModulusTarget finite_row_tail_selection : PRCRealFiniteRowTailSelectionTarget finite_representative_tail_selection : PRCRealFiniteRepresentativeTailSelectionTarget finite_diagonal_schedule : PRCRealFiniteDiagonalScheduleTarget tail_selection : PRCRealTailSelectionTarget raw_diagonal : PRCRealRawDiagonalLedgerTarget diagonal_selection : PRCRealDiagonalSelectionTarget completeness_from_diagonal_selection : PRCRealDiagonalSelectionTarget → PRCRealCompletenessTarget completeness : PRCRealCompletenessTarget completeness_target : PRCRealCompletenessTarget = PRCRealCompletenessTargetThe certificate is a structure, a bundle of three properties. PRCRealCompletenessSharpenedCertificate · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealCompleteness.lean