prc_real_complete_ordered_field_conditional_certificate
plain-language theorem explainer
Conditional certificate that the PRC null-distance quotient of Cauchy ledgers carries complete-ordered-field structure once named closure and congruence targets hold. Continuum completion and kernel first-pass assembly cite it. The proof fills the certificate structure: proved add/neg targets, trivial mul/order/completeness reductions, and operations recovered from those targets.
Claim. There is a conditional complete-ordered-field certificate on the PRC real carrier (Cauchy ledgers modulo null distance): the carrier and the rational embedding are inhabited; algebra, order, and completeness reduce to named exact targets; and addition and negation operations are recoverable from their closure and congruence targets (with multiplication likewise recoverable when its targets hold).
background
Primitive Recognition Calculus builds a real line from Cauchy ledgers of PRC rationals, then quotients by null distance. The closed carrier PRCRealNullClosed is that quotient once null-distance transitivity is available; rationals embed as constant protocols via ofRat.
This module is Build Order step 10 (first pass). The surrounding structure PRCRealCompleteOrderedFieldConditionalCertificate records a nonempty carrier and rational embedding, a bundle of exact targets for field operations and completeness, and reconstruction maps that turn proved closure/congruence targets into actual operations on the quotient.
Upstream, addition is already closed on Cauchy ledgers and respects null equivalence (PRCRealAddClosureTarget_proved, PRCRealAddCongruenceTarget_proved); negation has matching proved targets. Multiplication, order, and completeness sit as named exact targets (here discharged by reflexivity on the target bundle).
proof idea
Tactic-mode structure inhabitant. Carrier is the constant-zero class PRCRealNullClosed.ofRat 0; rational embedding is the full ofRat map. The target bundle plugs in the proved add and neg closure/congruence theorems and uses rfl for mul closure/congruence, order congruence, and completeness.
The three operation reconstructors are short intros: given the corresponding closure and congruence hypotheses, return the nonempty operation packages addOf, negOf, and mulOf on the null-closed carrier. Strength tag is reflexivity.
why it matters
This is the named commitment that a continuum completion exists once distinction is granted, without claiming the continuum is forced by distinction alone. Downstream, completion_R_delta_exists is literally this certificate: carrier PRCRealNullClosed, addition and negation closed and congruent, with mul/order/completeness still on named targets.
It also feeds the promoted complete-ordered-field certificate and appears in the kernel first-pass assembly path. In the Recognition forcing chain this sits under foundation work that later supports J-cost on the completed ratio line (T5 J-uniqueness and the Recognition Composition Law live on that continuum surface). Open remainder: full discharge of mul, order, and completeness targets beyond the conditional packaging.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.