PRCRealNull
plain-language theorem explainer
Conditional real carrier for Primitive Recognition Calculus: Cauchy ledgers modulo null J-cost distance, parameterized by a transitivity proof. Anyone building the PRC continuum or embedding rationals into the null quotient cites this type. The body is a one-line Quot of the setoid assembled from that hypothesis.
Claim. Given a proof that null-distance equivalence on PRC Cauchy sequences is transitive, let $R_{\mathrm{null}}$ be the quotient type of those sequences by the induced setoid (reflexive, symmetric, and the supplied transitivity). This is the intended PRC real carrier once the analytic triangle modulus is available.
background
Primitive Recognition Calculus builds a real continuum from Cauchy ledgers of rational recognition data, then collapses pairs at null J-cost distance. Null equivalence means the J-cost distance between two Cauchy sequences vanishes in the limit; the open analytic step is triangle-style transitivity of that relation.
Upstream, PRCNullDistanceTransitiveTarget is exactly that blocker: for all Cauchy sequences $u,v,w$, null-equivalence of $u\sim v$ and $v\sim w$ implies $u\sim w$. Feeding such a proof into the setoid constructor yields a Setoid on Cauchy sequences with relation null-equivalence (reflexivity and symmetry already hold unconditionally).
The module sits in the Foundation layer that bridges discrete recognition ledgers to a continuum carrier, conditional on Build Order step 9 analytic closure.
proof idea
One-line definitional wrapper. Apply the setoid constructor to the transitivity hypothesis, then take Lean's Quot of that setoid. No further algebra: the type is literally the quotient of PRC Cauchy sequences by null-distance equivalence once transitivity is assumed.
why it matters
This is the intended final PRC real type once the J-cost triangle modulus is proved. Downstream, the closed carrier is obtained by instantiating with a proved transitivity target, and rationals embed as constant Cauchy sequences in the quotient. The conditional certificate for Build Order step 9 records that triangle-modulus implies transitivity, which implies the setoid, which implies this quotient: no further quotient mechanics remain.
In the Recognition framework this supplies the continuum stage after discrete ledger structure, feeding later continuum-bridge and cost-distance geometry. It does not itself force $\varphi$, eight-tick structure, or $D=3$; those live in the T0–T8 forcing chain. The open hinge it exposes is the analytic triangle modulus for J-cost distance on Cauchy sequences.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.