PRCRealCompleteOrderedFieldConditionalCertificate
plain-language theorem explainer
Conditional certificate that the PRC real carrier (Cauchy ledgers modulo null distance) is nonempty and admits a rational embedding, while algebra, order, and completeness are reduced to named exact closure and congruence targets. Continuum and kernel first-pass results cite it as the Step-10 surface. Definitional Prop packaging: no proof body; the companion constructor fills the fields.
Claim. There is a nonempty carrier of null-closed PRC reals (Cauchy ledgers quotiented by null distance), a nonempty embedding of PRC rationals into that carrier, and a bundle of exact targets for additive, multiplicative, order, and completeness blockers. From proved additive (resp. negation, multiplicative) closure and congruence targets one obtains a nonempty binary (resp. unary, binary) operation on the carrier.
background
In Primitive Recognition Calculus, reals are built from Cauchy sequences of ledger values, then quotiented by null distance. The resulting carrier is the null-closed PRC real type: Cauchy ledgers identified when their pairwise J-cost distance is null. PRC rationals sit upstream as ratio-orbit quotient classes (nonzero-denominator orbits equated by cross-multiplication).
This module is Build Order step 10 for a complete ordered-field surface on that carrier. Exact blockers name the remaining obligations: pointwise sums, negations, and products of Cauchy ledgers remain Cauchy, and those operations respect null equivalence so they descend to the quotient. Order congruence and completeness appear as further named targets.
The local targets bundle packages those blockers as a single Prop. Some mul/order/completeness fields are still tautological placeholders equal to themselves, marking unfinished obligations rather than discharged proofs.
proof idea
Definitional Prop structure, not a theorem. It records nonempty carrier and rational embedding, holds the targets bundle, and exposes three implication fields: given the matching closure and congruence targets, one obtains a nonempty addition, negation, or multiplication map on the null-closed carrier. A strength-tag reflexivity marks the trace-closure stage. Instantiation is left to the companion constructor theorem in the same module.
why it matters
Parent use is the continuum commitment that the completion $R_\delta$ exists with conditional field structure: carrier is the null-distance quotient of Cauchy ledgers, with addition and negation closed and congruent, while multiplication, order, and completeness stay as named exact targets. That commitment stresses the continuum is not forced by distinction alone, but once admitted the completion exists.
Also consumed by the promoted Step-10 certificate (closed operations and theorem surfaces for the current ordered-field layer, Mathlib typeclasses deferred) and by the first-pass kernel certificate that bundles concrete Lean objects for each early PRC stage.
In the Recognition foundation this is the first-pass surface reducing quotient algebra to exact targets, a prerequisite for continuum cost and forced $J$ on the completion rather than a finished ordered-field instance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.