PRCRealCompleteOrderedFieldPromotedCertificate
plain-language theorem explainer
Bundles the promoted Step 10 certificate: the PRC null-distance quotient of Cauchy ledgers carries closed field operations, order congruence, and representative completeness. Universal-foundation and kernel first-pass certificates cite it as the real-analytic surface. It is a definitional Prop packing nonempty carriers, operation targets, and already-proved sub-certificates; Mathlib typeclass instances are deferred.
Claim. A certificate that the null-distance quotient of PRC Cauchy ledgers is nonempty, admits an embedding of the PRC rationals, and supports closed, congruence-respecting addition, negation, and multiplication; that order is well-defined on the quotient and every Cauchy sequence of representatives has a representative limit; and that the first-pass complete ordered-field certificate, product-continuity certificate, order-congruence certificate, and sharpened completeness certificate all hold (with a trivial strength-tag identity).
background
Primitive Recognition Calculus builds an internal real carrier before any Mathlib Real instance. Cauchy ledgers are sequences with a raw Cauchy predicate; the final carrier PRCRealNullClosed is that space quotiented by null distance (the transitive null-equivalence relation). PRC rationals are ratio-orbit quotient classes identified by cross-multiplication.
The complete ordered-field layer is staged as exact blockers: add/mul/neg closure (pointwise operations preserve Cauchy), congruence (null-equivalent inputs yield null-equivalent outputs), order congruence, and representative completeness (every Cauchy sequence of ledger representatives has a ledger limit). The sharpened completeness certificate records raw-ledger realization, diagonal selection, and the representative-completeness theorem on the closed null quotient.
This module promotes those blockers into a single Prop surface for the current foundation stack, without yet installing Mathlib ordered-field typeclasses.
proof idea
No proof body: this is a structure definition whose fields are Prop obligations. Downstream, the inhabitant prc_real_complete_ordered_field_promoted_certificate fills them by pointing at concrete witnesses (e.g. the zero rational embedding for nonempty carrier), the proved closure/congruence targets (PRCRealAddClosureTarget_proved, and analogs for negation and multiplication), and the packaged sub-certificates (first-pass conditional complete ordered field, product continuity, order congruence, sharpened completeness). The strength-tag field is a reflexive equality used as a trace-closure marker.
why it matters
Step 10 of the PRC foundation chain: it asserts that the internal null quotient is ready as a complete ordered-field surface for everything above it. PRCUniversalFoundationCertificate and PRCUniversalFoundationConditionalCertificate both require this field as real_complete_ordered_field, so the top-level universal-foundation close depends on it. KernelFirstPassCertificate sits in the same first-pass bundling path.
In Recognition Science terms this is pre-physics scaffolding: a native real line built from recognition ledgers and null distance, on which later cost, J-uniqueness, and forcing-chain arguments can sit without importing classical ℝ as an axiom. Full Mathlib packaging remains open; the certificate only guarantees the internal theorem surfaces.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.