prc_real_completeness_sharpened_certificate
plain-language theorem explainer
The sharpened real-completeness certificate for the primitive recognition calculus packages every intermediate target needed to realize Cauchy rational ledgers as points of the null-distance quotient and to extract diagonal completeness. Anyone assembling the recognition complete ordered field or the first-pass kernel cites this bundle. The proof is a pure structure inhabitant: each field is filled by a previously proved component target.
Claim. There is a sharpened completeness certificate for the primitive recognition real line: every raw rational Cauchy ledger realizes a point of the null-closed quotient; a cofinal unit-fraction tolerance schedule and a three-leg $J$-cost distance modulus exist; finite-row and representative tail selections produce a raw diagonal ledger and thence a diagonal selection; and that diagonal selection is exactly the sharpened completeness target for the null-closed recognition reals.
background
In the Primitive Recognition Calculus, candidate reals are raw rational Cauchy ledgers, then quotiented by a null-distance relation. Completeness is not an axiom; it is assembled from selection, schedule, and modulus targets that turn Cauchy data into diagonal representatives of the null-closed quotient.
The $J$-cost supplies the ledger metric. Upstream, the three-leg distance modulus is obtained by iterating the triangle modulus twice, so three small legs stay inside a prescribed $\varepsilon$. The cofinal tolerance schedule is the unit-fraction sequence, eventually below any positive threshold. Raw Cauchy realization is the identity packing of a Cauchy sequence into the ledger type; the quotient-point target then sends that ledger into the null-distance quotient.
Step 10e records the closed raw-ledger realization fact, the tail-selection diagonal chain, and the representative-completeness theorem for the null-closed recognition reals. Diagonal selection is definitionally the sharpened completeness target.
proof idea
Term-mode structure construction, not a new argument. Each field of the sharpened certificate is filled by a named proved target: raw Cauchy realization and quotient point; the two bridges (tail selection implies raw diagonal ledger; raw diagonal implies diagonal selection); the cofinal unit-fraction schedule and three-leg $J$-cost modulus; finite-row, finite-representative, and finite-diagonal schedule targets; the tail, raw-diagonal, and diagonal selection targets themselves; completeness-from-diagonal-selection (definitional identity); the proved completeness target; and the sharpened completeness target. No tactic reasoning beyond assembling those lemmas into one Prop structure.
why it matters
This is the Step 10e certificate in the PRC foundation stack. Downstream it feeds the promoted complete ordered-field certificate, which needs a complete carrier on the null-closed recognition reals (with rational embedding and additive closure), and it is listed among the ingredients of the kernel first-pass certificate (K7/A2). Without the bundle, completeness remains a scatter of separate targets rather than a single fact usable by ordered-field promotion.
In the Recognition Science layering this sits in Foundation under the continuum that later physics extraction assumes. It does not itself force $\varphi$, the eight-tick octave, or $D=3$; those live in the T0–T8 forcing chain. Its job is narrower: close the raw-ledger-to-diagonal path so the recognition real line is certificate-complete.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.