completion_R_delta_exists
plain-language theorem explainer
The PRC continuum completion R_δ exists as a conditionally structured complete ordered field on the null-distance quotient of Cauchy ledgers. Addition and negation are closed and congruent; multiplication, order, and completeness sit behind named exact targets. Anyone citing the continuum commitment (as opposed to RealLineNonNativity) uses this existence certificate. The proof is a one-line term applying the pre-built conditional certificate constructor.
Claim. There exists a conditional complete ordered field certificate for the PRC real completion $R_\delta$: its carrier is the null-distance quotient of Cauchy ledgers, addition and negation are closed and congruent on that carrier, and multiplication, order, and completeness are reduced to named exact targets. The continuum is not forced by distinction alone; once the completion commitment is made, the structure exists.
background
In the Primitive Recognition Calculus continuum layer, reals are not taken from Mathlib's classical Real. The carrier is the null-distance quotient of Cauchy ledgers (PRC-native Cauchy sequences of ledger data modulo vanishing defect distance). That quotient is the intended $R_\delta$.
The module's stance is explicit: distinction forcing does not produce a continuum (RealLineNonNativity). The continuum is a named commitment. Once that commitment is made, one must still exhibit a complete ordered field structure on the quotient, at least conditionally: some operations are fully proved closed and congruent; others are pinned to named exact targets rather than discharged inline.
Upstream cost and calibration material (J-cost on recognition events, multiplicative recognizer cost, rung-coarsen total cost, self-similar dressing) sits in the broader foundation stack. This declaration itself is only the existence certificate for the completed carrier with conditional field data, not yet the forced identification of cost with $J(x)=(x+x^{-1})/2-1$.
proof idea
One-line term proof: the theorem is definitionally the value of the constructor prc_real_complete_ordered_field_conditional_certificate. No tactics, no intermediate lemmas in the body. All substantive work (closure and congruence of addition and negation on the null-closed quotient, and the packaging of multiplication, order, and completeness as named exact targets) lives inside that certificate definition and its supporting modules (PRC cost-on-field, real complete ordered field scaffolding, native cost uniqueness, character rigidity forcing).
why it matters
This is the named continuum commitment in the PRC foundation: $R_\delta$ exists with conditional complete ordered field structure, even though the continuum is not forced by distinction. Sibling results in the same module then force the canonical cost on ratio orbits to the rational display $J(q)=(q+q^{-1})/2-1$, propagate one-point calibration to cyclic subgroups, and obtain forced $J$ on the completion. Those steps sit on the path toward T5 J-uniqueness in the forcing chain (the cost $J(x)=\cosh(\log x)-1$) once the continuum carrier is available.
No downstream consumers are recorded yet in the graph; the declaration is an existence anchor for the continuum layer rather than a lemma in a long used-by chain. It closes the "completion exists" half of the non-nativity story: RealLineNonNativity says the line is not forced; this certificate says that after the commitment, the structure is present and ready for cost forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.