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

Blueprint Summary🔗

Overview
Total entries58completed: 54; deps incomplete: 2; sorries: 0; no proof: 0
Ready now2Entries whose next formalization step is currently unblocked.
Fully closed54Local code and prerequisite closure are both complete.
Actionable priorities1Entries ready now and already unlocking downstream work.
Current blockers2Missing external or incomplete Lean declarations.
Missing informal coverage26Entries with Lean code but missing an informal statement or proof block.
Ready next (1)
Current blockers (2)
Missing informal coverage (26)
Entry index (58)
Definitions2completed: 2; deps incomplete: 0; sorries: 0; no proof: 0
Lemmas33completed: 32; deps incomplete: 0; sorries: 0; no proof: 0
Theorems20completed: 18; deps incomplete: 1; sorries: 0; no proof: 0
Corollaries3completed: 2; deps incomplete: 1; sorries: 0; no proof: 0
Definition Index (2)
Theorem / Lemma / Corollary Index (56)
By parent groups (7)
Linear lifting theory and duality (14)
The candidate as a profinite group (3)
Quadratic determinant obstructions (8)
The common tamepro-2 boundary and the global induction (1)
A minimal non-scalar module layer in the wild kernel (4)
The tame and maximal pro-2 quotients (7)
Central covers, affine fibres, and Fourier inversion (16)
Dependency insights
Proof-used entries36Entries reused in proof-only dependencies.
Tracked parent groups7Grouped health rollups for parents with more than one child entry.
Most used in proofs (36)
Group health (7)
  • Central covers, affine fibres, and Fourier inversion«ch-Fourier»
    Grouped view over entries sharing the same parent.
    total: 17closed: 15local-only: 1ready: 1blocked: 0incomplete Lean: 1unlock score: 32
    Next: «lem-obstructionseparation» stage: proofdownstream unlocks: 2
  • A minimal non-scalar module layer in the wild kernel«ch-Block»
    Grouped view over entries sharing the same parent.
    total: 4closed: 3local-only: 0ready: 1blocked: 0incomplete Lean: 1unlock score: 7
    Next: no ready child currently unlocks downstream work.
  • Linear lifting theory and duality«ch-Deformation»
    Grouped view over entries sharing the same parent.
    total: 14closed: 14local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 120
    Next: no ready child currently unlocks downstream work.
  • The tame and maximal pro-2 quotients«ch-Quotients»
    Grouped view over entries sharing the same parent.
    total: 7closed: 7local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 10
    Next: no ready child currently unlocks downstream work.
  • Quadratic determinant obstructions«ch-Quadratic»
    Grouped view over entries sharing the same parent.
    total: 8closed: 7local-only: 1ready: 0blocked: 0incomplete Lean: 0unlock score: 9
    Next: no ready child currently unlocks downstream work.
  • The candidate as a profinite group«ch-Candidate»
    Grouped view over entries sharing the same parent.
    total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 1
    Next: no ready child currently unlocks downstream work.
  • The common tamepro-2 boundary and the global induction«ch-Boundary»
    Grouped view over entries sharing the same parent.
    total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
    Next: no ready child currently unlocks downstream work.
Metadata
Metadata audit
Missing owner58
Missing effort58
Untagged58
Missing owner (58)
Missing effort (58)
Untagged (58)
Structure and coverage
Ready to formalize2Entries whose next step is currently unblocked.
Formalized, ancestors open2Local Lean work is done, but prerequisite closure is still open.
Fully closed54Local code and ancestor closure are both complete.
Heaviest prerequisites (30)
No prerequisites (28)
No dependents (22)
Proof debt hotspots (2)
  • A minimal non-scalar module layer in the wild kernel«ch-Block»
    Grouped proof/code debt derived from the current incomplete-declaration snapshots.
    affected entries: 1incomplete decls: 0missing decls: 1total debt: 1
  • Central covers, affine fibres, and Fourier inversion«ch-Fourier»
    Grouped proof/code debt derived from the current incomplete-declaration snapshots.
    affected entries: 1incomplete decls: 0missing decls: 1total debt: 1