equiv_symm
plain-language theorem explainer
Symmetry of working equality on regular δ-rational sequences: if s and t agree eventually within every tolerance 1/(k+1), then so do t and s. Anyone building the M0a real setoid cites this. The argument is a short rewrite: cross-difference flips sign, absolute value and denominator product are invariant.
Claim. Let $s,t$ be regular sequences of $\delta$-rationals. If for every $k\in\mathbb{N}$ there exists $N$ such that for all $n\ge N$ one has $|s_n-t_n|\le 1/(k+1)$ (expressed via integer cross-multiplication), then the same holds with $s$ and $t$ swapped.
background
This module builds a choice-free completion carrier for Recognition Science's primitive calculus: regular sequences of $\delta$-rationals (RatioOrbit points), with equality defined by eventual pointwise closeness rather than by displaying $\mathbb{Q}$.
A sequence $(a_n)$ is regular when $|a_m-a_n|\le 1/(m+1)+1/(n+1)$ for all $m,n$, written without rationals as $|\mathrm{crossDiff}(a_m,a_n)|\cdot(m+1)\cdot(n+1)\le(m+n+2),\mathrm{den}(a_m),\mathrm{den}(a_n)$. Here $\mathrm{crossDiff}(a,b)=a.\mathrm{num},b.\mathrm{den}-b.\mathrm{num},a.\mathrm{den}$ is the integer numerator of $a-b$.
Working equality equiv says: for every tolerance $1/(k+1)$, eventually $|s_n-t_n|\le 1/(k+1)$ in the same cross-multiplication form. The sibling crossDiff_swap records that swapping arguments only negates the cross-difference.
proof idea
Fix tolerance index $k$. From $h:k$ obtain a witness $N$ for $s$ versus $t$. Reuse the same $N$ for $t$ versus $s$. For $n\ge N$, apply crossDiff_swap to get $\mathrm{crossDiff}(t_n,s_n)=-\mathrm{crossDiff}(s_n,t_n)$. Rewrite with Int.natAbs_neg (absolute value ignores the sign) and commute the denominator product Nat.mul_comm. The original bound from $h$ applies verbatim.
why it matters
Feeds directly into equiv_equivalence, which packages reflexivity, symmetry, and transitivity into a genuine Equivalence on regular sequences: "the completion of the M0a carrier into a genuine setoid, all choice-free." That setoid is the M0a real carrier (regular $\delta$-rational sequences modulo pointwise convergence to zero difference).
In the Recognition foundation stack this is scaffolding for arithmetic and analysis built from logic without classical choice or $\mathbb{Q}$ display, staying on {propext, Quot.sound}. It is not itself a forcing-chain (T0–T8) step, but it underwrites the constructive real layer those landmarks eventually sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.