Blueprint: a profinite presentation of the absolute Galois group of ℚ₂

 Blueprint: a profinite presentation of the absolute Galois group of ℚ₂🔗

Compiled2026-07-15T05:55:57ZProjectf2a4590Refresh arXiv preview PDF (75 pp) with rendered novelty, questions, bridgesLeanleanprover/lean4:v4.31.0-rc2VersoBlueprintv4.31.0@914d8a6bca61Mathlibec410d23dfa4e7540d4663405b5e0dc71f3c3363@ec410d23dfa4

This blueprint pairs every paper statement that has a formalized counterpart with its Lean declarations, generated from the paper source and the formalization crosswalk (paperforge ingest/blueprint_gen.py). Node status is computed from the Lean declarations directly; edges follow the paper's proofs and the axiom census.

Contents

  1. 1. Foundational inputs
  2. 2. Introduction and main theorem
  3. 3. The candidate as a profinite group
  4. 4. The tame and maximal pro-2 quotients
  5. 5. The common tamepro-2 boundary and the global induction
  6. 6. Linear lifting theory and duality
  7. 7. Quadratic determinant obstructions
  8. 8. A minimal non-scalar module layer in the wild kernel
  9. 9. Central covers, affine fibres, and Fourier inversion
  10. 10. Proof of the boundary-framed theorem
  11. 11. Passage to all finite quotients
  12. Dependency Graph
  13. Blueprint Summary