realCauchyClaim
plain-language theorem explainer
Audit record K1/R9 tagging the internal Cauchy real-ledger step as a trace-closure strength claim. Build-order trackers cite it when PRC introduces reals via Cauchy sequences and an internal null-distance quotient rather than a classical ℝ alias. The body is a pure structure literal: fixed label, StrengthTag.traceClosure, and a one-line statement string.
Claim. Record, as a strength claim with tag trace-closure, the Build-Order-8 assertion that PRC Cauchy ledgers and their first internal quotient are indexed by completed orbits (rather than by a classical real alias).
background
In the Primitive Recognition Calculus, rationals sit on a native ledger; continuum objects are not imported from classical $\mathbb{R}$. Instead one builds Cauchy sequences of PRC rationals, equips them with a $J$-cost distance, and quotients by the null-distance relation. Sibling definitions in this module introduce that distance (PRCJCostDistance), Cauchy sequences (PRCCauchySeq), constant embeddings, and the null-equivalence relation.
StrengthClaim is a small audit triple (label, strength tag, statement string) used to mark how far a construction has been internalized. The tag here is traceClosure: the carrier and its first quotient are required to live inside the trace-stable fragment of the ledger, not behind an external real type.
Upstream orbit and quotient machinery (object-level division on distinction naturals) supplies the completed orbit indexing named in the statement. The module sits after rational-field and trace-closure imports, so the claim is the bookkeeping step before the certificate structure is assembled.
proof idea
Definitional structure literal, not a proof. The three fields of StrengthClaim are filled directly: label string BuildOrder8_real_cauchy_internal_quotient, tag StrengthTag.traceClosure, and a fixed English statement that PRC Cauchy ledgers and their first internal quotient use completed orbit indexing. No lemmas are applied.
why it matters
Feeds PRCRealCauchyCertificate, the first-pass real Cauchy certificate whose doc-comment states that the carrier is internal and trace-closure tagged, with the final null-distance quotient left as an exact Lean target rather than hidden behind a classical real alias. That certificate packages nonempty Cauchy sequences, a constant rational embedding, vanishing of $J$-cost self-distance, and reflexivity of the null relation.
In the Recognition build order this is the K1/R9 audit gate for internal reals: continuum structure must arise from ledger Cauchy data under trace closure, consistent with the broader program of deriving continuum geometry from discrete recognition cost rather than assuming $\mathbb{R}$. It does not itself close the quotient; it records the obligation the certificate and later null-quotient work discharge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.