PRCSameTermSetoid
plain-language theorem explainer
Packages pointwise equality of PRC Cauchy sequences as a Lean setoid on the space of those sequences. Anyone building the first internal real carrier (the Cauchy-ledger quotient) cites it. The proof is a one-line wrapper: the relation is PRCSameTerm and equivalence is the already-proved PRCSameTerm.equivalence.
Claim. The relation of pointwise term equality on PRC Cauchy sequences (sequences $u,v:\mathbb{N}\to\mathrm{PRCRat}$ that are Cauchy in $J$-cost distance) forms a setoid: $u\sim v$ iff $u_n=v_n$ for every $n$, and this relation is an equivalence.
background
Primitive Recognition Calculus builds reals internally from rational ledgers, not from Lean's ℝ. A PRC Cauchy sequence is an orbit-indexed map $\mathbb{N}\to\mathrm{PRCRat}$ whose $J$-cost distance eventually drops below every positive PRC rational tolerance. The $J$-cost distance is the recognition cost separating two ledger values.
The intended final identification of sequences is null $J$-cost distance (sequences that become arbitrarily close). That target setoid needs a triangle inequality for null-distance; its equivalence is still recorded as an open obligation (PRCNullDistanceSetoidTarget).
Meanwhile the development needs a working quotient carrier. Pointwise sequence identity is available immediately: two Cauchy ledgers are related when every term agrees. That relation is strictly stronger than null-distance, so the quotient is coarser than the eventual real line, but it is already an equivalence and needs no analytic lemma.
proof idea
One-line setoid construction. The underlying relation field is set to pointwise term equality (PRCSameTerm). The iseqv field is discharged by the existing theorem that pointwise equality is reflexive, symmetric, and transitive (PRCSameTerm.equivalence), proved by constructor on the three Equivalence fields with rfl and symm on the pointwise equalities.
why it matters
This is the first internal quotient carrier for PRC reals. Downstream, PRCReal is defined as the quotient of Cauchy sequences by this setoid, and ofRat embeds a rational as the class of the constant Cauchy ledger. The audit theorem real_cauchy_certificate (Order step 8, first pass) records that internal Cauchy ledgers and an internal quotient carrier exist, while naming the exact null-distance setoid as the remaining target.
In the Recognition foundation stack this sits under continuum construction from the ledger: reals arise as completed recognition orbits with $J$-cost Cauchy control, not as an imported analytic axiom. The definition is deliberately temporary scaffolding for the carrier type; the scientific identification of reals will switch to the null-distance setoid once its triangle/transitivity obligation closes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.