PRCReal
plain-language theorem explainer
First internal real carrier for Primitive Recognition Calculus: Cauchy sequences of PRC rationals, quotiented by termwise equality. Not Lean ℝ; the intended null-distance quotient remains an open target. Downstream certificate and rational-embedding code cite it. Pure type definition via Quot of the same-term setoid.
Claim. The type of PRC reals is the quotient of Cauchy sequences of PRC rationals by the equivalence relation of termwise identity (a provisional setoid strictly finer than the intended null-distance relation).
background
Primitive Recognition Calculus builds continuum structure from ledger data rather than importing classical reals. A PRC Cauchy sequence is a sequence of PRC rationals with a Cauchy modulus relative to the J-cost distance on the rational field. Constant sequences are Cauchy by a trivial modulus.
The same-term setoid equates two Cauchy sequences when they agree at every index. Its doc states it is "intentionally stronger than the final null-distance setoid" and is available without the null-distance triangle lemma. The exact target for the intended real setoid is the proposition that null-equivalence (vanishing J-cost distance of the difference) is an equivalence; reflexivity and symmetry are already proved, transitivity is the live obligation.
This module sits after the rational field and trace-closure layers and supplies the first internal continuum carrier for Order step 8.
proof idea
One-line type definition: the carrier is Quot of the same-term setoid on PRC Cauchy sequences. No proof obligations; the setoid's equivalence proof is already packaged in the sibling setoid definition.
why it matters
Gives the first named internal real type so later material need not alias Lean ℝ. The rational embedding maps a PRC rational to the class of its constant Cauchy ledger. The first-pass real Cauchy certificate records that Cauchy sequences and a constant embedding exist, with the null-distance setoid left as an exact Lean target rather than hidden behind a classical real. The certificate theorem (Order step 8, first pass) witnesses nonempty Cauchy sequences via the zero constant sequence and names the open null-distance target. Framework role: continuum bridge scaffolding inside Foundation, prior to forcing-chain landmarks that assume a completed real line.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.