PRCRealCompletenessSharpenedCertificate
plain-language theorem explainer
Step 10e certificate bundling the sharpened completeness surface for the PRC null-closed reals: raw Cauchy packaging and quotient points, the tail-to-raw-diagonal-to-selection chain, cofinal tolerances, the three-leg J-cost modulus, finite schedules, and the representative-completeness theorem. Kernel and ordered-field promotion layers cite it as the closed analytic package. It is a Prop structure; the companion inhabitant theorem fills every field.
Claim. A proposition asserting all of the following for the PRC real construction: every raw rational Cauchy ledger packages as a Cauchy sequence and determines a point of the null-distance quotient; diagonal selection follows from a raw diagonal ledger, and a raw diagonal ledger follows from tail selection; a cofinal positive tolerance schedule exists; the three-leg $J$-cost distance modulus holds; finite row-tail, representative-tail, and diagonal schedules exist; tail selection, raw diagonal, and diagonal selection hold; diagonal selection implies completeness; and the completeness target for the null-closed PRC reals holds (with a trivial self-equality marker).
background
Primitive Recognition Calculus builds an internal real carrier as a null-distance quotient of rational Cauchy ledgers. Completeness is not imported from Mathlib; it is stated as a chain of named targets that isolate packaging, selection, and modulus work.
Raw realization says every raw rational Cauchy ledger packages as a PRCCauchySeq. The quotient-point target says every such ledger determines a point of the final null-closed quotient. Diagonal selection asks for an actual Cauchy-ledger limit of every representative-Cauchy sequence of ledgers. The sharper raw-diagonal target constructs the underlying rational ledger and proves both Cauchy and limit properties. Tail selection strengthens that by choosing, in each representative, a deep enough raw index so the diagonal is built from actual terms.
Supporting pieces include a cofinal positive tolerance schedule (tolerances eventually below any positive rational) and the three-leg $J$-cost distance modulus, which the diagonal argument uses when comparing selected diagonal points through an intermediate raw point across representatives. Finite-rung schedules sit below the global tail-selection theorem.
proof idea
No proof body: this is a bare structure ... : Prop whose fields are named completeness targets and a few implication arrows between them (raw diagonal implies diagonal selection; tail selection implies raw diagonal; diagonal selection implies completeness). The companion theorem prc_real_completeness_sharpened_certificate is the one-line-style inhabitant that assigns each field to a proved target or a previously established implication lemma (for example PRCRawCauchyRealizationTarget_proved and PRCRealDiagonalSelectionTarget_of_raw_diagonal_ledger).
why it matters
This is the Step 10e certificate for representative completeness of PRCRealNullClosed: it freezes the closed raw-ledger realization fact, the tail-selection diagonal, and the completeness theorem into one Prop surface. Downstream, prc_real_completeness_sharpened_certificate inhabits it; PRCRealCompleteOrderedFieldPromotedCertificate consumes the package when promoting the null quotient to the complete ordered-field layer (carrier, operations, congruences); and KernelFirstPassCertificate (K7/A2) treats the analytic stage objects as part of the first-pass PRC kernel bundle. In the broader Recognition stack this is foundation plumbing for an internal complete ordered field, not yet a forcing-chain (T0–T8) landmark, but it is the completeness hinge those later physics layers assume once the reals are internal.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.