IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealCompleteness
Packages every raw rational Cauchy ledger as a PRC Cauchy sequence, supplying the completeness scaffolding for the Primitive Recognition Calculus reals. Analysts reconstructing RS reals from ordered-field data cite it when lifting rational Cauchy data to completed points. The module defines realization and quotient targets, diagonal and tail selection, and unit-fraction tolerance schedules that make the packaging constructive.
claimEvery raw rational Cauchy ledger admits a packaging as a PRC Cauchy sequence. The module supplies realization and quotient-point targets, diagonal and tail selection on raw ledgers, and a unit-fraction cofinal tolerance schedule $1/n$ with the eventual bound $1/n < \varepsilon$ for positive rational $\varepsilon$.
background
Primitive Recognition Calculus builds the reals from recognition-native ordered-field data rather than assuming classical completeness. Upstream, RealOrderCongruence fixes the order and congruence structure on the rational ledger layer. A raw rational Cauchy ledger is a sequence of rationals with a Cauchy modulus expressed in that ledger language.
This module sits between that order layer and the completed field. It introduces unit fractions $1/n$ as the standard positive rational tolerance schedule, maps them to $\mathbb{Q}$, records positivity, and proves they are eventually smaller than any fixed positive rational bound. Diagonal and tail selection targets organize how one extracts convergent subdata from raw Cauchy ledgers.
The local goal is packaging: turn an arbitrary raw Cauchy ledger into a PRC Cauchy sequence object that later stages can quotient and complete.
proof idea
Definition-and-target module, not a single theorem. It declares realization and quotient-point targets for raw Cauchy ledgers, with companion _proved flags marking discharged instances. Unit fractions are defined, coerced to rationals, shown positive, and shown eventually below any positive rational tolerance. Diagonal, raw-diagonal-ledger, tail-selection, and cofinal-tolerance-schedule targets supply the classical completeness toolkit in PRC naming. Argument structure is constructive packaging plus schedule lemmas, not a deep analytic proof.
why it matters in Recognition Science
Feeds the PRC Kernel and the promoted real complete ordered field module. Without packaging raw rational Cauchy ledgers as PRC Cauchy sequences, the completeness step that upgrades the ordered field to a complete ordered field cannot start. Downstream RealCompleteOrderedFieldPromoted imports this layer to obtain the completed real structure used across Recognition Science foundation work. In the broader forcing chain this is infrastructure for continuum-level quantities (costs, ladders, constants) rather than a T0–T8 landmark itself, but it is required before those continuum objects are well-typed over completed reals.
scope and limits
- Does not construct the quotient field of reals or prove uniqueness of completions.
- Does not prove classical metric completeness of $\mathbb{R}$ outside the PRC ledger packaging.
- Does not discharge every named target; some remain interface or proved flags only.
- Does not address mass ladders, J-cost, or forcing steps T5–T8.
used by (2)
depends on (1)
declarations in this module (37)
-
def
PRCRawCauchyRealizationTarget -
theorem
PRCRawCauchyRealizationTarget_proved -
def
PRCRawCauchyQuotientPointTarget -
theorem
PRCRawCauchyQuotientPointTarget_proved -
def
PRCRealDiagonalSelectionTarget -
def
PRCRealRawDiagonalLedgerTarget -
def
PRCRealTailSelectionTarget -
def
PRCUnitFraction -
theorem
PRCUnitFraction_toRat -
theorem
PRCUnitFraction_positive -
def
PRCRealCofinalToleranceScheduleTarget -
theorem
PRCUnitFraction_eventually_lt -
theorem
PRCRealCofinalToleranceScheduleTarget_proved -
def
PRCJCostDistanceThreeLegModulusTarget -
theorem
PRCJCostDistanceThreeLegModulusTarget_proved -
def
PRCRowTailBound -
theorem
PRCRowTailBound_mono -
theorem
PRCRealFiniteRowTailBound_exists -
def
PRCRealFiniteRowTailSelectionTarget -
theorem
PRCRealFiniteRowTailSelectionTarget_proved -
def
PRCRepresentativeFiniteTailBound -
theorem
PRCRepresentativeFiniteTailBound_mono -
theorem
PRCRepresentativeFiniteTailBound_exists -
def
PRCRealFiniteRepresentativeTailSelectionTarget -
theorem
PRCRealFiniteRepresentativeTailSelectionTarget_proved -
def
PRCRealFiniteDiagonalScheduleTarget -
theorem
PRCRealFiniteDiagonalScheduleTarget_proved -
theorem
PRCRealTailSelectionTarget_proved -
theorem
PRCRealRawDiagonalLedgerTarget_of_tail_selection -
theorem
PRCRealRawDiagonalLedgerTarget_proved -
theorem
PRCRealDiagonalSelectionTarget_of_raw_diagonal_ledger -
theorem
PRCRealDiagonalSelectionTarget_proved -
theorem
PRCRealCompletenessTarget_of_diagonal_selection -
theorem
PRCRealCompletenessTarget_proved -
theorem
PRCRealCompletenessTarget_sharpened -
structure
PRCRealCompletenessSharpenedCertificate -
theorem
prc_real_completeness_sharpened_certificate