§6: quadratic determinant obstructions — statements

Statement-first extraction of the paper's §6 (pages 21–37): the Gauss-sign pair 6.8/6.9, the D₈/Evens-norm normalization 6.13, the orbit–stabilizer Shapiro ledger 6.15, the Hilbert ledger 6.16 → 6.17 → 6.18 (the dyadic base determinant theorem, the section's headline), and the transgression/shear pair 6.21/6.22. Every statement carries its paper display number; all are proved (Ax: B5, B6, B9; B7′ has since been proved as a theorem). The definitional layer here (factor sets, graph pullbacks, orbit cocycles, the local functional ι_F) never needed the proofs; classes of cocycles are formed with the junk-total H2ofFun/H1ofFun (GQ2/Corestriction.lean).

Design rationale, statement-by-statement display map, and flagged deviations (democratic Arf, canonical transversals, 6.5/6.19 represented through their downstream interfaces, 6.13's (100) folded into 6.15's (105), 6.21 in consequence form, (83) as the definition shape of Q⁰_A): docs/section67-extraction.md.

The §6 objects, as encoded here

• Factor-set data (Lemma 6.1, eqs. (59)–(62)): FactorSet C V carries the normalized factor set f and the equivariant-lift corrections m_c; IsEquivariantFactorSet q dat is the Prop bundle (59)/(60) + square map + polar compatibility. kappa0 is the base central cocycle (61) on V ⋊ C; graphPullback dat ρ b is its pullback (62) along a lower map ρ and a 1-cochain b — the only form the statements consume.
• The local functional ι_F = inv_{ℚ₂} (§6 opening): iotaF D : H²(G_ℚ₂, 𝔽₂) →+ 𝔽₂ through the 𝔽₂ ≅ μ₂ coefficient bridge (muTwoOfF2) and B6's invariant D.inv (GQ2/TateDuality.lean). Q0loc (eq. (92)) is the base quadratic connecting map, on H¹-classes via the canonical representative (Quotient.out; well-definedness = Lemma 6.4, a the §§6–7 proof layer obligation).
• Deep units (§6.3, eqs. (93)/(94)): IsDeepUnit N A says A = 1 + 2b with ‖b‖ < 1, A, b fixed by N — i.e. A ∈ U_{e+1}(K) for K the fixed field of N, phrased through the spectral norm on ℚ̄₂ (Mathlib's NormedField (AlgebraicClosure ℚ_[p])), with no ramification-index bookkeeping: v_K(A−1) ≥ e+1 ⟺ ‖A−1‖ < ‖2‖.
• Ramified/unramified (for 6.9/6.18): the module's lower map factors through GQ2.Ttame (GQ2/BoundaryFrame.lean), and the dichotomy is whether the inertia generator tameTau acts trivially on V. U = S^{ω₂} is powOmega2 (GQ2/Omega2.lean) of the Frobenius image.

Axioms: none consumed here (statement layer).

Instance transports: the trivial G_ℚ₂-action on 𝔽₂

GQ2/Kummer.lean registers the trivial action for GaloisGroup ℚ₂ = ℚ̄₂ ≃ₐ[ℚ₂] ℚ̄₂; we transport it to the AbsGalQ2-phrasing (definitionally the same group), following the GQ2/MuN.lean precedent.

@[implicit_reducible]

instance GQ2.instDistribMulActionAbsGalQ2ZModOfNatNat : DistribMulAction AbsGalQ2 (ZMod 2)

Equations

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

instance GQ2.instContinuousSMulAbsGalQ2ZModOfNatNat : ContinuousSMul AbsGalQ2 (ZMod 2)

theorem GQ2.absGal_smul_zmodTwo (g : AbsGalQ2) (m : ZMod 2) : g • m = m

The G_ℚ₂-action on 𝔽₂ is trivial (definitionally).

The local functional ι_F = inv_{ℚ₂} (§6 opening display)

noncomputable def GQ2.SectionSix.negOneMuTwo : MuN 2

−1 as an element of μ₂ ⊂ ℚ̄₂ˣ (additively written).

Equations

• GQ2.SectionSix.negOneMuTwo = Additive.ofMul ⟨-1, GQ2.SectionSix.negOneMuTwo._proof_1⟩

noncomputable def GQ2.SectionSix.muTwoOfF2 : ZMod 2 →+ MuN 2

The coefficient bridge 𝔽₂ →+ μ₂, 1 ↦ −1.

Equations

• GQ2.SectionSix.muTwoOfF2 = (ZMod.lift 2) ⟨(zmultiplesHom (GQ2.MuN 2)) GQ2.SectionSix.negOneMuTwo, GQ2.SectionSix.muTwoOfF2._proof_1⟩

theorem GQ2.SectionSix.smul_negOneMuTwo (g : AbsGalQ2) : g • negOneMuTwo = negOneMuTwo

Galois fixes −1 ∈ μ₂ (it lies in the base field).

theorem GQ2.SectionSix.muTwoOfF2_equivariant (g : AbsGalQ2) (n : ZMod 2) : muTwoOfF2 (g • n) = g • muTwoOfF2 n

The bridge is G_ℚ₂-equivariant (both actions relevant: trivial on 𝔽₂, Galois on μ₂).

noncomputable def GQ2.SectionSix.iotaF (D : TateDuality 2) : ContCoh.H2 AbsGalQ2 (ZMod 2) →+ ZMod 2

The local source functional ι_F = inv_{ℚ₂} : H²(G_ℚ₂, 𝔽₂) → 𝔽₂ (§6 opening display), through the 𝔽₂ ≅ μ₂ bridge and B6's invariant map (D.inv, GQ2/TateDuality.lean). Parametrized by a duality bundle D : TateDuality 2, so the statement layer stays axiom-free.

Equations

• GQ2.SectionSix.iotaF D = D.inv.toAddMonoidHom.comp (GQ2.ContCoh.mapCoeff2 GQ2.SectionSix.muTwoOfF2 GQ2.SectionSix.iotaF._proof_5 GQ2.SectionSix.muTwoOfF2_equivariant)

Factor-set data (Lemma 6.1, eqs. (59)–(62)) — moved to GQ2/OrbitData.lean

FactorSet, IsEquivariantFactorSet, kappa0, graphPullback, FactorSet.comap now live in GQ2/OrbitData.lean (top-level namespace GQ2), reachable here unqualified. See docs/orchestration/orbit-data-refactor.md.

Q⁰_loc: the base quadratic connecting map (§6.3, eq. (92))

noncomputable def GQ2.SectionSix.Q0loc {C : Type} [Group C] [TopologicalSpace C] {V : Type} [AddCommGroup V] [TopologicalSpace V] [DiscreteTopology V] [DistribMulAction AbsGalQ2 V] [DistribMulAction C V] (D : TateDuality 2) (dat : FactorSet C V) (ρ : AbsGalQ2 →ₜ* C) : ContCoh.H1 AbsGalQ2 V → ZMod 2

Q⁰_loc (eq. (92)): Q⁰_loc([b]) = inv_{ℚ₂}((b, ρ)^* κ⁰_q), on H¹(G_ℚ₂, V) via the canonical cocycle representative. Independence of the representative (and of the datum, given IsEquivariantFactorSet) is the Lemma 6.4 content — a the §§6–7 proof layer obligation, not baked into the definition. Junk value 0 when the pullback is not a cocycle (H2ofFun).

Equations

• GQ2.SectionSix.Q0loc D dat ρ x = (GQ2.SectionSix.iotaF D) (GQ2.H2ofFun GQ2.AbsGalQ2 (GQ2.graphPullback dat ⇑ρ ↑(Quotient.out x)))

theorem GQ2.SectionSix.graphPullback_mem_Z2 {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] {V : Type} [AddCommGroup V] [TopologicalSpace V] [DiscreteTopology V] [DistribMulAction AbsGalQ2 V] [DistribMulAction C V] {q : V → ZMod 2} (dat : FactorSet C V) (hdat : IsEquivariantFactorSet q dat) (ρ : AbsGalQ2 →ₜ* C) (hρ : ∀ (g : AbsGalQ2) (v : V), g • v = ρ g • v) (b : ↥(ContCoh.Z1 AbsGalQ2 V)) : graphPullback dat ⇑ρ ↑b ∈ ContCoh.Z2 AbsGalQ2 (ZMod 2)

Well-formedness of the graph pullback (Lemma 6.1's cocycle assertion, specialized to the graph (62)): for an equivariant factor-set datum and a continuous 1-cocycle b (with the G_ℚ₂-action on V acting through ρ), the pullback is a continuous 2-cocycle. Paper: Lemma 6.1, display (62). [the §§6–7 statement; proof the §§6–7 proof layer.]

The Gauss-sign pair: Wall doubling and the candidate base counts

(§6.2: Lemma 6.6, Lemma 6.8, Proposition 6.9)

The candidate base form is taken in its evaluated shape (83): Q⁰_A = q when the inertia image is trivial (T = 1), and Q⁰_A = q_U = qDouble q U with U = S^{ω₂} when V^T = 0 (ramified). Deriving (83) from the relator ledger is Prop 6.5 = the Fox–Heisenberg design seam (deviation note §6.5).

def GQ2.SectionSix.onePlusU {V : Type u_1} [AddCommGroup V] (U : V ≃+ V) : V →+ V

The additive endomorphism 1 + U of V (char 2).

Equations

• GQ2.SectionSix.onePlusU U = AddMonoidHom.mk' (fun (v : V) => v + U v) ⋯

theorem GQ2.SectionSix.lemma_6_6 {V : Type u_1} [AddCommGroup V] [Finite V] (q : V → ZMod 2) (hq : QuadraticFp2.IsQuadraticFp2 q) (h2 : ∀ (v : V), v + v = 0) (hns : QuadraticFp2.Nonsingular q) (U : V ≃+ V) (hUq : ∀ (v : V), q (U v) = q v) (hU2 : ∃ (n : ℕ), (⇑U)^[2 ^ n] = id) : QuadraticFp2.Nonsingular (QuadraticFp2.qDouble q ⇑U) ∧ ∃ (k : ℕ), Nat.card ↥(onePlusU U).range = 2 ^ k ∧ QuadraticFp2.arf (QuadraticFp2.qDouble q ⇑U) = QuadraticFp2.arf q + ↑k

Lemma 6.6 (Wall doubling), eq. (86): for a nonsingular q and an orthogonal operator U of 2-power order, the doubling q_U(x) = q(x) + B(x, Ux) is nonsingular and Arf(q_U) = Arf(q) + rank(1 + U) (mod 2). The rank enters as the exponent k of #im(1 + U) = 2^k. [the §§6–7 statement; proof the §§6–7 proof layer.]

theorem GQ2.SectionSix.lemma_6_8 {V : Type u_1} [AddCommGroup V] [Finite V] {Hf : Type} [Group Hf] [TopologicalSpace Hf] [Finite Hf] [DistribMulAction Hf V] (c : ↑Ttame.toProfinite.toTop →ₜ* Hf) : Function.Surjective ⇑c → ∀ (hfaith : ∀ (h : Hf), (∀ (v : V), h • v = v) → h = 1), (∀ (W : AddSubgroup V), (∀ (h : Hf), ∀ w ∈ W, h • w ∈ W) → W = ⊥ ∨ W = ⊤) → c tameTau ≠ 1 → ∀ (q : V → ZMod 2) (hq : QuadraticFp2.IsQuadraticFp2 q) (hns : QuadraticFp2.Nonsingular q) (hinv : QuadraticFp2.IsInvariant Hf q) (hV2 : ∀ (v : V), v + v = 0) (s r a : ℕ) (hr : Odd r) (ha : 1 ≤ a) (hs1 : 1 ≤ s) (Wt : Type) [inst : AddCommGroup Wt] [inst✝ : DistribMulAction (↥(Subgroup.zpowers (c tameTau))) Wt] (hWt2 : ∀ (w : Wt), w + w = 0) (hWtsimple : FoxH.IsSimpleModTwo (↥(Subgroup.zpowers (c tameTau))) Wt) (hWcard : Nat.card Wt = 2 ^ (2 ^ a * r)) (e : V ≃+ (Fin s → Wt)) (he : ∀ (t : ↥(Subgroup.zpowers (c tameTau))) (v : V) (j : Fin s), e (↑t • v) j = t • e v j) (hVU : Nat.card { v : V // powOmega2 (c tameSigma) • v = v } = 2 ^ (r * s)) (hrank : ∀ (k : ℕ), Nat.card ↥(onePlusU (DistribMulAction.toAddEquiv V (powOmega2 (c tameSigma)))).range = 2 ^ k → ↑k = ↑s), QuadraticFp2.arf q = ↑s ∧ Nat.card { v : V // powOmega2 (c tameSigma) • v = v } = 2 ^ (r * s) ∧ (∃ (k : ℕ), Nat.card ↥(onePlusU (DistribMulAction.toAddEquiv V (powOmega2 (c tameSigma)))).range = 2 ^ k ∧ ↑k = ↑s) ∧ QuadraticFp2.arf (QuadraticFp2.qDouble q fun (x : V) => powOmega2 (c tameSigma) • x) = 0

Lemma 6.8 (ramified Hermitian model and Frobenius fixed space), eqs. (87)/(88): for a faithful simple ramified tame module V (tame image Hf marked by c : T_tame ↠ Hf; inertia T = c(τ) ≠ 1; V|_⟨T⟩ ≅ W^{⊕s} isotypic with #W = 2^f, f = 2^a·r, r odd, a ≥ 1) and an Hf-invariant nonsingular q:

• (87) Arf(q) ≡ s (mod 2);
• (88) #V^U = 2^{rs} and rank(1 + U) ≡ s (mod 2), for U = S^{ω₂} = powOmega2 (c σ);
• consequently Arf(q_U) = 0 (the ramified candidate base form of (83)).

[the §§6–7 statement; proof the §§6–7 proof layer.]

theorem GQ2.SectionSix.prop_6_9_unramified {V : Type u_1} [AddCommGroup V] [Finite V] {Hf : Type} [Group Hf] [TopologicalSpace Hf] [DiscreteTopology Hf] [Finite Hf] [DistribMulAction Hf V] (c : ↑Ttame.toProfinite.toTop →ₜ* Hf) (hc : Function.Surjective ⇑c) (hfaith : ∀ (h : Hf), (∀ (v : V), h • v = v) → h = 1) (hsimple : ∀ (W : AddSubgroup V), (∀ (h : Hf), ∀ w ∈ W, h • w ∈ W) → W = ⊥ ∨ W = ⊤) : (∃ (v : V), v ≠ 0) → ∀ (hunram : c tameTau = 1) (q : V → ZMod 2) (hq : QuadraticFp2.IsQuadraticFp2 q) (hns : QuadraticFp2.Nonsingular q) (hinv : QuadraticFp2.IsInvariant Hf q) (m : ℕ) (hm : 1 ≤ m) (hcard : Nat.card V = 2 ^ (2 * m)), QuadraticFp2.zeroCount q = 2 ^ (2 * m - 1) - 2 ^ (m - 1)

Proposition 6.9 (candidate base determinant zero count), eq. (91), unramified case: if inertia acts trivially (c(τ) = 1, so Q⁰_A = q by (83)) and #V = 2^{2m}, then #(Q⁰_A)⁻¹(0) = 2^{2m−1} − 2^{m−1} (negative Gauss sign). [the §§6–7 statement; proof the §§6–7 proof layer.]

theorem GQ2.SectionSix.prop_6_9_ramified {V : Type u_1} [AddCommGroup V] [Finite V] {Hf : Type} [Group Hf] [TopologicalSpace Hf] [Finite Hf] [DistribMulAction Hf V] (c : ↑Ttame.toProfinite.toTop →ₜ* Hf) (hc : Function.Surjective ⇑c) (hfaith : ∀ (h : Hf), (∀ (v : V), h • v = v) → h = 1) (hsimple : ∀ (W : AddSubgroup V), (∀ (h : Hf), ∀ w ∈ W, h • w ∈ W) → W = ⊥ ∨ W = ⊤) (hram : c tameTau ≠ 1) (q : V → ZMod 2) (hq : QuadraticFp2.IsQuadraticFp2 q) (hns : QuadraticFp2.Nonsingular q) (hinv : QuadraticFp2.IsInvariant Hf q) (hV2 : ∀ (v : V), v + v = 0) (s r a : ℕ) (hr : Odd r) (ha : 1 ≤ a) (hs1 : 1 ≤ s) (Wt : Type) [AddCommGroup Wt] [DistribMulAction (↥(Subgroup.zpowers (c tameTau))) Wt] (hWt2 : ∀ (w : Wt), w + w = 0) (hWtsimple : FoxH.IsSimpleModTwo (↥(Subgroup.zpowers (c tameTau))) Wt) (hWcard : Nat.card Wt = 2 ^ (2 ^ a * r)) (e : V ≃+ (Fin s → Wt)) (he : ∀ (t : ↥(Subgroup.zpowers (c tameTau))) (v : V) (j : Fin s), e (↑t • v) j = t • e v j) (hVU : Nat.card { v : V // powOmega2 (c tameSigma) • v = v } = 2 ^ (r * s)) (hrank : ∀ (k : ℕ), Nat.card ↥(onePlusU (DistribMulAction.toAddEquiv V (powOmega2 (c tameSigma)))).range = 2 ^ k → ↑k = ↑s) (m : ℕ) (hm : 1 ≤ m) (hcard : Nat.card V = 2 ^ (2 * m)) : QuadraticFp2.zeroCount (QuadraticFp2.qDouble q fun (x : V) => powOmega2 (c tameSigma) • x) = 2 ^ (2 * m - 1) + 2 ^ (m - 1)

Proposition 6.9, eq. (91), ramified case: if inertia acts nontrivially (Q⁰_A = q_U, U = S^{ω₂}, by (83)) and #V = 2^{2m}, then #(Q⁰_A)⁻¹(0) = 2^{2m−1} + 2^{m−1} (positive Gauss sign). [the §§6–7 statement; proof the §§6–7 proof layer.]

Lemma 6.13: the universal two-point class and the index-two Evens norm

The repo defines the index-two Evens norm by the two-point graph cocycle (98) (GQ2/EvensKahn.lean, per the Evens–Kahn interface design), so the paper's eq. (99) is definitional here. The remaining 6.13 content is the universal model: the explicit κ_J on E ⋊ J (eq. (95)), its D₈ fibre extension, and eq. (96) [κ_J] = N^{Ev}(e₁^∨). Eq. (100) is folded into 6.15's (105) (deviation note).

@[reducible, inline]

abbrev GQ2.SectionSix.swapE : Type

The swap module E = 𝔽₂e₁ ⊕ 𝔽₂e_s with J = C₂ acting by the coordinate swap (Lemma 6.13). The acting group is Multiplicative (ZMod 2).

Equations

• GQ2.SectionSix.swapE = (ZMod 2 × ZMod 2)

def GQ2.SectionSix.swapSmul (c : Multiplicative (ZMod 2)) (v : swapE) : swapE

The swap action function: c · v = v for c = 1 and v.swap for the involution.

Equations

• GQ2.SectionSix.swapSmul c v = if Multiplicative.toAdd c = 0 then v else Prod.swap v

@[implicit_reducible]

instance GQ2.SectionSix.instSMulMultiplicativeZModOfNatNatSwapE : SMul (Multiplicative (ZMod 2)) swapE

Equations

• GQ2.SectionSix.instSMulMultiplicativeZModOfNatNatSwapE = { smul := GQ2.SectionSix.swapSmul }

@[implicit_reducible]

instance GQ2.SectionSix.instDistribMulActionMultiplicativeZModOfNatNatSwapE : DistribMulAction (Multiplicative (ZMod 2)) swapE

The swap action of J = Multiplicative (ZMod 2) on E.

Equations

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

def GQ2.SectionSix.twoPointDatum : FactorSet (Multiplicative (ZMod 2)) swapE

The factor-set datum of the universal two-point class (Lemma 6.13): f_J(x, y) = x₁·y_s, m_1 = 0, m_s(y) = y₁·y_s.

Equations

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

def GQ2.SectionSix.CentralExt (A : Type u_1) (_f : A → A → ZMod 2) : Type u_1

The central extension of a finite elementary abelian group by 𝔽₂ attached to a raw factor set f: the carrier A × 𝔽₂ with (v,z)·(w,t) = (v+w, z+t+f(v,w)). A Group instance is available exactly when f is a normalized 2-cocycle; for the concrete two-point f_J this is decidable (twoPointExtGroup).

Equations

• GQ2.SectionSix.CentralExt A _f = (A × ZMod 2)

@[implicit_reducible]

instance GQ2.SectionSix.instMulCentralExtOfAddCommGroup {A : Type u_1} [AddCommGroup A] (f : A → A → ZMod 2) : Mul (CentralExt A f)

The twisted multiplication on CentralExt.

Equations

• GQ2.SectionSix.instMulCentralExtOfAddCommGroup f = { mul := fun (p q : GQ2.SectionSix.CentralExt A f) => (p.1 + q.1, p.2 + q.2 + f p.1 q.1) }

@[reducible, inline]

abbrev GQ2.SectionSix.twoPointExt : Type

The fibre extension of the two-point class: E_{f_J} = E × 𝔽₂ with the f_J-twisted multiplication.

Equations

• GQ2.SectionSix.twoPointExt = GQ2.SectionSix.CentralExt GQ2.SectionSix.swapE GQ2.SectionSix.twoPointDatum.f

@[implicit_reducible]

instance GQ2.SectionSix.instDecidableEqTwoPointExt : DecidableEq twoPointExt

Equations

• GQ2.SectionSix.instDecidableEqTwoPointExt = GQ2.SectionSix.instDecidableEqTwoPointExt._aux_1

@[implicit_reducible]

instance GQ2.SectionSix.instFintypeTwoPointExt : Fintype twoPointExt

Equations

• GQ2.SectionSix.instFintypeTwoPointExt = { elems := GQ2.SectionSix.instFintypeTwoPointExt._aux_1, complete := GQ2.SectionSix.instFintypeTwoPointExt._proof_3 }

@[implicit_reducible]

instance GQ2.SectionSix.twoPointExtGroup : Group twoPointExt

The group structure on the two-point fibre extension — the axioms are kernel-checked finite computations over the 8 elements using kernel-checkable decide; native_decide does not appear.

Equations

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

theorem GQ2.SectionSix.lemma_6_13_dihedral : Nonempty (twoPointExt ≃* DihedralGroup 4)

Lemma 6.13, the D₈ claim: the fibre extension of the universal two-point class is the dihedral group of order 8 — via the explicit exponent-table map r ↦ ẽ₁ẽ_s, sr 0 ↦ ẽ₁; all axioms are kernel-checked finite computations. Paper: Lemma 6.13. [the §§6–7 proof layer.]

def GQ2.SectionSix.SemiProd (C : Type u_1) (V : Type u_2) [Group C] [AddCommGroup V] [DistribMulAction C V] : Type (max u_1 u_2)

The semidirect product V ⋊ C of an additive C-module, on the carrier V × C with (v,c)·(w,d) = (v + c·w, cd) — the group all §6 base classes live on (Lemma 6.1, display (66)). A bespoke synonym (rather than Mathlib's SemidirectProduct) avoids Multiplicative wrappers on the fibre; the paper's formulas transcribe verbatim.

Equations

• GQ2.SectionSix.SemiProd C V = (V × C)

@[implicit_reducible]

instance GQ2.SectionSix.SemiProd.instMul {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] : Mul (SemiProd C V)

Equations

• GQ2.SectionSix.SemiProd.instMul = { mul := fun (p q : GQ2.SectionSix.SemiProd C V) => (p.1 + p.2 • q.1, p.2 * q.2) }

@[implicit_reducible]

instance GQ2.SectionSix.SemiProd.instOne {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] : One (SemiProd C V)

Equations

• GQ2.SectionSix.SemiProd.instOne = { one := (0, 1) }

@[implicit_reducible]

instance GQ2.SectionSix.SemiProd.instInv {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] : Inv (SemiProd C V)

Equations

• GQ2.SectionSix.SemiProd.instInv = { inv := fun (p : GQ2.SectionSix.SemiProd C V) => (-(p.2⁻¹ • p.1), p.2⁻¹) }

@[simp]

theorem GQ2.SectionSix.SemiProd.mul_def {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] (a b : SemiProd C V) : a * b = (a.1 + a.2 • b.1, a.2 * b.2)

@[simp]

theorem GQ2.SectionSix.SemiProd.inv_def {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] (a : SemiProd C V) : a⁻¹ = (-(a.2⁻¹ • a.1), a.2⁻¹)

@[implicit_reducible]

instance GQ2.SectionSix.SemiProd.instGroup {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] : Group (SemiProd C V)

Equations

• GQ2.SectionSix.SemiProd.instGroup = Group.ofLeftAxioms ⋯ ⋯ ⋯

def GQ2.SectionSix.SemiProd.fibre {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] : Subgroup (SemiProd C V)

The fibre subgroup V × {1} ≤ V ⋊ C.

Equations

• GQ2.SectionSix.SemiProd.fibre = { carrier := {p : GQ2.SectionSix.SemiProd C V | p.2 = 1}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

@[implicit_reducible]

instance GQ2.SectionSix.SemiProd.instTopologicalSpace {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] : TopologicalSpace (SemiProd C V)

Equations

• GQ2.SectionSix.SemiProd.instTopologicalSpace = ⊥

instance GQ2.SectionSix.SemiProd.instDiscreteTopology {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] : DiscreteTopology (SemiProd C V)

@[implicit_reducible]

instance GQ2.SectionSix.SemiProd.instDistribMulActionZModOfNatNat {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] : DistribMulAction (SemiProd C V) (ZMod 2)

The trivial action of V ⋊ C on 𝔽₂ (every action on ℤ/2 is trivial).

Equations

• GQ2.SectionSix.SemiProd.instDistribMulActionZModOfNatNat = { smul := fun (x : GQ2.SectionSix.SemiProd C V) (m : ZMod 2) => m, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }

instance GQ2.SectionSix.SemiProd.instContinuousSMulZModOfNatNat {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] : ContinuousSMul (SemiProd C V) (ZMod 2)

def GQ2.SectionSix.fibreCoord (u : ↥SemiProd.fibre) : ZMod 2

The first-coordinate functional e₁^∨ on the fibre subgroup of E ⋊ J.

Equations

• GQ2.SectionSix.fibreCoord u = (↑u).1.1

theorem GQ2.SectionSix.lemma_6_13_evens (sJ : SemiProd (Multiplicative (ZMod 2)) swapE) (hsJ : sJ = (0, Multiplicative.ofAdd 1)) (hUi : SemiProd.fibre.index = 2) (hUo : IsOpen ↑SemiProd.fibre) (hs : sJ ∉ SemiProd.fibre) (htriv : ∀ (g : SemiProd (Multiplicative (ZMod 2)) swapE) (m : ZMod 2), g • m = m) (hα : ∀ (u v : ↥SemiProd.fibre), fibreCoord (u * v) = fibreCoord u + fibreCoord v) (hαc : Continuous fibreCoord) : (H2ofFun (SemiProd (Multiplicative (ZMod 2)) swapE) fun (p : SemiProd (Multiplicative (ZMod 2)) swapE × SemiProd (Multiplicative (ZMod 2)) swapE) => kappa0 twoPointDatum p.1 p.2) = evensNormH2 htriv hUo hUi hs fibreCoord hα hαc

Lemma 6.13, eq. (96): on E ⋊ J, the class of the explicit two-point cocycle κ_J (eq. (95) — kappa0 twoPointDatum as a raw function on the SemiProd carrier) is the index-two Evens norm of the first coordinate functional e₁^∨ ∈ H¹(E, 𝔽₂). Since the repo defines the Evens norm by the two-point graph cocycle (98) (GQ2/EvensKahn.lean, so the paper's (99) is definitional), this statement is the normalization anchoring that definition to the paper's universal model. Quantified over the side-condition proofs evensNormH2 takes. [the §§6–7 statement; proof the §§6–7 proof layer.]

Lemma 6.15: the quadratic orbit–stabilizer Shapiro ledger (eqs. (103)–(105))

Stated per orbit type on a single regular summand W = 𝔽₂[G/N] (the multi-orbit assembly is additivity of graphPullback in the datum; deviation note). Here G is the ambient (profinite) group, N ◁ G open of finite index (K/F Galois with group G/N), α ∈ Z¹(N, 𝔽₂) the scalar Shapiro coordinate, and b = Sh(α) the normalized Shapiro cochain (GQ2/Corestriction.lean).

theorem GQ2.SectionSix.lemma_6_15_square {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DistribMulAction G (ZMod 2)] [ContinuousSMul G (ZMod 2)] (N : Subgroup G) [N.Normal] : IsOpen ↑N → ∀ (α : ↥(ContCoh.Z1 (↥N) (ZMod 2))), H2ofFun G (graphPullback (squareOrbitDatum N) (⇑(QuotientGroup.mk' N)) (Corestriction.shapiroFun N ↑α)) = H2ofFun G (Corestriction.cor2Fun N fun (p : ↥N × ↥N) => ↑α p.1 * ↑α p.2)

Lemma 6.15, eq. (103) (square orbits): the graph pullback of the square-orbit datum at the Shapiro cochain of α is the corestriction of the cup square α ⌣ α. [the §§6–7 statement; proof the §§6–7 proof layer.]

theorem GQ2.SectionSix.lemma_6_15_free {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DistribMulAction G (ZMod 2)] [ContinuousSMul G (ZMod 2)] (N : Subgroup G) [N.Normal] [Finite (G ⧸ N)] (hNo : IsOpen ↑N) (α β : ↥(ContCoh.Z1 (↥N) (ZMod 2))) (ghat : G) : H2ofFun G (graphPullback (freeOrbitDatum N ((QuotientGroup.mk' N) ghat)) ⇑(QuotientGroup.mk' N) fun (γ : G) => (Corestriction.shapiroFun N (↑α) γ, Corestriction.shapiroFun N (↑β) γ)) = H2ofFun G (Corestriction.cor2Fun N fun (p : ↥N × ↥N) => ↑α p.1 * ↑β ⟨ghat⁻¹ * ↑p.2 * ghat, ⋯⟩)

Lemma 6.15, eq. (104) (free orbits): the graph pullback of the free-orbit datum with shift ḡ at the Shapiro cochains of α, β is the corestriction of α ⌣ ḡβ (ḡβ = conjugate cocycle through a lift ĝ of ḡ). [the §§6–7 statement; proof the §§6–7 proof layer.]

theorem GQ2.SectionSix.lemma_6_15_involution {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DistribMulAction G (ZMod 2)] [ContinuousSMul G (ZMod 2)] (N : Subgroup G) [N.Normal] [Finite (G ⧸ N)] (hNo : IsOpen ↑N) (α : ↥(ContCoh.Z1 (↥N) (ZMod 2))) (ghat : G) (hg : ghat ∉ N) (hg2 : ghat * ghat ∈ N) (U₀ : Subgroup G) (hU₀ : U₀ = N ⊔ Subgroup.zpowers ghat) (hs : ⟨ghat, ⋯⟩ ∉ N.subgroupOf U₀) : H2ofFun G (graphPullback (invOrbitDatum N ((QuotientGroup.mk' N) ghat)) (⇑(QuotientGroup.mk' N)) (Corestriction.shapiroFun N ↑α)) = H2ofFun G (Corestriction.cor2Fun U₀ fun (p : ↥U₀ × ↥U₀) => evensNormFun (N.subgroupOf U₀) ⟨ghat, ⋯⟩ (fun (u : ↥(N.subgroupOf U₀)) => ↑α ⟨↑↑u, ⋯⟩) (p.1, p.2))

Lemma 6.15, eq. (105) (involution orbits): for an involution ḡ = mk ĝ of G/N, the graph pullback of the involution-orbit datum at the Shapiro cochain of α is cor_{K₀/F} N^{Ev}_{K/K₀}(α), where U₀ = ⟨N, ĝ⟩ is the index-2-over-N subgroup (fixed field K₀ = K^{⟨ḡ⟩}) and the Evens norm is the repo's two-point graph cocycle (98). This statement also absorbs the paper's eq. (100) (deviation note). Quantified over the membership/side proofs. [the §§6–7 statement; proof the §§6–7 proof layer.]

The Hilbert ledger: deep units (Lemma 6.16 → Lemma 6.17 → Proposition 6.18)

def GQ2.SectionSix.IsDeepUnit (N : Subgroup (Kummer.GaloisGroup ℚ_[2])) (A : AlgebraicClosure ℚ_[2]) : Prop

Deep unit relative to a subgroup N ≤ G_ℚ₂ with fixed field K (§6.3, eqs. (93)/(94)): A ∈ U_{e+1}(K) ⊂ K^×/K^{×2} via the representative A = 1 + 2b, b ∈ 𝔭_K — phrased through the spectral norm on ℚ̄₂ (‖b‖ < 1 ⟺ v_K(b) ≥ 1, so ‖A − 1‖ < ‖2‖ ⟺ v_K(A−1) ≥ e+1, e = v_K(2)); K-rationality of A and b is N-fixedness. No ramification-index bookkeeping is needed.

Equations

• GQ2.SectionSix.IsDeepUnit N A = (A ≠ 0 ∧ (∀ g ∈ N, g • A = A) ∧ ∃ (b : AlgebraicClosure ℚ_[2]), (∀ g ∈ N, g • b = b) ∧ A = 1 + 2 * b ∧ ‖b‖ < 1)

theorem GQ2.SectionSix.lemma_6_16 (k L : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) [FiniteDimensional ℚ_[2] ↥k] (hkL : k ≤ L) (hindex : (L.fixingSubgroup.subgroupOf k.fixingSubgroup).index = 2) (hunram : ∀ (x : AlgebraicClosure ℚ_[2]), x ≠ 0 → x ∈ L → ∃ (y : AlgebraicClosure ℚ_[2]), y ≠ 0 ∧ y ∈ k ∧ ‖x‖ = ‖y‖) (d : (↥k)ˣ) (δ : AlgebraicClosure ℚ_[2]) (hδ : δ ^ 2 = ↑↑d) (hδL : δ ∈ L) (hLδ : L.fixingSubgroup.subgroupOf k.fixingSubgroup = (MulAction.stabilizer (Kummer.GaloisGroup ℚ_[2]) δ).subgroupOf k.fixingSubgroup) (A β : AlgebraicClosure ℚ_[2]) (hdeep : IsDeepUnit L.fixingSubgroup A) (hβ : β ^ 2 = A) (hβ0 : β ≠ 0) (u : (↥k)ˣ) (v : ↥k) (hAuv : A = ↑↑u + ↑v * δ) (s : ↥k.fixingSubgroup) (hs : s ∉ L.fixingSubgroup.subgroupOf k.fixingSubgroup) (htriv : ∀ (g : ↥k.fixingSubgroup) (m : ZMod 2), g • m = m) (hUo : IsOpen ↑(L.fixingSubgroup.subgroupOf k.fixingSubgroup)) (hα : ∀ (u v : ↥(L.fixingSubgroup.subgroupOf k.fixingSubgroup)), Kummer.kummerCocycleFun β ↑(↑u * ↑v) = Kummer.kummerCocycleFun β ↑↑u + Kummer.kummerCocycleFun β ↑↑v) (hαc : Continuous fun (u : ↥(L.fixingSubgroup.subgroupOf k.fixingSubgroup)) => Kummer.kummerCocycleFun β ↑↑u) : evensNormH2 htriv hUo hindex hs (fun (u : ↥(L.fixingSubgroup.subgroupOf k.fixingSubgroup)) => Kummer.kummerCocycleFun β ↑↑u) hα hαc = 0

Lemma 6.16 (deep-unit Evens norm), eq. (110): for an unramified quadratic extension L/k of finite dyadic local fields (encoded: G_L ≤ G_k of index 2, equal norm value groups) and a deep unit a ∈ U_{e+1}(L), the index-two Evens norm of the Kummer class [a] vanishes: N^{Ev}_{L/k}([a]) = 0 in H²(G_k, 𝔽₂).

The Evens norm is the repo's evensNormH2Z (the two-point graph cocycle (98)); the proof route is the Hilbert-symbol ledger (111)–(114) through axioms B9/B11 — GQ2/HilbertLedger.lean (the Hilbert-ledger proof, Ax: B7′, B9, B11). Quantified over the side-condition proofs. [the §§6–7 statement; the Hilbert-ledger proof amendment: added [FiniteDimensional ℚ_[2] k] (the statement's "finite dyadic local fields", needed by B9/B11) and the Kummer presentation of L/k — the generator data (d, δ, hδ, hLδ) with L = k(δ), δ² = d, and the coordinates (u, v, hAuv) of the deep unit A = u + vδ (the paper's "write L = k(√d), a = u + v√d"); consumers (6.17, the deep-part proof) construct these concretely, and char-≠2 Kummer theory guarantees them abstractly. See docs/section67-extraction.md.]

def GQ2.SectionSix.deepPart {C : Type} [Group C] [TopologicalSpace C] {V : Type} [AddCommGroup V] [TopologicalSpace V] [DiscreteTopology V] [DistribMulAction AbsGalQ2 V] (ρ : AbsGalQ2 →ₜ* C) : Set (ContCoh.H1 AbsGalQ2 V)

The deep half X₊ (Lemma 6.17): the classes x ∈ H¹(G_ℚ₂, V) all of whose scalar Kummer coordinates are deep units — for every functional φ ∈ V^∨, the restriction of φ∘x to N = ker ρ (= G_K, K the splitting field) is the Kummer class of a deep unit of K. Encodes X₊ = Hom_{H_V}(V^∨, U_{e+1}) ⊂ H¹(ℚ₂, V) without the Kummer-theoretic identification of H¹ (which is proof-side, the §§6–7 proof layer).

Equations

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

Transgression and the marking-preserving shear (§6.4: Lemmas 6.21, 6.22)

theorem GQ2.SectionSix.lemma_6_21 {C : Type} [Group C] {V : Type} [AddCommGroup V] [Finite V] [DistribMulAction C V] {B : Type} [Group B] [Finite B] (p : B →* C) (hp : Function.Surjective ⇑p) (i : Multiplicative V →* B) : Function.Injective ⇑i → ∀ (hrange : i.range = p.ker) (hconj : ∀ (b : B) (v : V), b * i (Multiplicative.ofAdd v) * b⁻¹ = i (Multiplicative.ofAdd (p b • v))) (q : V → ZMod 2) (hq : QuadraticFp2.IsQuadraticFp2 q) (hns : QuadraticFp2.Nonsingular q) (dat : FactorSet C V) (hdat : IsEquivariantFactorSet q dat) (ξ : B × B → ZMod 2) (hcocycle : ∀ (g h k : B), ξ (h, k) + ξ (g, h * k) = ξ (g * h, k) + ξ (g, h)) (hξq : ∀ (v : V), ξ (i (Multiplicative.ofAdd v), i (Multiplicative.ofAdd v)) = q v), ∃ (s : C →* B), ∀ (cc : C), p (s cc) = cc

Lemma 6.21 (determinant transgression), consequence form — relative to the fixed equivariant class κ⁰_q: if a finite extension 1 → V → B → C → 1 (encoded: p : B ↠ C with central-kernel data i) admits a class ξ ∈ Z²(B, 𝔽₂) whose fibre restriction has square map a nonsingular q (i.e. ξ(i v, i v) = q v), and an equivariant factor-set datum for q is supplied ((dat, hdat) = Lemma 6.1's κ⁰_q — the paper's stated hypothesis "assume a zero-section-normalized equivariant class restricting to q on V has been fixed"), then the extension splits: B ≅ V ⋊ C over C. The paper's obstruction formula d₂(q) = B_q^♭∘η (eq. (116)) is the proof mechanism (the Lemma 6.21 proof, GQ2/Transgression.lean); only the splitting consequence is consumed (§§8–9). Encoding correction: the κ⁰_q hypothesis restores the paper's relative clause, dropped by the original consequence-form extraction — without it the intrinsic equivariance obstruction blocks the proof; see docs/orchestration/p15i-transgression-gap.md. [the §§6–7 statement; proof the Lemma 6.21 proof.]

def GQ2.SectionSix.gammaEdge {C : Type} [Group C] {V : Type} [AddCommGroup V] [DistribMulAction C V] (γ : C → V →+ ZMod 2) : V × C → V × C → ZMod 2

The filtration-one difference term Γ_γ (eq. (64)) as a raw function on the product carrier V × C: Γ_γ((v,c),(w,d)) = γ(c)(c·w).

Equations

• GQ2.SectionSix.gammaEdge γ p q = (γ p.2) (p.2 • q.1)

def GQ2.SectionSix.inflScalar {C V : Type} (δ : C × C → ZMod 2) : V × C → V × C → ZMod 2

The inflated scalar term inf δ as a raw function on V × C.

Equations

• GQ2.SectionSix.inflScalar δ p q = δ (p.2, q.2)

def GQ2.SectionSix.shear {C V : Type} [AddCommGroup V] (a : C → V) : V × C → V × C

The shear s_a(v, c) = (v + a(c), c) (Lemma 6.22).

Equations

• GQ2.SectionSix.shear a p = (p.1 + a p.2, p.2)

def GQ2.SectionSix.thetaPhase {C : Type} [Group C] {V : Type} [AddCommGroup V] [DistribMulAction C V] (dat : FactorSet C V) (a : C → V) : C × C → ZMod 2

The base phase term Θ⁰_q(a) = (a, id_C)^* κ⁰_q (eq. (122)), a raw function on C × C.

Equations

• GQ2.SectionSix.thetaPhase dat a = GQ2.graphPullback dat id a

def GQ2.SectionSix.gammaCupA {C : Type} [Group C] {V : Type} [AddCommGroup V] [DistribMulAction C V] (γ : C → V →+ ZMod 2) (a : C → V) : C × C → ZMod 2

The mixed term (γ ⌣ a)(c, d) = γ(c)(c·a(d)) (eq. (123)).

Equations

• GQ2.SectionSix.gammaCupA γ a p = (γ p.1) (p.1 • a p.2)

theorem GQ2.SectionSix.lemma_6_22 {C : Type} [Group C] {V : Type} [AddCommGroup V] [DistribMulAction C V] (q : V → ZMod 2) (hq : QuadraticFp2.IsQuadraticFp2 q) (dat : FactorSet C V) (hdat : IsEquivariantFactorSet q dat) (γ : C → V →+ ZMod 2) (δ : C × C → ZMod 2) (a : C → V) (ha : ∀ (c d : C), a (c * d) = a c + c • a d) : ∃ (w : V × C → ZMod 2), ∀ (p q' : V × C), kappa0 dat (shear a p) (shear a q') + gammaEdge γ (shear a p) (shear a q') + inflScalar δ (shear a p) (shear a q') = kappa0 dat p q' + gammaEdge (fun (c : C) => γ c + AddMonoidHom.mk' (QuadraticFp2.polar q (a c)) ⋯) p q' + inflScalar (fun (cd : C × C) => δ cd + thetaPhase dat a cd + gammaCupA γ a cd) p q' + (w (p.1 + p.2 • q'.1, p.2 * q'.2) + w p + w q')

Lemma 6.22 (marking-preserving shear), eq. (121): pulling a general determinant class κ = κ⁰_q + Γ_γ + inf δ back along the shear s_a (for a 1-cocycle a ∈ Z¹(C, V)) shifts the edge by the polar adjoint and the scalar by the phase terms:

s_a^*κ = κ⁰_q + Γ_{γ + B_q^♭ a} + inf(δ + Θ⁰_q(a) + γ ⌣ a),

as an identity of 𝔽₂-valued functions on (V ⋊ C)² up to a normalized coboundary — here stated cochain-exactly modulo the coboundary of an explicit 1-cochain w, quantified existentially. In particular (q nonsingular) a unique edge-killing shear class exists — recorded as the paper's phase-cover input to §8 (Prop 8.8). [the §§6–7 statement; proof the §§6–7 proof layer.]

Paper-tag ledger (auto-generated by paperforge; do not edit)

• eq. (100) = ⟦eq-halforbit-transfer-description⟧
• eq. (102) = ⟦eq-regularnaturality⟧
• eq. (103) = ⟦eq-shapirosquare⟧
• eq. (104) = ⟦eq-shapirofree⟧
• eq. (105) = ⟦eq-shapiroevens⟧
• eq. (110) = ⟦eq-evensvanish⟧
• eq. (115) = ⟦eq-localzeros⟧
• eq. (116) = ⟦eq-transgressionformula⟧
• eq. (121) = ⟦eq-shearformula⟧
• eq. (122) = ⟦eq-Thetadef⟧
• eq. (123) = ⟦eq-gammacupa⟧
• eq. (59) = ⟦eq-mquadratic⟧
• eq. (62) = ⟦eq-baseconnectingcochain⟧
• eq. (64) = ⟦eq-Gammagamma⟧
• eq. (77) = ⟦eq-basepullback⟧
• eq. (86) = ⟦eq-relativeArf⟧
• eq. (87) = ⟦eq-ramifiedarfq⟧
• eq. (91) = ⟦eq-candidatezeros⟧
• eq. (92) = ⟦eq-localbaseQ⟧
• eq. (93) = ⟦eq-squareclassgraded⟧
• eq. (95) = ⟦eq-universal-two-point-cocycle⟧
• eq. (96) = ⟦eq-universal-evens-class⟧
• eq. (99) = ⟦eq-evens-normalization⟧
• Lemma 6.1 = ⟦lem-extraspecialconnecting⟧
• Lemma 6.13 = ⟦lem-twopointevans⟧
• Lemma 6.14 = ⟦lem-regularrealization⟧
• Lemma 6.15 = ⟦lem-orbitshapiro⟧
• Lemma 6.16 = ⟦lem-evensvanish⟧
• Lemma 6.17 = ⟦lem-shapirodet⟧
• Lemma 6.21 = ⟦lem-transgression⟧
• Lemma 6.22 = ⟦lem-shear⟧
• Lemma 6.4 = ⟦lem-detnormalizationindependence⟧
• Lemma 6.6 = ⟦lem-wall⟧
• Lemma 6.8 = ⟦lem-ramifiedhermitian⟧
• Proposition 6.18 = ⟦prop-localzero⟧
• Prop 6.5 = ⟦prop-wordquadratic⟧
• Prop 6.9 = ⟦prop-candidatezero⟧
• Prop 8.8 = ⟦prop-phaseidentity⟧