eta_regular
plain-language theorem explainer
The constant sequence at a fixed ratio orbit is regular: the cross-difference of an orbit with itself vanishes, so the regularity bound holds for every index pair. Cited by anyone building the unit map from delta-rationals into regular sequences. Proof rewrites via the self-cross-difference identity, then finishes with nonnegativity of naturals.
Claim. For every ratio orbit $q$ and all $m,n\in\mathbb{N}$, $|\Delta(q,q)|\,(m+1)(n+1)\le(m+n+2)\,d(q)^2$, where $\Delta$ is the integer cross-difference of two ratio orbits and $d(q)$ is the natural-number reading of the denominator of $q$. The bound holds because $\Delta(q,q)=0$.
background
In the primitive recognition calculus grow layer, ratio orbits package rational numerator/denominator data used as values of sequences. A regular sequence is a sequence of ratio orbits whose pairwise cross-differences obey a controlled growth bound: the absolute cross-difference times $(m+1)(n+1)$ is at most $(m+n+2)$ times a product of denominators. That inequality is the well-formedness condition packaged in the RegularSeq carrier.
The cross-difference of any orbit against itself is identically zero (the sibling identity crossDiff_self). The unit map that embeds a single ratio orbit as the constant sequence valued at that orbit therefore reduces regularity to the zero case of the bound. The surrounding module (EtaCompletionM0a) builds that unit map and the equivalence apparatus on regular sequences from discrete ratio data.
Upstream arithmetic infrastructure supplies the natural-number reading of denominators and basic order facts (zero_le, multiplication by zero) used when the rewritten goal is a trivial nonnegativity claim.
proof idea
Short term-mode proof. Rewrite the cross-difference of $q$ with itself to zero via crossDiff_self; absolute value of zero is zero; two multiplications by $(m+1)$ and $(n+1)$ keep the left-hand side at zero. The goal is then $0\le(m+n+2),d(q)^2$, discharged by Nat.zero_le.
why it matters
This is the proof obligation inside the definition of the unit map eta, which sends a ratio orbit to the constant regular sequence $\langle q,q,q,\ldots\rangle$. Downstream, eta is the canonical embedding of delta-rationals into RegularSeq, the carrier for sequence equivalence and completion in the grow layer of the primitive recognition calculus.
Without the bound, the constant sequence would not inhabit RegularSeq, and the unit of the eta/equiv apparatus would be unavailable. The lemma is small and purely algebraic, but it closes the well-formedness gap that lets discrete ratio data seed the regular-sequence side of the foundation stack. It does not itself touch the forcing chain (T0–T8) or the J-cost; it sits earlier, at the arithmetic scaffolding that those later landmarks presuppose.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.