eta
plain-language theorem explainer
The unit map sends a delta-rational to the constant regular sequence with that value at every index. Anyone building the Archimedean completion of ratio orbits (or proving that equivalent constants are cross-equal) cites it. The definition is a structure pair: constant sequence plus the already-proved regularity lemma for constants.
Claim. For each delta-rational $q$ (a ratio orbit), define $\eta(q)$ to be the constant sequence $n \mapsto q$. This sequence is regular: for all $m,n$, the integer cross-difference bound $|q-q|\cdot(m+1)(n+1)\le(m+n+2)\,\mathrm{den}(q)^2$ holds, so $\eta(q)$ is a regular sequence of delta-rationals.
background
This module grows an Archimedean completion of delta-rationals. A RatioOrbit is an integer numerator over a nonzero distinction-nat denominator (the native display of a rational, avoiding bare $\mathbb{Q}$). Differences are measured by integer crossDiff, so inequalities stay in $\mathbb{Z}$ and $\mathbb{N}$.
A regular sequence is a map $\mathbb{N}\to$ ratio orbits whose pairwise gaps shrink like Bishop regularity: $|a_m-a_n|\le 1/(m+1)+1/(n+1)$, rewritten as $|\mathrm{crossDiff}(a_m,a_n)|(m+1)(n+1)\le(m+n+2),\mathrm{den}(a_m),\mathrm{den}(a_n)$. Working equality of two regular sequences is pointwise convergence of the difference to zero at every tolerance $1/(k+1)$.
Upstream, eta_regular already shows the constant sequence at $q$ meets that bound (both sides collapse because crossDiff q q = 0). The pattern mirrors the constant Cauchy ledger in the real-Cauchy layer.
proof idea
Pure structure construction, not a tactic proof. The sequence field is fun _ => q. The regularity field is discharged by applying eta_regular q m n at each pair of indices. That lemma rewrites crossDiff q q to zero via crossDiff_self, then uses Nat.zero_le.
why it matters
Without a unit map there is no dense copy of the delta-rationals inside the regular-sequence completion. Downstream, equiv treats $\eta(q)$ and $\eta(r)$ as the constant test objects; crossEq_of_equiv_eta is the Archimedean recovery step: if $\eta(q)\sim\eta(r)$ then $q$ and $r$ are cross-equal (instantiate tolerance at $k=\mathrm{den}(q),\mathrm{den}(r)$ and force the cross-difference to vanish). Equivalence machinery (equiv_refl, equiv_symm, equiv_trans, equiv_equivalence) is stated on all regular sequences and specializes cleanly on the image of $\eta$.
In the Primitive Recognition Calculus this is the first embedding step toward a choice-free real line on which cost, forcing, and later continuum statements can sit. It is scaffolding for the completion, not a physics law by itself; landmarks such as T5–T8 or the RCL are not invoked here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.