PRCRealNullClosed
plain-language theorem explainer
The final PRC real number type: equivalence classes of Cauchy rational ledgers under null J-cost distance. Anyone building continuum structure, completeness, or the forced-J capstone cites this carrier. It is a one-line specialization of the conditional null-distance quotient by the proved transitivity of null distance.
Claim. Let $R_{\delta}$ be the type of Cauchy rational ledgers modulo the null-distance relation induced by the J-cost metric. Once null distance is known to be transitive, $R_{\delta}$ is well-defined as an ordinary quotient type; write $\mathbb{R}_{\mathrm{PRC}}$ for that closed carrier.
background
Primitive Recognition Calculus builds reals from rational Cauchy ledgers equipped with a J-cost distance. The cost $J$ is the unique reciprocal-symmetric solution of the Recognition Composition Law; null distance means two ledgers are identified when their J-distance vanishes.
Upstream, PRCRealNull is the conditional carrier: given a proof that null distance is transitive, it forms the quotient Quot by the induced setoid. The sibling theorem that null distance is transitive discharges that hypothesis via the triangle-modulus estimate for the rational increment display.
This module closes Build Order step 9c: once the increment triangle, verifier triangle, and modulus are proved, the real carrier no longer carries a free transitivity hypothesis.
proof idea
One-line definitional wrapper. Apply the conditional quotient constructor to the already-proved null-distance transitivity theorem (itself a one-line application of the triangle-modulus target). No new analytic work occurs here; the body is pure specialization of the setoid quotient.
why it matters
This is the concrete real line on which continuum PRC results land. Downstream, every raw rational Cauchy ledger is required to determine a point of this carrier; the sharpened completeness target and the complete-ordered-field certificate both quantify over it. The capstone theorem forced_J_on_completion states that on this completion the recognition laws force $J(x)=(x+1/x)/2-1$ (T5 J-uniqueness), unique up to reciprocal gauge. The rational embedding ofRat and the step-9c increment-triangle certificate package this carrier as the closed endpoint of the null-distance setoid chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.