eta_seq
plain-language theorem explainer
The unit embedding of a delta-rational as a constant regular sequence evaluates pointwise to that same rational at every index. Anyone comparing constant sequences under the working equality of regular sequences cites this. The proof is pure definitional equality via rfl.
Claim. For every delta-rational $q$ (a ratio orbit: signed numerator over nonzero distinction denominator) and every natural number $n$, the $n$-th term of the constant regular sequence $\eta(q)$ equals $q$.
background
In the primitive recognition calculus, a RatioOrbit is a delta-rational: integer numerator over a nonzero orbit denominator. Regular sequences are sequences of such orbits whose consecutive cross-differences stay controlled (the regularity side-condition).
The unit map $\eta$ sends a single delta-rational $q$ to the constant sequence with value $q$ at every index, packaged as a RegularSeq. Working equality equiv on regular sequences says that pointwise cross-differences eventually fall below every positive rational tolerance $1/(k+1)$.
This lemma records the obvious evaluation fact for that constant sequence, which later rewrites need when comparing $\eta(q)$ and $\eta(r)$.
proof idea
One-line wrapper: rfl. By definition, $\eta(q)$ is the pair whose sequence component is fun _ => q, so evaluating at any $n$ is definitionally $q$.
why it matters
Feeds the two well-definedness and separation facts for the unit map in this module. Downstream, eta_respects_crossEq rewrites both sides of the constant sequences via this lemma to reduce equivalence of $\eta(q)$ and $\eta(r)$ to vanishing of the cross-difference of $q$ and $r$. The Archimedean converse crossEq_of_equiv_eta likewise substitutes the constant values at a fixed index to force cross-equality from equiv of the constant sequences (instantiate tolerance at the product of denominators).
Together those close that $\eta$ is a well-defined, injective unit from delta-rationals into the regular-sequence completion under equiv. This is foundation scaffolding for the recognition calculus cost and forcing chain, not yet a physics landmark (T5–T8), but it is the concrete embedding step those later layers sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.