prc_real_complete_ordered_field_promoted_certificate
plain-language theorem explainer
The PRC null-closed real carrier (Cauchy ledgers modulo null distance) carries closed addition, negation, and multiplication, order congruence, and representative completeness, packaged as the promoted Step 10 complete ordered-field certificate. Foundation work cites it before any Mathlib typeclass pass. The proof is a term-mode structure fill: each field is a previously proved target or certificate, with multiplication routed through eventual boundedness plus J-cost product continuity.
Claim. The PRC null-closed real carrier admits a promoted complete ordered-field certificate: the carrier is nonempty; rationals embed into it; addition, negation, and multiplication exist as closed, congruence-invariant operations on the quotient; order is congruence-invariant; representatives are complete; and the first-pass ordered-field, product-continuity, order-congruence, and sharpened completeness certificates all hold (full Mathlib typeclass instances deferred).
background
Primitive Recognition Calculus builds reals internally from Cauchy ledgers of rational intervals, not from Mathlib's ℝ. The final carrier PRCRealNullClosed is the quotient of those ledgers by null distance (the transitive null-distance target already closed). Rationals embed as constant protocols via ofRat.
The local module promotes Step 10 of the PRC foundation stack: the null quotient must support the closed field operations and theorem surfaces required by the complete ordered-field layer. The certificate structure records nonempty carrier and rational embedding, add/neg/mul closure and congruence targets, the induced binary/unary operations on the quotient, order congruence, representative completeness, plus four subordinate certificates (first-pass, product continuity, order congruence, sharpened completeness).
Upstream, eventual boundedness of J-cost Cauchy ledgers and J-cost product continuity supply the multiplication half; add/neg closure and congruence, order congruence, and the sharpened completeness certificate are already proved in sibling modules.
proof idea
Term-mode inhabitant of the certificate structure. Carrier is witnessed by the image of rational zero under the null-closed ofRat embedding; rational embedding is that same map. Addition and negation fields are the already-proved closure and congruence targets, with operations built by the null-closed addOf / negOf constructors from those targets.
Multiplication is the only composite step: closure and congruence are obtained from the bounded-continuity lemmas applied to the proved eventual-boundedness target and the proved J-cost mul bounded-continuity target; the operation is then mulOf of those two. Order congruence and representative completeness are direct citations of their proved targets. The four named certificates (first-pass conditional, product continuity, order congruence, sharpened completeness) are plugged in as fields; strength_tag is rfl.
why it matters
This is the promoted Step 10 gate for the PRC real layer: without a closed complete ordered-field surface on the null quotient, later foundation certificates cannot treat PRC reals as a field. Downstream, prc_universal_foundation_conditional_certificate installs this object as its real_complete_ordered_field field, and the kernel first-pass path sits in the same universal-foundation bundle.
In the Recognition stack this is pure foundation plumbing (carrier arithmetic before physics constants). It does not yet force T5–T8 (J-uniqueness, φ, eight-tick octave, D=3); those live higher in the forcing chain. The doc-comment is explicit that full Mathlib typeclass instances remain a later packaging pass, so this certificate is the internal theorem surface, not the end of the real-number story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.