D_R is a rank-3 Demushkin group with q = 2 (Roe note Lemma 3.2, ⟦lem:initial⟧)

Complete (skeleton ticket R7; the H¹ side is R12; the H² side and the cup Gram matrix are R13b, through the single-relator obstruction of GQ2/Roe/DRWordCoh.lean; the q-invariant consumes ticket R8's abelianization decomposition).

The note's Lemma 3.2: the degree-two initial form of r₂ is y² + [x,s], so D_R is a rank-three Demushkin group whose cup–Bockstein matrix in the basis dual to (s, x, y) is

[[0,1,0], [1,0,0], [0,0,1]], ⟦eq:cupmatrix⟧

which is nonsingular. Per the campaign plan (§3 Route L), no Zassenhaus filtration is formalized: the dimension counts and the Gram matrix are stated in the repo's cochain/cup vocabulary (GQ2.ContCoh + GQ2.trivialCupPairing), the route the tree already knows (Demushkin.lean, WordCoh2.lean, CardH2GammaA.lean), and feed the abstract IsDemushkin predicate — its first load-bearing use.

Encoding

• Dimensions are Nat.card clauses, as in IsDemushkin: dim H¹ = 3 is #H¹(D_R, 𝔽₂) = 8 and dim H² = 1 is #H²(D_R, 𝔽₂) = 2.
• The dual basis of (s, x, y): every triple v : Fin 3 → 𝔽₂ extends to a (continuous) character D_R → 𝔽₂ — the relator dies in any elementary-abelian target since its abelianization is −4x̄ + 2ȳ (drWord_comm) — giving classes drH1 v ∈ H¹(D_R, 𝔽₂); drSStar, drXStar, drYStar are the coordinate vectors. That drH1 is a bijection 𝔽₂³ ≃ H¹ is the rank-3 statement in basis form (drH1_bijective + card_H1_DR).
• The p = 2 pitfall (R2 spike): at p = 2 the diagonal of ⟦eq:cupmatrix⟧ is the Bockstein — u ∪ u = β(u) is additive in u — so the matrix is the Gram matrix of the symmetric bilinear cup form GQ2.trivialCupPairing (with the Bockstein on the diagonal), not the polar form of a quadratic form (the polar is alternating and would have zero diagonal). The nine entries are stated below as cup values against the dual basis, with #H² = 2 making "≠ 0" mean "= the generator". Do not reformulate through QuadraticForm/Arf: the spike documents how that briefly "refuted" the correct matrix.

Statement inventory

card_H1_DR, drH1_bijective (R12); card_H2_DR, the nine Gram entries drCup_* (R13); isDemushkin_DR (assembly: nondegeneracy from the Gram entries and the basis); demushkinRank_DR = 3 (proved from card_H1_DR); demushkinQ_DR = 2 (from R8's B_R = C₂t ⊕ ℤ₂s̄ ⊕ ℤ₂x̄, note eq. (3.6) ⟦eq:BRsplit⟧) — the invariant quadruple consumed by the B-Lab hypothesis (GQ2/Roe/MarkedPro2.lean).

The trivial coefficient action

Aut(ℤ/2) = 1, so every distributive action on 𝔽₂ is trivial; registering the literal trivial action globally is the house convention (GQ2/Kummer.lean, RStage/GammaA.lean).

@[implicit_reducible]

instance GQ2.instDistribMulActionDR : DistribMulAction (↑DR.toProfinite.toTop) (ZMod 2)

Equations

• One or more equations did not get rendered due to their size.

instance GQ2.instContinuousSMulCarrierToTopTotallyDisconnectedSpaceToProfiniteDRZModOfNatNat : ContinuousSMul (↑DR.toProfinite.toTop) (ZMod 2)

theorem GQ2.drSmul_trivial (g : ↑DR.toProfinite.toTop) (m : ZMod 2) : g • m = m

The D_R-action on 𝔽₂ is trivial (definitional).

The dual basis of H¹(D_R, 𝔽₂)

theorem GQ2.isProP_two_multZMod2_roe : IsProP 2 (Multiplicative (ZMod 2))

Multiplicative (ZMod 2) is pro-2 (a finite 2-group; local clone of GQ2.isProP_two_multZMod2, which lives downstream in GQ2/SectionThree.lean).

noncomputable def GQ2.drCharM (v : Fin 3 → ZMod 2) : ↑DR.toProfinite.toTop →ₜ* Multiplicative (ZMod 2)

The multiplicative 𝔽₂-character of D_R with generator values s, x, y ↦ v 0, v 1, v 2 (additively): well-defined for every triple v because the relator abelianizes to −4x̄ + 2ȳ = 0 (drWord_comm), which is vacuous mod 2 — the Burnside face of dim H¹ = 3.

Equations

• GQ2.drCharM v = GQ2.drLiftHom GQ2.isProP_two_multZMod2_roe (fun (i : Fin 3) => Multiplicative.ofAdd (v i)) ⋯

@[simp]

theorem GQ2.drCharM_drS (v : Fin 3 → ZMod 2) : (drCharM v) drS = Multiplicative.ofAdd (v 0)

@[simp]

theorem GQ2.drCharM_drX (v : Fin 3 → ZMod 2) : (drCharM v) drX = Multiplicative.ofAdd (v 1)

@[simp]

theorem GQ2.drCharM_drY (v : Fin 3 → ZMod 2) : (drCharM v) drY = Multiplicative.ofAdd (v 2)

noncomputable def GQ2.drZ1 (v : Fin 3 → ZMod 2) : ↥(ContCoh.Z1 (↑DR.toProfinite.toTop) (ZMod 2))

The additive 1-cocycle of the character drCharM v (for the trivial action, continuous 1-cocycles are continuous additive characters).

Equations

• GQ2.drZ1 v = ⟨fun (g : ↑GQ2.DR.toProfinite.toTop) => Multiplicative.toAdd ((GQ2.drCharM v) g), ⋯⟩

noncomputable def GQ2.drH1 (v : Fin 3 → ZMod 2) : ContCoh.H1 (↑DR.toProfinite.toTop) (ZMod 2)

The H¹(D_R, 𝔽₂)-class with coordinates v in the basis dual to (s, x, y).

Equations

• GQ2.drH1 v = (GQ2.ContCoh.H1mk (↑GQ2.DR.toProfinite.toTop) (ZMod 2)) (GQ2.drZ1 v)

noncomputable def GQ2.drSStar : ContCoh.H1 (↑DR.toProfinite.toTop) (ZMod 2)

s* ∈ H¹(D_R, 𝔽₂): the class dual to s.

Equations

• GQ2.drSStar = GQ2.drH1 ![1, 0, 0]

noncomputable def GQ2.drXStar : ContCoh.H1 (↑DR.toProfinite.toTop) (ZMod 2)

x* ∈ H¹(D_R, 𝔽₂): the class dual to x.

Equations

• GQ2.drXStar = GQ2.drH1 ![0, 1, 0]

noncomputable def GQ2.drYStar : ContCoh.H1 (↑DR.toProfinite.toTop) (ZMod 2)

y* ∈ H¹(D_R, 𝔽₂): the class dual to y.

Equations

• GQ2.drYStar = GQ2.drH1 ![0, 0, 1]

Topological generation of D_R by {drS, drX, drY}

The three named generators topologically generate D_R (GQ2.dr_topGen, ticket R8), so two continuous homs out of D_R agree once they agree on drS, drX, drY — R8's dr_hom_ext, the "characters are determined by generator values" input of drH1_bijective-surjectivity.

dim H¹ = 3 (fill: R12)

theorem GQ2.drH1_bijective : Function.Bijective drH1

The dual basis is a basis — v ↦ drH1 v is a bijection 𝔽₂³ ≃ H¹(D_R, 𝔽₂) ⟦lem:initial⟧. Injectivity evaluates classes on the generators (coboundaries vanish — the action is trivial); surjectivity is the Burnside/Frattini argument — a continuous 1-cocycle for the trivial action is a continuous character, determined by its generator values via topological generation (dr_hom_ext), and drCharM realizes every triple.

theorem GQ2.card_H1_DR : Nat.card (ContCoh.H1 (↑DR.toProfinite.toTop) (ZMod 2)) = 8

dim_𝔽₂ H¹(D_R, 𝔽₂) = 3, in Nat.card form ⟦lem:initial⟧ — the rank clause of the note's Lemma 3.2. Fill (R12): transport Nat.card (Fin 3 → ZMod 2) = 8 along drH1_bijective.

theorem GQ2.finite_H1_DR : Finite (ContCoh.H1 (↑DR.toProfinite.toTop) (ZMod 2))

H¹(D_R, 𝔽₂) is finite (clause 1 of IsDemushkin; from card_H1_DR).

The elementary-abelian quotient D_R ↠ 𝔽₂³ and the cup obstruction (fill: R13b)

The whole H² half runs through GQ2/Roe/DRWordCoh.lean's single-relator obstruction obsH2_DR : H²(D_R, 𝔽₂) →+ 𝔽₂, which is injective (obsH2_DR_injective) because a 2-cocycle with vanishing relator obstruction lifts through drLiftHom to a splitting section. Evaluating obsH2_DR on a cup product is then a finite computation: the cup cocycle (g, h) ↦ z_v(g) · z_w(h) factors through the elementary-abelian quotient drE : D_R → 𝔽₂³ assembled from the dual basis, so obsH2_DR_eq_of_factor rewrites the class as the single-relator obstruction of the explicit TwoCocycle 𝔽₂³ drCC v w, and decide evaluates the relator word r₂ in the resulting 16-element central extension.

The answer (drCup_obs) is the bilinear form B(v, w) = v₀w₁ + v₁w₀ + v₂w₂, i.e. exactly the Gram matrix ⟦eq:cupmatrix⟧ [[0,1,0],[1,0,0],[0,0,1]] — the off-diagonal [x,s]-pair and the y²-Bockstein. All nine entries, #H² = 2 and both nondegeneracy clauses are corollaries of this single identity.

dim H² = 1 (fill: R13)

theorem GQ2.card_H2_DR : Nat.card (ContCoh.H2 (↑DR.toProfinite.toTop) (ZMod 2)) = 2

dim_𝔽₂ H²(D_R, 𝔽₂) = 1, in Nat.card form ⟦lem:initial⟧ — "the presentation is minimal and has one relation". Fill (R13), one-relator central-extension route (clone of the WordCoh2/CardH2GammaA pattern): the upper bound from the single relator through the word cohomology bridge, the lower bound from a concrete finite central-extension witness detecting a nonzero class (equivalently, from any nonzero Gram entry below).

The cup–Bockstein Gram matrix ⟦eq:cupmatrix⟧ (fill: R13)

The nine entries of the matrix [[0,1,0],[1,0,0],[0,0,1]] of the symmetric bilinear cup form on H¹(D_R, 𝔽₂) in the dual basis (s*, x*, y*) — rows and columns in that order, diagonal entries the Bocksteins (u ∪ u = β(u) at p = 2; see the module docstring for the quadratic-form trap). With card_H2_DR, "≠ 0" says "= the generator of H² ≅ 𝔽₂". Both triangles are stated since graded-commutativity of cup11 is not formalized (the IsDemushkin.nondegen_left/right precedent).

theorem GQ2.drCup_ss : ((trivialCupPairing 2 (↑DR.toProfinite.toTop) drSmul_trivial) drSStar) drSStar = 0

Gram entry (s, s) = 0: the Bockstein β(s*) = s* ∪ s* vanishes (no s² in the initial form of r₂).

theorem GQ2.drCup_sx : ((trivialCupPairing 2 (↑DR.toProfinite.toTop) drSmul_trivial) drSStar) drXStar ≠ 0

Gram entry (s, x) = 1: s* ∪ x* ≠ 0 — the [x, s]-term of the initial form y² + [x,s] ⟦lem:initial⟧.

theorem GQ2.drCup_sy : ((trivialCupPairing 2 (↑DR.toProfinite.toTop) drSmul_trivial) drSStar) drYStar = 0

Gram entry (s, y) = 0.

theorem GQ2.drCup_xs : ((trivialCupPairing 2 (↑DR.toProfinite.toTop) drSmul_trivial) drXStar) drSStar ≠ 0

Gram entry (x, s) = 1 (the transpose of drCup_sx; stated separately since graded-commutativity is not formalized).

theorem GQ2.drCup_xx : ((trivialCupPairing 2 (↑DR.toProfinite.toTop) drSmul_trivial) drXStar) drXStar = 0

Gram entry (x, x) = 0: the Bockstein β(x*) vanishes — x enters r₂ with exponent −4 ≡ 0 (mod 4).

theorem GQ2.drCup_xy : ((trivialCupPairing 2 (↑DR.toProfinite.toTop) drSmul_trivial) drXStar) drYStar = 0

Gram entry (x, y) = 0.

theorem GQ2.drCup_ys : ((trivialCupPairing 2 (↑DR.toProfinite.toTop) drSmul_trivial) drYStar) drSStar = 0

Gram entry (y, s) = 0.

theorem GQ2.drCup_yx : ((trivialCupPairing 2 (↑DR.toProfinite.toTop) drSmul_trivial) drYStar) drXStar = 0

Gram entry (y, x) = 0.

theorem GQ2.drCup_yy : ((trivialCupPairing 2 (↑DR.toProfinite.toTop) drSmul_trivial) drYStar) drYStar ≠ 0

Gram entry (y, y) = 1: the Bockstein β(y*) = y* ∪ y* ≠ 0 — the y²-term of the initial form y² + [x,s] ⟦lem:initial⟧, and the diagonal 1 that makes the matrix nonsingular over 𝔽₂ (det = 1).

The Demushkin package

theorem GQ2.isDemushkin_DR : IsDemushkin 2 ↑DR.toProfinite.toTop

D_R is a Demushkin pro-2 group ⟦lem:initial⟧ — "this is exactly the defining cohomological condition". The first load-bearing use of the abstract IsDemushkin predicate. Nondegeneracy fill (R13, after the Gram entries): a class a·s* + b·x* + c·y* cups with x* to a, with s* to b, and with y* to c — the matrix [[0,1,0],[1,0,0],[0,0,1]] is nonsingular — using drH1_bijective to write an arbitrary nonzero class in coordinates.

theorem GQ2.demushkinRank_DR : demushkinRank 2 ↑DR.toProfinite.toTop = 3

D_R has Demushkin rank 3 ⟦lem:initial⟧ (8 = 2³; proved from card_H1_DR).

theorem GQ2.demushkinQ_DR : demushkinQ ↑DR.toProfinite.toTop = 2

D_R has q-invariant 2 ⟦eq:BR⟧/⟦eq:BRsplit⟧ (note (3.4)–(3.6)): the topological abelianization is B_R = ⟨s̄, x̄, ȳ | −4x̄ + 2ȳ = 0⟩ = C₂·t ⊕ ℤ₂·s̄ ⊕ ℤ₂·x̄ with t = ȳ − 2x̄, whose torsion subgroup has order 2. Fill: from ticket R8's BRDecomposition (the BDecomposition clone; see the R7 design memo §R8).

Paper-tag ledger (Roe note paper/roe-presentation-verification.tex; hand-maintained)

• Lemma 3.2 = ⟦lem:initial⟧
• eq. (3.2) = ⟦eq:cupmatrix⟧
• eq. (3.4)–(3.6) = ⟦eq:BR⟧/⟦eq:tR⟧/⟦eq:BRsplit⟧ (demushkinQ_DR; fill via ticket R8)