Three of the proposed presentations of $\operatorname{Gal}(\overline{\mathbb{Q}}_2/\mathbb{Q}_2)$ are developed enough to compare head to head: the presentation proved in the paper, David Roe’s shorter presentation (verifier-passed when this comparison was built, since proved in Appendix C and checked in Lean), and a new hybrid that GPT proposed on July 26, 2026 in the course of building exactly this comparison. This page fixes names for the three, explains the comparison model, and records its conclusions; the complete calculation is in the underlying note (PDF).
A comparison reads badly when every sentence tracks provenance, so we name each presentation for the block that dominates its wild relator. The presentation proved in the paper is the collector presentation: its relator is assembled from the class-two collector word $h_0$. Roe’s candidate is the square-commutator presentation: its relator closes with the literal block $x_1^2[x_1,x_1^{\sigma_2}]$. The hybrid is the twisted-square presentation: its principal block is the twisted square $y^{\sigma_2^2}y\,d^2$ with $y=x_0d^{-1}$. (The note calls them the paper, Roe, and hybrid presentations.)
The three presentations
All three share the same frame. Writing $x^g=g^{-1}xg$ and $[x,y]=x^{-1}y^{-1}xy$, each is topologically generated by $\sigma,\tau,x_0,x_1$, with the closed normal subgroup generated by $x_0,x_1$ required to be pro-$2$, subject to the common tame relation $\tau^\sigma=\tau^2$ and one wild relation, which is where they differ. As on the presentations page, $\omega_2\in\widehat{\mathbb{Z}}$ is the idempotent projecting to $1$ in the $\mathbb{Z}_2$ component and to $0$ in every odd component. Expand a name to see the wild relation.
The collector presentation
Proved in the paper and formalized in Lean; found by David Turturean with GPT on June 23, 2026. Named for the class-two collector word $h_0$, assembled by collecting commutators to the right.
Put
$$\begin{aligned} \sigma_2&=\sigma^{\omega_2}, & u_i&=(x_i\tau)^{\omega_2}\ \ (i=0,1), & d_0&=u_0x_0^{-1},\\ z_0&=x_0^{\sigma_2}, & c_0&=[d_0,z_0], & g_0&=\sigma_2^{2},\\ d_g&=d_0^{g_0}, & h_c&=[d_g,d_0], & h_0&=x_0^{g_0}x_0\,d_gd_0d_0^{2}h_c. \end{aligned}$$The wild relation is
$$h_0\,u_1^{-1}\,x_1^{\sigma}\,c_0=1.$$The square-commutator presentation
Verifier-passed, and proved and formalized on July 26, 2026 (Appendix C); found by David Roe with Fable 5 on June 10, 2026. Named for the literal square-and-commutator block $x_1^2[x_1,x_1^{\sigma_2}]$ that closes its relator.
Put
$$\sigma_2=\sigma^{\omega_2},\qquad a=(x_0^{-3}\tau)^{\omega_2},\qquad y_1=x_1^{\sigma_2},\qquad c=[x_1,y_1].$$The wild relation is
$$(x_0^{\sigma})^{-1}\,a\,x_1^{2}\,c=1.$$The twisted-square presentation
Proposed by GPT on July 26, 2026, together with this comparison; verifier-passed the same day. Named for its principal block $(x_0d^{-1})^{\sigma_2^2}x_0d$, which equals the twisted square $y^{\sigma_2^2}y\,d^2$ for $y=x_0d^{-1}$.
Put
$$\sigma_2=\sigma^{\omega_2},\qquad u_i=(x_i\tau)^{\omega_2}\ \ (i=0,1),\qquad d=u_0x_0^{-1}.$$The wild relation is
$$(x_0d^{-1})^{\sigma_2^{2}}\,x_0d\;u_1^{-1}\,x_1^{\sigma}\,[d,x_0^{\sigma_2}]=1.$$Status badges
Every candidate card on the presentations page and on this page carries a status badge from a fixed five-level scale. "Proven" on its own is too compressed for this project, where a claim can be proved in the manuscript, checked in Lean modulo the axiom census, proved equivalent to a proven presentation, or merely supported through a finite range of tests. Solid badges mark theorem-level status, outlined badges mark experimental status, and red badges mark refuted proposals.
- Manuscript theorem
- Proved in the current manuscript with a complete human-readable proof (in the main text or an appendix).
- Lean-checked
- The statement has a
sorry-free Lean 4 proof resting only on the project's nine named external interfaces; "×2" means two independently initiated formalizations. - Proved-equivalent reformulation
- Obtained from a proven presentation by an explicit change of generators (Nielsen or Tietze moves), so its correctness follows from the proven one. No current candidate carries this badge; it is defined for future proposals.
- Verifier-supported
- Passed the finite-quotient verifier on all 5,402 test groups. Strong evidence, not a proof. An amber qualifier badge records any additional non-formal evidence (an AI proof sketch, or an AI-checked but unformalized proof).
- Untested candidate
- Proposed, but not yet run through the verifier and without a proof.
- Verifier-failed Incorrect
- Refuted: the verifier found a finite group with the wrong count, or a direct computation showed the proposal wrong.
The model
A single number cannot rank presentations honestly. Tietze and Nielsen transformations trade short relators for complicated generators, and a tower of auxiliary definitions can make a printed relator look artificially short. More importantly, the paper’s proof never consumes the wild relator whole: different quotients of the word drive different stages of the argument, and a relator can make one stage trivial while making another one hard. The note therefore scores each presentation $P$ by a five-component vector
$$C(P)=\bigl(L,\ C_{\text{pro-2}},\ C_{\text{Fox}},\ C_{\text{quad}},\ C_{\text{mark}}\bigr),$$whose entries are not meant to be added without first choosing application-dependent weights. The first coordinate measures the word itself; the other four measure how much work each stage of the paper’s proof needs when run on that word.
Straight-line length $L$
$L$ is straight-line-program size, not the letter count of the expanded free word, computed in a fixed grammar:
- generators and previously defined auxiliary words are free;
- each multiplication, inversion, conjugation, commutator, integer power, and $\omega_2$-power costs $1$ (a product of $n$ displayed factors costs $n-1$);
- each auxiliary definition is charged once, and later reuse is free;
- the tame relation $\tau^\sigma=\tau^2$ is omitted, since it is common to all three presentations.
In particular an $\omega_2$-power is charged as a single primitive profinite operation. The grammar is a convention, not an intrinsic invariant, but it prevents free abbreviations from gaming the count: every auxiliary word and every primitive operation is charged exactly once.
Four proof-stage scores
The paper’s proof confronts the wild relator four times, and each confrontation gets an ordinal score:
| 1 | direct calculation or an explicit one-line normalization |
| 2 | one short structural lemma or a small case split |
| 3 | a substantial word ledger, orientation calculation, or auxiliary normalization |
- $C_{\text{pro-2}}$: the work needed to identify the maximal pro-$2$ quotient abstractly with the rank-three dyadic Demushkin group;
- $C_{\text{Fox}}$: the candidate-specific work needed to obtain the evaluated simple-factor Fox Jacobian, the linear (first-order) input to the deformation argument;
- $C_{\text{quad}}$: the work needed to identify the mixed Heisenberg pairing and the extraspecial determinant quadratic form, the class-two (second-order) input;
- $C_{\text{mark}}$: the additional work needed to pin down the full integral unramified character, not merely its reduction modulo $2$.
The last coordinate is scored separately because it is logically independent of the mod-$2$ structure: two one-relator pro-$2$ groups can share the same quadratic initial form while placing the unramified $\mathbb{Z}_2$-coordinate differently in their abelianizations. And one caveat applies throughout: the scores measure the proof route furnished by the methods of the paper. They are not evidence of correctness: the collector presentation remains the only proven one.
The scores
| component | collector | square-commutator | twisted-square |
|---|---|---|---|
| definitions before the principal block | 12 | 6 | 7 |
| principal square or collector block | 7 | 1 | 6 |
| remaining operations in the final relator | 5 | 5 | 7 |
| $L$ | 24 | 12 | 20 |
The square-commutator presentation is decisively shortest in this grammar. (The twisted-square split charges $(x_0d^{-1})^{\sigma_2^2}x_0d$ as one reusable block; counting straight off the displayed relator instead gives $7$ definitions and $13$ relator operations, the same total.)
Pro-$2$ quotient and integral marking. In a finite $2$-group quotient $\tau$ dies and $\omega_2$-powering is the identity, so each wild relator collapses to a pro-$2$ relation. The collector and twisted-square relators collapse to the same relation, $x_0^{\sigma^2}x_0[x_1,\sigma]=1$, and an explicit Nielsen substitution identifies it with the standard marked Demushkin presentation: abstract identification and integral marking in one stroke, so both presentations score $1$ on both coordinates. The square-commutator relator collapses instead to $(x_0^\sigma)^{-1}x_0^{-3}x_1^2[x_1,x_1^\sigma]=1$; its degree-two initial form is nondegenerate of the correct dyadic Demushkin type, so the abstract group is recognized, but the marked identification runs through a genuine $2$-adic orientation calculation, scoring $3$ on both coordinates.
The Nielsen substitution
The relation $x_0^{\sigma^2}x_0[x_1,\sigma]=1$ admits the explicit Nielsen normalization
$$\sigma=s,\qquad x_1=y,\qquad x_0=s^{-2}a^{-1}$$from the standard marked rank-three dyadic Demushkin presentation
$$\langle a,s,y\mid a^2s^4[s,y]=1\rangle_{\text{pro-}2}.$$From $\nu_{\mathrm{ur}}(a,s,y)=(-2,1,0)$ it follows immediately that $\nu_{\mathrm{ur}}(\sigma)=1$ and $\nu_{\mathrm{ur}}(x_0)=\nu_{\mathrm{ur}}(x_1)=0$: the unramified character is read off integrally, not just modulo $2$.
The orientation calculation
Writing $S=\chi(\sigma)$, $X=\chi(x_0)$, $Y=\chi(x_1)$ for the values of the orientation character, the square-commutator pro-$2$ relator forces
$$Y=-X^2,\qquad X^3+2X^2+1=0,\qquad S=-\frac{X^3}{X^2+X+1}.$$One must choose the unique root $X\equiv5\pmod{16}$, verify $S\equiv13\pmod{16}$, and finish with an orientation-preserving abelian correction. This is a genuine $2$-adic normalization rather than a direct Nielsen substitution.
First order: Fox calculus. All three presentations share the tame row of the evaluated Fox Jacobian, and all three land on essentially the same matrix: the square-commutator Jacobian is the collector Jacobian with its two wild columns interchanged. The difference is the work needed to get there. The square-commutator relator differentiates directly (its square and commutator have vanishing first derivative in characteristic $2$): score $1$. The collector presentation needs a separate shadow lemma (that the long word $h_0$ has the elementary shadow of $x_0^2$) extracted from the full finite-word ledger: score $3$. The twisted-square block’s first derivative vanishes by a short two-case split: score $2$.
The evaluated Fox Jacobian
At a tame lower map, write variations of $(\sigma,\tau,x_0,x_1)$ as $(a,b,c,d)$, let $\mathsf{S},\mathsf{T}$ be the lower actions of $\sigma,\tau$, put $\mathsf{U}=\mathsf{S}^{\omega_2}$, and let $P=1+\mathsf{T}+\cdots+\mathsf{T}^{e-1}$ be the norm projector for the odd order $e$ of $\mathsf{T}$. The collector and twisted-square presentations evaluate to
$$J=\begin{pmatrix} \mathsf{S}^{-1}(1+\mathsf{T})&\mathsf{S}^{-1}+1+\mathsf{T}&0&0\\ 0&P&0&P+\mathsf{S}^{-1} \end{pmatrix},$$with columns indexed by $(a,b,c,d)$; the square-commutator presentation gives the same matrix with the two wild columns interchanged (its wild row is $Pb+(P+\mathsf{S}^{-1})c$).
Second order: the quadratic layer. The sharpest separation is at class two. The square-commutator relator wears its quadratic data on its sleeve; the literal square and commutator directly give the normalized form $q(d)+b_q(d,\mathsf{U}^{-1}d)$, where $q$ is the extraspecial determinant form and $b_q$ its polar pairing: score $1$. The twisted-square block is governed by a two-case square identity in central extensions showing it carries exactly the class-two data of $x_0^2$: score $2$. The collector presentation reaches the same conclusion only through the full collector ledger: score $3$. The three resulting forms agree: the collector and twisted-square forms coincide outright, and match the square-commutator form after exchanging the wild coordinates.
The square identity
Lemma. Let $1\to Z\to E\to V\to 1$ be a central extension and let $\phi$ be an automorphism of $E$ fixing $Z$ pointwise. For $X,D\in E$ put
$$H_\phi(X,D)=(XD^{-1})^\phi(XD^{-1})D^2.$$If $X$ and $D$ have the same image in $V$, then $H_\phi(X,D)=X^2$: writing $D=Xz$ with $z\in Z$ gives $XD^{-1}=z^{-1}$ and $H_\phi(X,D)=z^{-2}(Xz)^2=X^2$. If instead $D\in Z$ and $\phi=1$, centrality gives $(XD^{-1})^2D^2=X^2$.
In the $P=0$ case the images of $d$ and $x_0$ agree, so the first case applies; in the $P=1$ case $d$ is central on the normalized representatives and $\sigma_2^2$ acts trivially on the class-two coefficients, so the second case applies. Either way the twisted-square block has exactly the same Heisenberg and extraspecial coordinates as $x_0^2$.
| presentation | $L$ | $C_{\text{pro-2}}$ | $C_{\text{Fox}}$ | $C_{\text{quad}}$ | $C_{\text{mark}}$ |
|---|---|---|---|---|---|
| collector | 24 | 1 | 3 | 3 | 1 |
| square-commutator | 12 | 3 | 1 | 1 | 3 |
| twisted-square | 20 | 1 | 2 | 2 | 1 |
Conclusions
In this model the twisted-square presentation strictly improves the collector presentation: it is shorter, it keeps the same immediate marked pro-$2$ normalization, and its first- and second-order analyses are strictly easier. The square-commutator and twisted-square presentations do not dominate one another, so the Pareto frontier has exactly two points.
Shortest and cohomologically simplest. Favored by this scoring model when the goal is the shortest theorem statement or the smallest candidate-specific Fox calculation, at the price of a genuinely $2$-adic marked normalization.
Simplest balanced marked proof. Favored by this scoring model when the goal is to minimize the complete proof while keeping the full unramified marking explicit, at the price of eight more straight-line operations.
None of this changes the epistemic ordering: the collector and square-commutator presentations are both proven and formalized, the second in Appendix C, unconditionally and on the same axiom base as the first. The twisted-square presentation has passed the finite-quotient verifier but remains unproven, carrying an AI proof sketch along the paper’s architecture that has not itself been checked.
Limitations
The four proof-stage scores are ordinal assessments, not intrinsic invariants: they presuppose the proof architecture of the paper and treat the integral marking as a separate load-bearing input. The square-commutator presentation’s two marking coordinates looked at first like a gap that a new explicit Nielsen transformation might close; the proof in Appendix C settles that the other way, by showing that no triple of words in the generators of either pro-$2$ quotient generates the other and satisfies its relation, so those coordinates are a real feature of the presentation and not an artifact of not having looked hard enough. Conversely, a different proof strategy could make the full finite word, rather than its first two jets, the dominant cost. The length coordinate depends on the chosen grammar: charging $\omega_2$-powers by their cost in finite quotients would change all three totals. What the conventions buy is not canonicity but reproducibility.