equivSetoid
plain-language theorem explainer
Packages working equality of regular δ-rational sequences (pointwise difference to zero) as a setoid. Anyone forming the M0a constructive real line ℝδ_pre cites this carrier. One-line assembly: relation is equiv, equivalence proof is the already-established refl/symm/trans package.
Claim. The relation of eventual pointwise closeness on regular sequences of $\delta$-rationals is a setoid: $s \sim t$ means that for every tolerance $1/(k+1)$ there exists $N$ such that for all $n \ge N$, $|s_n - t_n| \le 1/(k+1)$ (via integer cross-multiplication), and this relation is reflexive, symmetric, and transitive.
background
M0a builds a choice-free constructive real line from δ-rationals already obtained from logic. A regular sequence is a map $n \mapsto a_n$ into ratio-orbits satisfying the Bishop-style modulus $|a_m - a_n| \le 1/(m+1) + 1/(n+1)$, written without ℚ display via integer cross-differences and denominators.
Working equality on two regular sequences is eventual pointwise closeness: for every $k$ there is $N$ so that past $N$ the cross-difference bound forces $|s_n - t_n| \le 1/(k+1)$. Upstream, that relation is proved an equivalence (refl, symm, trans), all choice-free.
The setoid is the packaging step that lets Quot form the carrier. The module aims at ℝδ_pre on the audit tier {propext, Quot.sound} only.
proof idea
Definitional one-liner. The setoid relation field is the existing predicate equiv (eventual cross-diff bound). The iseqv field is the theorem equiv_equivalence, which already bundles equiv_refl, equiv_symm, and equiv_trans. No new arithmetic is proved here.
why it matters
This is the setoid the M0a real carrier quotients by. Downstream, RealDelta is defined as Quot of this setoid, and mk sends a regular sequence to its class. Without the setoid package, the constructive line and the rational embedding eta cannot descend.
In the Recognition foundation stack this is pure carrier work: integers and rationals from logic, then regular sequences, then this equivalence, then the pre-real line. It does not yet touch the forcing chain (T5–T8), RCL, or physical constants; it supplies the analytic substrate those later layers sit on. Audit note: the quotient uses only propext and Quot.sound (FORCED tier).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.