real_cauchy_certificate
plain-language theorem explainer
Internal Cauchy sequences of rational ledgers and an internal quotient carrier for reals exist in the primitive recognition calculus, with the exact null-distance setoid target named. Build Order step 8 (first pass). Anyone assembling the PRC kernel or the real-completion layer cites this. The proof inhabits each certificate field by constant sequences, self-zero J-cost distance, and reflexivity/symmetry of null equivalence.
Claim. A first-pass real Cauchy certificate is inhabited: the type of Cauchy sequences of PRC rationals is nonempty; constant embeddings $\mathbb{Q}_{\mathrm{PRC}}\to$ Cauchy sequences exist; the $J$-cost distance from any rational to itself vanishes; null-equivalence of Cauchy sequences is reflexive and symmetric; a same-term setoid on those sequences is nonempty; and an internal quotient carrier with rational embedding is inhabited, with the exact null-distance setoid targets named by definitional equality.
background
In the Primitive Recognition Calculus, a Cauchy sequence is an orbit-indexed ledger of PRC rationals whose pairwise $J$-cost distance eventually falls below every positive rational tolerance. The $J$-cost distance is built from the square-gap of the recognition cost $J$ on the rational field; it is the metric seed for completing rationals internally rather than by classical reals.
Null-equivalence identifies two Cauchy ledgers when their $J$-cost distance tends to zero. The certificate structure packages existence of such sequences, a constant embedding of rationals, self-zero distance, reflexivity and symmetry of null-equivalence, a same-term setoid, and an internal quotient carrier, leaving the final null-distance quotient as an exact Lean target rather than a classical alias.
Upstream, constant rational ledgers are already proved Cauchy, self-distance vanishes by injectivity of the rational embedding of $J$, and ofRat embeds a rational as a constant Cauchy class in the quotient.
proof idea
Structure inhabitation, field by field. Nonemptiness of Cauchy sequences is witnessed by the constant-zero ledger. The constant embedding is the map sending each rational to its constant Cauchy sequence. Self-zero $J$-cost distance is the already-proved lemma on diagonal distance. Reflexivity of null-equivalence is the structure's refl; symmetry is a one-line intro then symm. The same-term setoid is supplied as a nonempty witness. The real quotient and rational embedding are witnessed by the zero class and the constant-class map ofRat. The three remaining targets (null-transitivity, null-setoid, strength tag) are discharged by rfl, pinning the exact named targets.
why it matters
This is Build Order step 8, first pass: it certifies that internal Cauchy ledgers and an internal quotient carrier exist before the kernel is closed. Downstream it feeds the first-pass kernel certificate (kernel_first_pass_certificate), which packages strength tags, trace syntax, judgment surface, and trace logic into a single inhabited kernel record.
In the Recognition framework this sits under Foundation, supplying the real-completion substrate on which later forcing and measurement layers rest. It does not yet invoke T5–T8 (J-uniqueness, $\varphi$, eight-tick, $D=3$); those enter after the carrier is in place. The certificate keeps the null-distance quotient as an exact target, so later closure steps can discharge transitivity and setoid laws without smuggling classical reals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.