Interpreted quadratic arithmetic completion (Block 21).
On this page · Permalink · Source line 2313
Fix the continuous quotient
obtained by the action on a chosen square root \(i\) of \(-1\) in the algebraic closure. Its surjectivity and the equivalence
are proved using the existing actual quadratic Galois construction. For a commutative ring \(B\), define the arithmetic packet
where the maps are group homomorphisms. Unique descent through the actual surjective map \(q\) is derived, rather than supplied. Every member has finite image and is continuous for the coefficient topology, since its descent has the finite discrete domain \(C_2\).
Let \(R\) be any commutative ring and \(B\) any commutative \(R\)-algebra. The coordinate ring \(A_R=R[X]/(X^2-1)\) represents precisely this specified packet:
The first map evaluates the coordinate. Its inverse is the quotient universal property. A root is a unit with itself as inverse and determines a character by its value on the generator of \(C_2\). Finally pull back along \(q\). All inverse identities and naturality under coefficient homomorphisms are proved. In particular, the point reductions and actual arithmetic character reductions coincide. There is no invertibility-of-two, reducedness or nontriviality hypothesis on \(B\). No smoothness or étaleness statement at two is used or asserted.
Let \(I\subseteq R\) and suppose that \(R\) is \(I\)-adically complete. Using the checked ring-map reconstruction on the quadratic coordinate ring, Lean proves
The zero-precision quotient is included only for the formal indexing. The inverse constructs an actual arithmetic character, with exactly the prescribed reductions. It is unique, and its continuity is derived from its factorization through the same finite quotient.
There is also a completion theorem without chosen compatible characters. Suppose that \(R/I^m\) is finite for every \(m\ge1\), and that \(C_m\subseteq\mathcal P_q(R/I^m)\) are allowed subsets such that every reduction of an allowed member is allowed. Then
The root interpretation makes the allowed finite levels genuinely finite. Finite-branch compactness chooses the compatible roots, and the ring reconstruction gives their integral root. Naturality turns this into the required arithmetic character. Surjectivity of transitions and individual liftability of every finite node are not assumed. The root-level theorem needs only the allowed root subsets to be finite.
For \(R={\mathbf Z}_2\), Lean derives finiteness of all positive maximal-ideal quotients and applies this completion theorem. Since \({\mathbf Z}_2\) is a domain, its only roots of \(X^2-1\) are \(1\) and \(-1\). Thus the integral packet has exactly two distinct characters: the trivial character and the sign character describing the action on \(i\). They have the same reduction modulo two and distinct reductions modulo four.
The distinction between finite occupancy and continuation is witnessed by an actual finite arithmetic character. The roots modulo eight are \(1,3,5,7\). The root \(3\) defines a member of \(\mathcal P_q({\mathbf Z}/8{\mathbf Z})\), but no member of \(\mathcal P_q({\mathbf Z}/16{\mathbf Z})\) reduces to it. Indeed the only scalar lifts of \(3\) are \(3\) and \(11\), and both square to \(9\) modulo sixteen. The formal proof also classifies all roots modulo sixteen and the reductions with children. Consequently a nonempty finite node need not lie on an infinite branch, even in this explicitly interpreted arithmetic packet.
Block 21 completes this restricted arithmetic interpretation and its conditional completion. The packet is defined by one fixed quotient; it is not the collection of all quadratic characters of \(G_{{\mathbf Q}}\). No local ramification criterion, Hodge–Tate weight, Weil–Deligne attachment, or cross-coefficient local invariant was established by Block 21. The full manuscript still requires its remaining packet identifications and arithmetic comparisons. At the Block 21 checkpoint, the ledger recorded fifteen checked claims and five partial claims; see the Block 23 conditional-scope correction above. Universal positive occupancy remains conjectural.