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

Blueprint Summary🔗

Overview
Total entries61completed: 31; deps incomplete: 19; sorries: 9; no proof: 0
Ready now11Entries whose next formalization step is currently unblocked.
Fully closed31Local code and prerequisite closure are both complete.
Actionable priorities10Entries ready now and already unlocking downstream work.
Current blockers12Missing external or incomplete Lean declarations.
Missing informal coverage28Entries with Lean code but missing an informal statement or proof block.
Ready next (10)
Current blockers (12)
Missing informal coverage (28)
Entry index (61)
Propositions22completed: 5; deps incomplete: 7; sorries: 9; no proof: 0
Lemmas36completed: 26; deps incomplete: 9; sorries: 0; no proof: 0
Theorems2completed: 0; deps incomplete: 2; sorries: 0; no proof: 0
Corollaries1completed: 0; deps incomplete: 1; sorries: 0; no proof: 0
Axiom-like entries9completed: 0; deps incomplete: 0; sorries: 9; no proof: 0
Theorem / Proposition / Lemma / Corollary Index (61)
By parent groups (9)
Linear lifting theory and duality (10)
Introduction and main theorem (2)
The candidate as a profinite group (2)
Quadratic determinant obstructions (13)
A minimal non-scalar module layer in the wild kernel (4)
Proof of the boundary-framed theorem (2)
The tame and maximal pro-2 quotients (9)
The foundational inputs of the formalization: statements assumed as Lean axioms, each resting on the literature, plus former axioms since discharged by proofs. (9)
Central covers, affine fibres, and Fourier inversion (8)
Axiom-like Index (9)
Dependency insights
Proof-used entries51Entries reused in proof-only dependencies.
Tracked parent groups9Grouped health rollups for parents with more than one child entry.
Most used in proofs (51)
Group health (9)
  • The foundational inputs of the formalization: statements assumed as Lean axioms, each resting on the literature, plus former axioms since discharged by proofs.foundations
    Grouped view over entries sharing the same parent.
    total: 9closed: 0local-only: 0ready: 9blocked: 0incomplete Lean: 9unlock score: 46
    Next: «ax-localReciprocity» stage: proofdownstream unlocks: 8
  • The tame and maximal pro-2 quotients«ch-Quotients»
    Grouped view over entries sharing the same parent.
    total: 9closed: 2local-only: 6ready: 1blocked: 0incomplete Lean: 1unlock score: 43
    Next: «lem-o2tame» stage: proofdownstream unlocks: 4
  • 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: 5
    Next: no ready child currently unlocks downstream work.
  • Linear lifting theory and duality«ch-Deformation»
    Grouped view over entries sharing the same parent.
    total: 10closed: 8local-only: 2ready: 0blocked: 0incomplete Lean: 0unlock score: 51
    Next: no ready child currently unlocks downstream work.
  • Quadratic determinant obstructions«ch-Quadratic»
    Grouped view over entries sharing the same parent.
    total: 13closed: 10local-only: 3ready: 0blocked: 0incomplete Lean: 0unlock score: 23
    Next: no ready child currently unlocks downstream work.
  • Central covers, affine fibres, and Fourier inversion«ch-Fourier»
    Grouped view over entries sharing the same parent.
    total: 8closed: 5local-only: 3ready: 0blocked: 0incomplete Lean: 0unlock score: 6
    Next: no ready child currently unlocks downstream work.
  • Proof of the boundary-framed theorem«ch-Induction»
    Grouped view over entries sharing the same parent.
    total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 5
    Next: no ready child currently unlocks downstream work.
  • Introduction and main theorem«ch-IntroductionAndMainTheorem»
    Grouped view over entries sharing the same parent.
    total: 2closed: 0local-only: 2ready: 0blocked: 0incomplete Lean: 0unlock score: 4
    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: 2closed: 1local-only: 1ready: 0blocked: 0incomplete Lean: 0unlock score: 2
    Next: no ready child currently unlocks downstream work.
Metadata
Tags in use1Distinct tags currently attached to blueprint entries.
Tag rollups (1)
  • tag: axiom
    entries: 9actionable: 9quick wins: 0linked PRs: 0
Metadata audit
Missing owner61
Missing effort61
Untagged52
Missing owner (61)
Missing effort (61)
Untagged (52)
Structure and coverage
Ready to formalize11Entries whose next step is currently unblocked.
Formalized, ancestors open19Local Lean work is done, but prerequisite closure is still open.
Fully closed31Local code and ancestor closure are both complete.
Heaviest prerequisites (33)
No prerequisites (28)
No dependents (10)
Proof debt hotspots (3)
  • The foundational inputs of the formalization: statements assumed as Lean axioms, each resting on the literature, plus former axioms since discharged by proofs.foundations
    Grouped proof/code debt derived from the current incomplete-declaration snapshots.
    affected entries: 9incomplete decls: 9missing decls: 0total debt: 9
  • The tame and maximal pro-2 quotients«ch-Quotients»
    Grouped proof/code debt derived from the current incomplete-declaration snapshots.
    affected entries: 1incomplete decls: 0missing decls: 2total debt: 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