2 Residual partition and no crossing
On this page · Permalink · Source line 195
Theorem 2.1: Residual partition
For every coefficient algebra \(A\),
Read proof · Visual guide: Higher digits cannot change the root · Read statement and proof side by side · Permalink · Source line 197 · Claim record · Lean coverage · Code · Worked examples
Proof of Theorem 2.1
Every \(A\)-valued object has one reduced object \({\operatorname{red}}_A(x)\in\mathcal M(k)\), so the union is exhaustive. Two distinct fibers cannot intersect because an object cannot have two different reductions. Hence the union is disjoint.
Back to statement · Read statement and proof side by side · Permalink · Source line 209 · Claim record · Lean coverage · Code · Worked examples
Theorem 2.2: No crossing under positive-depth perturbation
Suppose \(x,y\in\mathcal M({\mathcal O})\) are related by a deformation operation that is congruent to the identity modulo \(\varpi\). Then
Every finite composition remains in one residual fiber. If an infinite perturbation stream converges in the \(\varpi\)-adic topology, its limit remains in the same fiber. The existence of that limit is an explicit hypothesis, not a consequence of positive depth alone.
Read proof · Visual guide: Higher digits cannot change the root · Read statement and proof side by side · Permalink · Source line 213 · Claim record · Lean coverage · Code · Worked examples
Proof of Theorem 2.2
A correction in \(\varpi{\mathcal O}\) vanishes after reduction modulo \(\varpi\). Thus one operation preserves the residual root, and induction proves the finite statement. For a convergent stream, convergence at the first finite precision makes its reduction eventually equal to that of its limit. Every term already has the initial reduction, so the limit has that reduction too. Completeness applies to Cauchy streams; it does not make every root-preserving stream Cauchy. For example, \(0,3,0,3,\ldots\) has constant reduction modulo \(3\) but no limit modulo \(9\).
Back to statement · Read statement and proof side by side · Permalink · Source line 221 · Claim record · Lean coverage · Code · Worked examples
Corollary 2.3: Zeroth-order obstruction
If two admissible objects have different residual roots, no sequence of genuinely positive-depth perturbations beginning at one can reach the other. A horizontal transport between their roots is a zeroth-order operation, not a deeper lift.
Visual guide: Higher digits cannot change the root · Permalink · Source line 225 · Claim record · Lean coverage · Code · Worked examples

Numerical certificate 2.4: Exact residual partition
The finite implementation partitions the integers \(0,\ldots,8\) into the three classes modulo \(3\):
Every tested correction of the form \(x\mapsto x+p h\) preserves the residual class exactly.
Permalink · Source line 235 · Claim record · Lean coverage · Code · Worked examples