IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealCompleteness

declarations in this module (37)

• def PRCRawCauchyRealizationTarget L25
• theorem PRCRawCauchyRealizationTarget_proved L30
• def PRCRawCauchyQuotientPointTarget L38
• theorem PRCRawCauchyQuotientPointTarget_proved L43
• def PRCRealDiagonalSelectionTarget L54
• def PRCRealRawDiagonalLedgerTarget L62
• def PRCRealTailSelectionTarget L74
• def PRCUnitFraction L86
• theorem PRCUnitFraction_toRat L99
• theorem PRCUnitFraction_positive L106
• def PRCRealCofinalToleranceScheduleTarget L113
• theorem PRCUnitFraction_eventually_lt L119
• theorem PRCRealCofinalToleranceScheduleTarget_proved L144
• def PRCJCostDistanceThreeLegModulusTarget L159
• theorem PRCJCostDistanceThreeLegModulusTarget_proved L168
• def PRCRowTailBound L197
• theorem PRCRowTailBound_mono L201
• theorem PRCRealFiniteRowTailBound_exists L207
• def PRCRealFiniteRowTailSelectionTarget L236
• theorem PRCRealFiniteRowTailSelectionTarget_proved L242
• def PRCRepresentativeFiniteTailBound L253
• theorem PRCRepresentativeFiniteTailBound_mono L259
• theorem PRCRepresentativeFiniteTailBound_exists L267
• def PRCRealFiniteRepresentativeTailSelectionTarget L323
• theorem PRCRealFiniteRepresentativeTailSelectionTarget_proved L333
• def PRCRealFiniteDiagonalScheduleTarget L347
• theorem PRCRealFiniteDiagonalScheduleTarget_proved L359
• theorem PRCRealTailSelectionTarget_proved L376
• theorem PRCRealRawDiagonalLedgerTarget_of_tail_selection L493
• theorem PRCRealRawDiagonalLedgerTarget_proved L500
• theorem PRCRealDiagonalSelectionTarget_of_raw_diagonal_ledger L507
• theorem PRCRealDiagonalSelectionTarget_proved L515
• theorem PRCRealCompletenessTarget_of_diagonal_selection L521
• theorem PRCRealCompletenessTarget_proved L526
• theorem PRCRealCompletenessTarget_sharpened L533
• structure PRCRealCompletenessSharpenedCertificate L539
• theorem prc_real_completeness_sharpened_certificate L560