GitHub - roed314/gq2: An explicit marked profinite presentation of the absolute Galois group of Q₂: four generators, two relations, and a pro-2 wild-inertia condition, with interactive paper, two Lean 4 formalizations, and a finite-quotient verifier

Branches Tags

Name		Name	Last commit message	Last commit date
Latest commit History 39 Commits
artifacts		artifacts
blueprint-gpt		blueprint-gpt
blueprint		blueprint
development		development
errata		errata
formalizations		formalizations
lean		lean
paper		paper
presentations		presentations
reproducibility		reproducibility
vendor		vendor
verifier		verifier
.nojekyll		.nojekyll
CITATION.cff		CITATION.cff
apple-touch-icon.png		apple-touch-icon.png
bg-knowls.js		bg-knowls.js
favicon.ico		favicon.ico
favicon.svg		favicon.svg
index.html		index.html
paper.pdf		paper.pdf
site.css		site.css
status.json		status.json

About

An explicit marked profinite presentation of the absolute Galois group of Q₂: four generators, two relations, and a pro-2 wild-inertia condition, with interactive paper, two Lean 4 formalizations, and a finite-quotient verifier

roed314.github.io/gq2/