PRCRealCompleteOrderedFieldTargets
plain-language theorem explainer
Packages the exact algebraic and analytic blockers needed to finish the internal real completion from Cauchy ledgers under null distance. Anyone assembling the first complete ordered field surface from the primitive recognition calculus cites this bundle. It is a Prop-valued structure collecting closure, congruence, order, and completeness targets; there is no proof body.
Claim. A proposition packing eight named targets on Cauchy ledgers: (i) pointwise sums of Cauchy ledgers remain Cauchy; (ii) addition respects null-distance equivalence; (iii) pointwise negation preserves the Cauchy property; (iv) negation respects null equivalence; (v)--(vi) the analogous multiplicative closure and congruence statements; (vii) the order relation descends to the null-distance quotient; (viii) every Cauchy sequence of Cauchy-ledger representatives admits a Cauchy-ledger representative limit.
background
This module builds an internal real completion inside the primitive recognition calculus. Carriers are Cauchy sequences of rational ledgers; two sequences are identified when their pointwise difference is null in the $J$-cost distance (null-equivalent). Raw pointwise addition, negation, and multiplication act on the underlying ledger sequences before quotienting.
Each field of the bundle is an exact blocker already named in-module. Additive and multiplicative closure demand that the raw operations send Cauchy pairs to Cauchy sequences. The congruence targets demand that those operations descend to the null-distance quotient. Completeness is the diagonal statement: every Cauchy sequence of Cauchy-ledger representatives has a Cauchy-ledger representative limit.
Multiplication targets are flagged as needing eventual boundedness of Cauchy ledgers. The local setting is the next real-completion phase after the $J$-cost distance and triangle infrastructure imported from the sibling PRC $J$-cost module.
proof idea
Definitional Prop structure, not a proved theorem. The first four fields are the additive and negation closure and congruence propositions themselves. The remaining four fields are recorded as tautological equalities of the named multiplicative, order, and completeness target propositions to themselves, so the structure names those blockers without yet demanding inhabitants. No tactics or upstream lemmas are applied.
why it matters
This is the single targets argument consumed by the conditional first complete-ordered-field certificate in the same module. That certificate records a nonempty null-closed carrier and a rational embedding, then reduces algebra, order, and completeness to the named exact targets packaged here, with operation constructors gated on the corresponding blockers.
In the Recognition foundation stack, an internal complete ordered field is the analytic substrate on which later forcing-chain geometry (phi fixed point, eight-tick octave, $D=3$) and constant extractions sit. The bundle isolates what remains open before the real surface can be treated as closed rather than conditional: mul boundedness, order descent, and the diagonal completeness theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.