Blueprint (GPT formalization): a profinite presentation of the absolute Galois group of ℚ₂

 Blueprint (GPT formalization): a profinite presentation of the absolute Galois group of ℚ₂🔗

Compiled2026-07-15T18:23:56ZProject77c18e4Update gq2-claude to the cleaned formalization (02155b3 -> 91e1918)Leanleanprover/lean4:v4.28.0VersoBlueprintv4.28.0@84fb00913d07Mathlibv4.28.0@8f9d9cff6bd7

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 formalization's own dependency graph.

Contents

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