7. Quadratic determinant obstructions
Lemma7.1
Group: Quadratic determinant obstructions (12)
Associated Lean declarations
-
GQ2.QuadraticFp2.qDouble_nonsingular[complete] -
GQ2.SectionSix.lemma_6_6[complete]
Lemma 6.6 of the paper (Wall doubling).
Let (V,q) be nonsingular over \F_2, with polar form b_q, and let
\mathsf U\in O(V,q) have 2-power order. Put
q_{\mathsf U}(x)=q(x)+b_q(x,\mathsf U^{-1}x).
Then q_{\mathsf U} is nonsingular and
\Arf(q_{\mathsf U})=\Arf(q)+\operatorname{rank}(1+\mathsf U)\pmod2.
Lean code for Lemma7.1●2 theorems
Associated Lean declarations
-
GQ2.QuadraticFp2.qDouble_nonsingular[complete]
-
GQ2.SectionSix.lemma_6_6[complete]
Associated Lean declarations
-
GQ2.QuadraticFp2.qDouble_nonsingular[complete] -
GQ2.SectionSix.lemma_6_6[complete]
-
theoremdefined in GQ2/GaussCount/Wall.leancomplete
theorem GQ2.QuadraticFp2.qDouble_nonsingular.{u_2} {V : Type u_2} [AddCommGroup V] (q : V → ZMod 2) (U : V ≃+ V) [Finite V] (hq : GQ2.QuadraticFp2.IsQuadraticFp2 q) (h2 : ∀ (v : V), v + v = 0) (hns : GQ2.QuadraticFp2.Nonsingular q) (hUq : ∀ (v : V), q (U v) = q v) (hU2 : ∃ n, (⇑U)^[2 ^ n] = id) : GQ2.QuadraticFp2.Nonsingular (GQ2.QuadraticFp2.qDouble q ⇑U)
theorem GQ2.QuadraticFp2.qDouble_nonsingular.{u_2} {V : Type u_2} [AddCommGroup V] (q : V → ZMod 2) (U : V ≃+ V) [Finite V] (hq : GQ2.QuadraticFp2.IsQuadraticFp2 q) (h2 : ∀ (v : V), v + v = 0) (hns : GQ2.QuadraticFp2.Nonsingular q) (hUq : ∀ (v : V), q (U v) = q v) (hU2 : ∃ n, (⇑U)^[2 ^ n] = id) : GQ2.QuadraticFp2.Nonsingular (GQ2.QuadraticFp2.qDouble q ⇑U)
**Lemma 6.6, nonsingularity**: for a nonsingular `q` and a `2`-power-order isometry `U`, the doubling `q_U` is nonsingular (`1 + U + U⁻¹` is bijective on the finite `V`).
-
theoremdefined in GQ2/SectionSix.leancomplete
theorem GQ2.SectionSix.lemma_6_6.{u_1} {V : Type u_1} [AddCommGroup V] [Finite V] (q : V → ZMod 2) (hq : GQ2.QuadraticFp2.IsQuadraticFp2 q) (h2 : ∀ (v : V), v + v = 0) (hns : GQ2.QuadraticFp2.Nonsingular q) (U : V ≃+ V) (hUq : ∀ (v : V), q (U v) = q v) (hU2 : ∃ n, (⇑U)^[2 ^ n] = id) : GQ2.QuadraticFp2.Nonsingular (GQ2.QuadraticFp2.qDouble q ⇑U) ∧ ∃ k, Nat.card ↥(GQ2.SectionSix.onePlusU U).range = 2 ^ k ∧ GQ2.QuadraticFp2.arf (GQ2.QuadraticFp2.qDouble q ⇑U) = GQ2.QuadraticFp2.arf q + ↑k
theorem GQ2.SectionSix.lemma_6_6.{u_1} {V : Type u_1} [AddCommGroup V] [Finite V] (q : V → ZMod 2) (hq : GQ2.QuadraticFp2.IsQuadraticFp2 q) (h2 : ∀ (v : V), v + v = 0) (hns : GQ2.QuadraticFp2.Nonsingular q) (U : V ≃+ V) (hUq : ∀ (v : V), q (U v) = q v) (hU2 : ∃ n, (⇑U)^[2 ^ n] = id) : GQ2.QuadraticFp2.Nonsingular (GQ2.QuadraticFp2.qDouble q ⇑U) ∧ ∃ k, Nat.card ↥(GQ2.SectionSix.onePlusU U).range = 2 ^ k ∧ GQ2.QuadraticFp2.arf (GQ2.QuadraticFp2.qDouble q ⇑U) = GQ2.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.]
Lemma7.2
Group: Quadratic determinant obstructions (12)
Used by 2
Associated Lean declarations
Lemma 6.7 of the paper (Invariant quadratic forms on a hermitian line).
Let F/F_0 be a quadratic extension of finite fields of characteristic 2,
write x\mapsto x^* for its involution, and let
\mathcal U_1=\{u\in F^\times:uu^*=1\}. Let W be a one-dimensional F-space. Every
nonsingular \mathcal U_1-invariant quadratic form Q:W\to\F_2 is uniquely of the form
Q(x)=\Tr_{F_0/\F_2}(a xx^*) \qquad (a\in F_0^\times).
Lean code for Lemma7.2●1 theorem
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in GQ2/DeepPart/HermitianCount.leancomplete
theorem GQ2.DeepPart.hermitian_form_eq_trace_form.{u_1} {D : Type u_1} [Field D] [Fintype D] {m : ℕ} (hm : 1 ≤ m) (hcard : Fintype.card D = 2 ^ (2 * m)) [Algebra (ZMod (ringChar D)) D] (e2 : ZMod (ringChar D) ≃+ ZMod 2) (Q : D → ZMod 2) (hQ : GQ2.QuadraticFp2.IsQuadraticFp2 Q) (hns : GQ2.QuadraticFp2.Nonsingular Q) (hU : ∀ (u : Dˣ), u ^ (2 ^ m + 1) = 1 → ∀ (x : D), Q (↑u * x) = Q x) : ∃ c, c ^ 2 ^ m ≠ c ∧ ∀ (x : D), Q x = e2 ((Algebra.trace (ZMod (ringChar D)) D) (c * x ^ (2 ^ m + 1)))
theorem GQ2.DeepPart.hermitian_form_eq_trace_form.{u_1} {D : Type u_1} [Field D] [Fintype D] {m : ℕ} (hm : 1 ≤ m) (hcard : Fintype.card D = 2 ^ (2 * m)) [Algebra (ZMod (ringChar D)) D] (e2 : ZMod (ringChar D) ≃+ ZMod 2) (Q : D → ZMod 2) (hQ : GQ2.QuadraticFp2.IsQuadraticFp2 Q) (hns : GQ2.QuadraticFp2.Nonsingular Q) (hU : ∀ (u : Dˣ), u ^ (2 ^ m + 1) = 1 → ∀ (x : D), Q (↑u * x) = Q x) : ∃ c, c ^ 2 ^ m ≠ c ∧ ∀ (x : D), Q x = e2 ((Algebra.trace (ZMod (ringChar D)) D) (c * x ^ (2 ^ m + 1)))
**Lemma 6.7 (invariant quadratic forms on a Hermitian line), existence form**: every nonsingular quadratic form on `D = 𝔽_{2^{2m}}` invariant under the norm-one circle `U = {u : u^{2^m+1} = 1}` is the Hermitian trace form of some `c` outside the fixed field. (The adjoint identity holds on a subring containing `U`, hence everywhere; the polar form is then trace-represented with Frobenius-fixed coefficient, an Artin–Schreier preimage matches the polars, and the additive `U`-invariant difference vanishes.)
Lemma7.3
Group: Quadratic determinant obstructions (12)
Associated Lean declarations
-
GQ2.GaussSigns.arf_qDouble_eq_zero[complete] -
GQ2.GaussSigns.arf_eq_s_ramified[complete] -
GQ2.SectionSix.lemma_6_8[complete]
Lemma 6.8 of the paper (Ramified Hermitian model and Frobenius fixed space).
Let I=\langle \mathsf T\rangle be tame inertia, let V be a simple ramified
self-dual \F_2[H_V]-module, and write
V|_I\cong W^{\oplus s}, \qquad f=\dim_{\F_2}W=2^a r, \qquad r\text{ odd},\quad a\ge1.
Let q be an H_V-invariant nonsingular quadratic form with polar form b_q.
Then
\Arf(q)\equiv s\pmod2.
For \mathsf U=\mathsf S^{\omega_2} one also has
\dim_{\F_2}V^{\mathsf U}=rs, \qquad \operatorname{rank}(1+\mathsf U)=rs(2^a-1)\equiv s\pmod2.
Consequently the ramified candidate base form of (83) has
\Arf(Q_A^0)=0.
Lean code for Lemma7.3●3 theorems
Associated Lean declarations
-
GQ2.GaussSigns.arf_qDouble_eq_zero[complete]
-
GQ2.GaussSigns.arf_eq_s_ramified[complete]
-
GQ2.SectionSix.lemma_6_8[complete]
Associated Lean declarations
-
GQ2.GaussSigns.arf_qDouble_eq_zero[complete] -
GQ2.GaussSigns.arf_eq_s_ramified[complete] -
GQ2.SectionSix.lemma_6_8[complete]
-
theoremdefined in GQ2/GaussSigns.leancomplete
theorem GQ2.GaussSigns.arf_qDouble_eq_zero.{u_1} {V : Type u_1} [AddCommGroup V] [Finite V] (q : V → ZMod 2) (U : V ≃+ V) (hq : GQ2.QuadraticFp2.IsQuadraticFp2 q) (h2 : ∀ (v : V), v + v = 0) (hns : GQ2.QuadraticFp2.Nonsingular q) (hUq : ∀ (v : V), q (U v) = q v) (hU2 : ∃ n, (⇑U)^[2 ^ n] = id) (N : V →+ V) (hN : ∀ (x : V), N x = x + U x) {k : ℕ} (hk : Nat.card ↥N.range = 2 ^ k) {s : ZMod 2} (h87 : GQ2.QuadraticFp2.arf q = s) (h88 : ↑k = s) : GQ2.QuadraticFp2.arf (GQ2.QuadraticFp2.qDouble q ⇑U) = 0
theorem GQ2.GaussSigns.arf_qDouble_eq_zero.{u_1} {V : Type u_1} [AddCommGroup V] [Finite V] (q : V → ZMod 2) (U : V ≃+ V) (hq : GQ2.QuadraticFp2.IsQuadraticFp2 q) (h2 : ∀ (v : V), v + v = 0) (hns : GQ2.QuadraticFp2.Nonsingular q) (hUq : ∀ (v : V), q (U v) = q v) (hU2 : ∃ n, (⇑U)^[2 ^ n] = id) (N : V →+ V) (hN : ∀ (x : V), N x = x + U x) {k : ℕ} (hk : Nat.card ↥N.range = 2 ^ k) {s : ZMod 2} (h87 : GQ2.QuadraticFp2.arf q = s) (h88 : ↑k = s) : GQ2.QuadraticFp2.arf (GQ2.QuadraticFp2.qDouble q ⇑U) = 0
**Lemma 6.8, final clause, from (87) and (88)**: for a nonsingular `q` and a 2-power-order isometry `U` with `arf q = s` and rank exponent `k ≡ s (mod 2)` for `N = 1 + U`, the doubling has `arf (q_U) = 0`. (Wall's relation `arf (q_U) = arf q + k`, plus `s + s = 0`.)
-
theoremdefined in GQ2/GaussSignsRamified.leancomplete
theorem GQ2.GaussSigns.arf_eq_s_ramified.{u_1, u_2, u_3} {V : Type u_1} [AddCommGroup V] [Finite V] {W : Type u_2} [AddCommGroup W] {G : Type u_3} [Group G] [Finite G] [DistribMulAction G V] [DistribMulAction G W] (T : G) (hTgen : ∀ (g : G), g ∈ Subgroup.zpowers T) (hVfaith : ∀ (g : G), (∀ (v : V), g • v = v) → g = 1) (hWsimple : GQ2.FoxH.IsSimpleModTwo G W) : (∀ (v : V), v + v = 0) → ∀ (hW2 : ∀ (w : W), w + w = 0) (q : V → ZMod 2) (hq : GQ2.QuadraticFp2.IsQuadraticFp2 q) (hns : GQ2.QuadraticFp2.Nonsingular q) (hqinv : ∀ (g : G) (v : V), q (g • v) = q v) (m' s : ℕ) (hm' : 1 ≤ m') (hs1 : 1 ≤ s) (hWcard : Nat.card W = 2 ^ (2 * m')) (e : V ≃+ (Fin s → W)) (he : ∀ (g : G) (v : V) (j : Fin s), e (g • v) j = g • e v j), GQ2.QuadraticFp2.arf q = ↑s
theorem GQ2.GaussSigns.arf_eq_s_ramified.{u_1, u_2, u_3} {V : Type u_1} [AddCommGroup V] [Finite V] {W : Type u_2} [AddCommGroup W] {G : Type u_3} [Group G] [Finite G] [DistribMulAction G V] [DistribMulAction G W] (T : G) (hTgen : ∀ (g : G), g ∈ Subgroup.zpowers T) (hVfaith : ∀ (g : G), (∀ (v : V), g • v = v) → g = 1) (hWsimple : GQ2.FoxH.IsSimpleModTwo G W) : (∀ (v : V), v + v = 0) → ∀ (hW2 : ∀ (w : W), w + w = 0) (q : V → ZMod 2) (hq : GQ2.QuadraticFp2.IsQuadraticFp2 q) (hns : GQ2.QuadraticFp2.Nonsingular q) (hqinv : ∀ (g : G) (v : V), q (g • v) = q v) (m' s : ℕ) (hm' : 1 ≤ m') (hs1 : 1 ≤ s) (hWcard : Nat.card W = 2 ^ (2 * m')) (e : V ≃+ (Fin s → W)) (he : ∀ (g : G) (v : V) (j : Fin s), e (g • v) j = g • e v j), GQ2.QuadraticFp2.arf q = ↑s
**Lemma 6.8 (87)** in engine form: for a finite cyclic `G = ⟨T⟩` acting faithfully on `V`, simply on the exponent-2 module `W` (`#W = 2^{2m'}`), with `V ≅ W^{⊕s}` `G`-equivariantly (via `e`, `he`) and a nonsingular `G`-invariant `q`, the Arf invariant is `arf q = s`. `G` acts diagonally on `V ≅ W^{⊕s}`, freely on `V ∖ 0` (`T` fixes only `0` in the simple faithful `W`), preserving `q`; `#G = ord(T)` divides `2^{2m'} − 1` (`T` a unit of `𝔽₂[T]`) but not `2^{m'} − 1` (`T` irreducible on `W`), so `GaussSigns.arf_eq_of_free` gives `arf q = s`. -
theoremdefined in GQ2/SectionSix.leancomplete
theorem GQ2.SectionSix.lemma_6_8.{u_1} {V : Type u_1} [AddCommGroup V] [Finite V] {Hf : Type} [Group Hf] [TopologicalSpace Hf] [Finite Hf] [DistribMulAction Hf V] (c : ↑GQ2.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 GQ2.tameTau ≠ 1 → ∀ (q : V → ZMod 2) (hq : GQ2.QuadraticFp2.IsQuadraticFp2 q) (hns : GQ2.QuadraticFp2.Nonsingular q) (hinv : GQ2.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 GQ2.tameTau))) Wt] (hWt2 : ∀ (w : Wt), w + w = 0) (hWtsimple : GQ2.FoxH.IsSimpleModTwo (↥(Subgroup.zpowers (c GQ2.tameTau))) Wt) (hWcard : Nat.card Wt = 2 ^ (2 ^ a * r)) (e : V ≃+ (Fin s → Wt)) (he : ∀ (t : ↥(Subgroup.zpowers (c GQ2.tameTau))) (v : V) (j : Fin s), e (↑t • v) j = t • e v j) (hVU : Nat.card { v // GQ2.powOmega2 (c GQ2.tameSigma) • v = v } = 2 ^ (r * s)) (hrank : ∀ (k : ℕ), Nat.card ↥(GQ2.SectionSix.onePlusU (DistribMulAction.toAddEquiv V (GQ2.powOmega2 (c GQ2.tameSigma)))).range = 2 ^ k → ↑k = ↑s), GQ2.QuadraticFp2.arf q = ↑s ∧ Nat.card { v // GQ2.powOmega2 (c GQ2.tameSigma) • v = v } = 2 ^ (r * s) ∧ (∃ k, Nat.card ↥(GQ2.SectionSix.onePlusU (DistribMulAction.toAddEquiv V (GQ2.powOmega2 (c GQ2.tameSigma)))).range = 2 ^ k ∧ ↑k = ↑s) ∧ GQ2.QuadraticFp2.arf (GQ2.QuadraticFp2.qDouble q fun x => GQ2.powOmega2 (c GQ2.tameSigma) • x) = 0
theorem GQ2.SectionSix.lemma_6_8.{u_1} {V : Type u_1} [AddCommGroup V] [Finite V] {Hf : Type} [Group Hf] [TopologicalSpace Hf] [Finite Hf] [DistribMulAction Hf V] (c : ↑GQ2.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 GQ2.tameTau ≠ 1 → ∀ (q : V → ZMod 2) (hq : GQ2.QuadraticFp2.IsQuadraticFp2 q) (hns : GQ2.QuadraticFp2.Nonsingular q) (hinv : GQ2.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 GQ2.tameTau))) Wt] (hWt2 : ∀ (w : Wt), w + w = 0) (hWtsimple : GQ2.FoxH.IsSimpleModTwo (↥(Subgroup.zpowers (c GQ2.tameTau))) Wt) (hWcard : Nat.card Wt = 2 ^ (2 ^ a * r)) (e : V ≃+ (Fin s → Wt)) (he : ∀ (t : ↥(Subgroup.zpowers (c GQ2.tameTau))) (v : V) (j : Fin s), e (↑t • v) j = t • e v j) (hVU : Nat.card { v // GQ2.powOmega2 (c GQ2.tameSigma) • v = v } = 2 ^ (r * s)) (hrank : ∀ (k : ℕ), Nat.card ↥(GQ2.SectionSix.onePlusU (DistribMulAction.toAddEquiv V (GQ2.powOmega2 (c GQ2.tameSigma)))).range = 2 ^ k → ↑k = ↑s), GQ2.QuadraticFp2.arf q = ↑s ∧ Nat.card { v // GQ2.powOmega2 (c GQ2.tameSigma) • v = v } = 2 ^ (r * s) ∧ (∃ k, Nat.card ↥(GQ2.SectionSix.onePlusU (DistribMulAction.toAddEquiv V (GQ2.powOmega2 (c GQ2.tameSigma)))).range = 2 ^ k ∧ ↑k = ↑s) ∧ GQ2.QuadraticFp2.arf (GQ2.QuadraticFp2.qDouble q fun x => GQ2.powOmega2 (c GQ2.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.]
Proposition7.4
Group: Quadratic determinant obstructions (12)
Associated Lean declarations
-
GQ2.GaussSigns.prop_6_9_unramified_of_free[complete] -
GQ2.GaussSigns.prop_6_9_unramified_of_abelian[complete] -
GQ2.GaussSigns.prop_6_9_unramified_of_cyclic[complete] -
GQ2.SectionSix.prop_6_9_unramified[complete] -
GQ2.SectionSix.prop_6_9_ramified[complete]
Proposition 6.9 of the paper (Candidate base determinant zero count).
If d=\dim V, then
\#(Q_A^0)^{-1}(0)= \begin{cases} 2^{d-1}-2^{d/2-1},&V\text{ unramified},\\ 2^{d-1}+2^{d/2-1},&V\text{ ramified}. \end{cases}
Lean code for Proposition7.4●5 theorems
Associated Lean declarations
-
GQ2.GaussSigns.prop_6_9_unramified_of_free[complete]
-
GQ2.GaussSigns.prop_6_9_unramified_of_abelian[complete]
-
GQ2.GaussSigns.prop_6_9_unramified_of_cyclic[complete]
-
GQ2.SectionSix.prop_6_9_unramified[complete]
-
GQ2.SectionSix.prop_6_9_ramified[complete]
Associated Lean declarations
-
GQ2.GaussSigns.prop_6_9_unramified_of_free[complete] -
GQ2.GaussSigns.prop_6_9_unramified_of_abelian[complete] -
GQ2.GaussSigns.prop_6_9_unramified_of_cyclic[complete] -
GQ2.SectionSix.prop_6_9_unramified[complete] -
GQ2.SectionSix.prop_6_9_ramified[complete]
-
theoremdefined in GQ2/GaussSigns.leancomplete
theorem GQ2.GaussSigns.prop_6_9_unramified_of_free.{u_1, u_2} {V : Type u_1} [AddCommGroup V] [Finite V] (q : V → ZMod 2) (hq : GQ2.QuadraticFp2.IsQuadraticFp2 q) (hns : GQ2.QuadraticFp2.Nonsingular q) (m : ℕ) (hm : 1 ≤ m) (hcard : Nat.card V = 2 ^ (2 * m)) {U : Type u_2} [Group U] [Finite U] [MulAction U V] (hUdvd : ¬Nat.card U ∣ 2 ^ m - 1) (hU0 : ∀ (u : U), u • 0 = 0) (hUq : ∀ (u : U) (v : V), q (u • v) = q v) (hfree : ∀ (u : U) (v : V), v ≠ 0 → u • v = v → u = 1) : GQ2.QuadraticFp2.zeroCount q = 2 ^ (2 * m - 1) - 2 ^ (m - 1)
theorem GQ2.GaussSigns.prop_6_9_unramified_of_free.{u_1, u_2} {V : Type u_1} [AddCommGroup V] [Finite V] (q : V → ZMod 2) (hq : GQ2.QuadraticFp2.IsQuadraticFp2 q) (hns : GQ2.QuadraticFp2.Nonsingular q) (m : ℕ) (hm : 1 ≤ m) (hcard : Nat.card V = 2 ^ (2 * m)) {U : Type u_2} [Group U] [Finite U] [MulAction U V] (hUdvd : ¬Nat.card U ∣ 2 ^ m - 1) (hU0 : ∀ (u : U), u • 0 = 0) (hUq : ∀ (u : U) (v : V), q (u • v) = q v) (hfree : ∀ (u : U) (v : V), v ≠ 0 → u • v = v → u = 1) : GQ2.QuadraticFp2.zeroCount q = 2 ^ (2 * m - 1) - 2 ^ (m - 1)
**Proposition 6.9, unramified case, from a free action** (the arithmetic core, independent of building the endomorphism field): if a finite group `U` acts on `V` (`#V = 2^(2m)`) fixing `0`, preserving a nonsingular `q`, freely on `V ∖ 0`, and with order not dividing `2^m − 1`, then `#q⁻¹(0) = 2^(2m−1) − 2^(m−1)`. The free orbits (all of size `#U`) divide both the nonzero-zero count and the nonzero count, so `#U ∣ zeroCount − 1` and `#U ∣ #V − zeroCount`; if `arf q` were `0` these force `#U ∣ 2^m − 1`, excluded by hypothesis, so `arf q = 1`. In the paper `U` is the norm-one group of order `2^m + 1` (so `#U ∤ 2^m − 1` since `0 < 2^m − 1 < 2^m + 1`), but the cyclic invariance group `Hf` itself already works — see `prop_6_9_unramified_of_abelian`.
-
theoremdefined in GQ2/GaussSigns.leancomplete
theorem GQ2.GaussSigns.prop_6_9_unramified_of_abelian.{u_1, u_2} {V : Type u_1} [AddCommGroup V] [Finite V] (q : V → ZMod 2) (hq : GQ2.QuadraticFp2.IsQuadraticFp2 q) (hns : GQ2.QuadraticFp2.Nonsingular q) (m : ℕ) (hm : 1 ≤ m) (hcard : Nat.card V = 2 ^ (2 * m)) {Hf : Type u_2} [Group Hf] [Finite Hf] [DistribMulAction Hf V] (habelian : ∀ (g h : Hf), g * h = h * g) (hfaith : ∀ (g : Hf), (∀ (v : V), g • v = v) → g = 1) (hsimple : ∀ (W : AddSubgroup V), (∀ (g : Hf), ∀ w ∈ W, g • w ∈ W) → W = ⊥ ∨ W = ⊤) (hdvd : ¬Nat.card Hf ∣ 2 ^ m - 1) (hinv : ∀ (g : Hf) (v : V), q (g • v) = q v) : GQ2.QuadraticFp2.zeroCount q = 2 ^ (2 * m - 1) - 2 ^ (m - 1)
theorem GQ2.GaussSigns.prop_6_9_unramified_of_abelian.{u_1, u_2} {V : Type u_1} [AddCommGroup V] [Finite V] (q : V → ZMod 2) (hq : GQ2.QuadraticFp2.IsQuadraticFp2 q) (hns : GQ2.QuadraticFp2.Nonsingular q) (m : ℕ) (hm : 1 ≤ m) (hcard : Nat.card V = 2 ^ (2 * m)) {Hf : Type u_2} [Group Hf] [Finite Hf] [DistribMulAction Hf V] (habelian : ∀ (g h : Hf), g * h = h * g) (hfaith : ∀ (g : Hf), (∀ (v : V), g • v = v) → g = 1) (hsimple : ∀ (W : AddSubgroup V), (∀ (g : Hf), ∀ w ∈ W, g • w ∈ W) → W = ⊥ ∨ W = ⊤) (hdvd : ¬Nat.card Hf ∣ 2 ^ m - 1) (hinv : ∀ (g : Hf) (v : V), q (g • v) = q v) : GQ2.QuadraticFp2.zeroCount q = 2 ^ (2 * m - 1) - 2 ^ (m - 1)
**Proposition 6.9, unramified case, from abelian invariance** — the unramified branch reduced to two concrete facts. If a finite **abelian** group `Hf` acts on `V` (`#V = 2^(2m)`) faithfully, simply, preserving a nonsingular `q`, with `#Hf ∤ 2^m − 1`, then `#q⁻¹(0) = 2^(2m−1) − 2^(m−1)`. The action is automatically free on `V ∖ 0`: for `g ≠ 1`, the fixed space `{v | g • v = v}` is `Hf`-stable (by commutativity), so `⊥` or `⊤` by simplicity, and `⊤` would make `g` act trivially (contradicting faithfulness). This is exactly the unramified geometry — `Hf` is the cyclic Frobenius image — modulo the arithmetic input `#Hf ∤ 2^m − 1` (equivalently: the generator is not contained in the proper subfield `𝔽_{2^m}`, i.e. `V` is genuinely `2m`-dimensional and simple). -
theoremdefined in GQ2/GaussSigns.leancomplete
theorem GQ2.GaussSigns.prop_6_9_unramified_of_cyclic.{u_1, u_2} {V : Type u_1} [AddCommGroup V] [Finite V] (q : V → ZMod 2) (hq : GQ2.QuadraticFp2.IsQuadraticFp2 q) (hns : GQ2.QuadraticFp2.Nonsingular q) (m : ℕ) (hm : 1 ≤ m) (hcard : Nat.card V = 2 ^ (2 * m)) (h2 : ∀ (v : V), v + v = 0) {Hf : Type u_2} [Group Hf] [Finite Hf] [DistribMulAction Hf V] (g : Hf) (hgen : ∀ (x : Hf), x ∈ Subgroup.zpowers g) (hfaith : ∀ (h : Hf), (∀ (v : V), h • v = v) → h = 1) (hsimple : ∀ (W : AddSubgroup V), (∀ (h : Hf), ∀ w ∈ W, h • w ∈ W) → W = ⊥ ∨ W = ⊤) (hinv : ∀ (h : Hf) (v : V), q (h • v) = q v) : GQ2.QuadraticFp2.zeroCount q = 2 ^ (2 * m - 1) - 2 ^ (m - 1)
theorem GQ2.GaussSigns.prop_6_9_unramified_of_cyclic.{u_1, u_2} {V : Type u_1} [AddCommGroup V] [Finite V] (q : V → ZMod 2) (hq : GQ2.QuadraticFp2.IsQuadraticFp2 q) (hns : GQ2.QuadraticFp2.Nonsingular q) (m : ℕ) (hm : 1 ≤ m) (hcard : Nat.card V = 2 ^ (2 * m)) (h2 : ∀ (v : V), v + v = 0) {Hf : Type u_2} [Group Hf] [Finite Hf] [DistribMulAction Hf V] (g : Hf) (hgen : ∀ (x : Hf), x ∈ Subgroup.zpowers g) (hfaith : ∀ (h : Hf), (∀ (v : V), h • v = v) → h = 1) (hsimple : ∀ (W : AddSubgroup V), (∀ (h : Hf), ∀ w ∈ W, h • w ∈ W) → W = ⊥ ∨ W = ⊤) (hinv : ∀ (h : Hf) (v : V), q (h • v) = q v) : GQ2.QuadraticFp2.zeroCount q = 2 ^ (2 * m - 1) - 2 ^ (m - 1)
**Proposition 6.9, unramified case, from a cyclic generator** — the complete unramified reduction. If `Hf` is generated by a single `g` (the Frobenius) acting on the exponent-2 space `V` (`#V = 2^(2m)`) faithfully, simply, preserving a nonsingular `q`, then `#q⁻¹(0) = 2^(2m−1) − 2^(m−1)`. Both hypotheses of `prop_6_9_unramified_of_abelian` are discharged here: abelianness is immediate from cyclicity, and the arithmetic input `#Hf ∤ 2^m − 1` comes from the operator crux `irreducible_operator_pow_ne_one` applied to `T = (g • ·)` (were `#Hf ∣ 2^m − 1` we would have `T^(2^m−1) = 1` for the irreducible `T` on the `2m`-dimensional `V`, which it forbids).
-
theoremdefined in GQ2/SectionSix.leancomplete
theorem GQ2.SectionSix.prop_6_9_unramified.{u_1} {V : Type u_1} [AddCommGroup V] [Finite V] {Hf : Type} [Group Hf] [TopologicalSpace Hf] [DiscreteTopology Hf] [Finite Hf] [DistribMulAction Hf V] (c : ↑GQ2.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 ≠ 0) → ∀ (hunram : c GQ2.tameTau = 1) (q : V → ZMod 2) (hq : GQ2.QuadraticFp2.IsQuadraticFp2 q) (hns : GQ2.QuadraticFp2.Nonsingular q) (hinv : GQ2.QuadraticFp2.IsInvariant Hf q) (m : ℕ) (hm : 1 ≤ m) (hcard : Nat.card V = 2 ^ (2 * m)), GQ2.QuadraticFp2.zeroCount q = 2 ^ (2 * m - 1) - 2 ^ (m - 1)
theorem GQ2.SectionSix.prop_6_9_unramified.{u_1} {V : Type u_1} [AddCommGroup V] [Finite V] {Hf : Type} [Group Hf] [TopologicalSpace Hf] [DiscreteTopology Hf] [Finite Hf] [DistribMulAction Hf V] (c : ↑GQ2.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 ≠ 0) → ∀ (hunram : c GQ2.tameTau = 1) (q : V → ZMod 2) (hq : GQ2.QuadraticFp2.IsQuadraticFp2 q) (hns : GQ2.QuadraticFp2.Nonsingular q) (hinv : GQ2.QuadraticFp2.IsInvariant Hf q) (m : ℕ) (hm : 1 ≤ m) (hcard : Nat.card V = 2 ^ (2 * m)), GQ2.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.] -
theoremdefined in GQ2/SectionSix.leancomplete
theorem GQ2.SectionSix.prop_6_9_ramified.{u_1} {V : Type u_1} [AddCommGroup V] [Finite V] {Hf : Type} [Group Hf] [TopologicalSpace Hf] [Finite Hf] [DistribMulAction Hf V] (c : ↑GQ2.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 GQ2.tameTau ≠ 1) (q : V → ZMod 2) (hq : GQ2.QuadraticFp2.IsQuadraticFp2 q) (hns : GQ2.QuadraticFp2.Nonsingular q) (hinv : GQ2.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 GQ2.tameTau))) Wt] (hWt2 : ∀ (w : Wt), w + w = 0) (hWtsimple : GQ2.FoxH.IsSimpleModTwo (↥(Subgroup.zpowers (c GQ2.tameTau))) Wt) (hWcard : Nat.card Wt = 2 ^ (2 ^ a * r)) (e : V ≃+ (Fin s → Wt)) (he : ∀ (t : ↥(Subgroup.zpowers (c GQ2.tameTau))) (v : V) (j : Fin s), e (↑t • v) j = t • e v j) (hVU : Nat.card { v // GQ2.powOmega2 (c GQ2.tameSigma) • v = v } = 2 ^ (r * s)) (hrank : ∀ (k : ℕ), Nat.card ↥(GQ2.SectionSix.onePlusU (DistribMulAction.toAddEquiv V (GQ2.powOmega2 (c GQ2.tameSigma)))).range = 2 ^ k → ↑k = ↑s) (m : ℕ) (hm : 1 ≤ m) (hcard : Nat.card V = 2 ^ (2 * m)) : GQ2.QuadraticFp2.zeroCount (GQ2.QuadraticFp2.qDouble q fun x => GQ2.powOmega2 (c GQ2.tameSigma) • x) = 2 ^ (2 * m - 1) + 2 ^ (m - 1)
theorem GQ2.SectionSix.prop_6_9_ramified.{u_1} {V : Type u_1} [AddCommGroup V] [Finite V] {Hf : Type} [Group Hf] [TopologicalSpace Hf] [Finite Hf] [DistribMulAction Hf V] (c : ↑GQ2.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 GQ2.tameTau ≠ 1) (q : V → ZMod 2) (hq : GQ2.QuadraticFp2.IsQuadraticFp2 q) (hns : GQ2.QuadraticFp2.Nonsingular q) (hinv : GQ2.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 GQ2.tameTau))) Wt] (hWt2 : ∀ (w : Wt), w + w = 0) (hWtsimple : GQ2.FoxH.IsSimpleModTwo (↥(Subgroup.zpowers (c GQ2.tameTau))) Wt) (hWcard : Nat.card Wt = 2 ^ (2 ^ a * r)) (e : V ≃+ (Fin s → Wt)) (he : ∀ (t : ↥(Subgroup.zpowers (c GQ2.tameTau))) (v : V) (j : Fin s), e (↑t • v) j = t • e v j) (hVU : Nat.card { v // GQ2.powOmega2 (c GQ2.tameSigma) • v = v } = 2 ^ (r * s)) (hrank : ∀ (k : ℕ), Nat.card ↥(GQ2.SectionSix.onePlusU (DistribMulAction.toAddEquiv V (GQ2.powOmega2 (c GQ2.tameSigma)))).range = 2 ^ k → ↑k = ↑s) (m : ℕ) (hm : 1 ≤ m) (hcard : Nat.card V = 2 ^ (2 * m)) : GQ2.QuadraticFp2.zeroCount (GQ2.QuadraticFp2.qDouble q fun x => GQ2.powOmega2 (c GQ2.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.]
Lemma7.5
Group: Quadratic determinant obstructions (12)
Associated Lean declarations
-
GQ2.lemma_6_11_of_tame_pair[complete] -
GQ2.lemma_6_11[complete]
Lemma 6.11 of the paper (Faithful-image projectivity).
If V is ramified, then V and V^\vee are projective
\F_2[H_V]-modules.
Lean code for Lemma7.5●2 theorems
Associated Lean declarations
-
GQ2.lemma_6_11_of_tame_pair[complete]
-
GQ2.lemma_6_11[complete]
Associated Lean declarations
-
GQ2.lemma_6_11_of_tame_pair[complete] -
GQ2.lemma_6_11[complete]
-
theoremdefined in GQ2/RegularSummand/Involution.leancomplete
theorem GQ2.lemma_6_11_of_tame_pair {C : Type} [Group C] [Finite C] {V : Type} [AddCommGroup V] [Finite V] [DistribMulAction C V] {sg t : C} (hgen : Subgroup.closure {sg, t} = ⊤) (hrel : sg⁻¹ * t * sg = t ^ 2) (hV2 : ∀ (v : V), v + v = 0) (hfaith : ∀ (h : C), (∀ (v : V), h • v = v) → h = 1) (hsimple : ∀ (W : AddSubgroup V), (∀ (h : C), ∀ w ∈ W, h • w ∈ W) → W = ⊥ ∨ W = ⊤) (hram : ∃ v, t • v ≠ v) : ∃ N ι r, (∀ (h : C) (v : V) (n : Fin N) (x : C), ι (h • v) n x = ι v n (h⁻¹ * x)) ∧ (∀ (h : C) (F : Fin N → C → ZMod 2), (r fun n x => F n (h⁻¹ * x)) = h • r F) ∧ ∀ (v : V), r (ι v) = v
theorem GQ2.lemma_6_11_of_tame_pair {C : Type} [Group C] [Finite C] {V : Type} [AddCommGroup V] [Finite V] [DistribMulAction C V] {sg t : C} (hgen : Subgroup.closure {sg, t} = ⊤) (hrel : sg⁻¹ * t * sg = t ^ 2) (hV2 : ∀ (v : V), v + v = 0) (hfaith : ∀ (h : C), (∀ (v : V), h • v = v) → h = 1) (hsimple : ∀ (W : AddSubgroup V), (∀ (h : C), ∀ w ∈ W, h • w ∈ W) → W = ⊥ ∨ W = ⊤) (hram : ∃ v, t • v ≠ v) : ∃ N ι r, (∀ (h : C) (v : V) (n : Fin N) (x : C), ι (h • v) n x = ι v n (h⁻¹ * x)) ∧ (∀ (h : C) (F : Fin N → C → ZMod 2), (r fun n x => F n (h⁻¹ * x)) = h • r F) ∧ ∀ (v : V), r (ι v) = v
**Lemma 6.11, abstract tame-pair form**: the split-summand package from a generating pair `(sg, t)` with the tame relation, rather than a `Ttame`-marking. This is the form the κ⁰ assembly consumes (`ActsThroughTame` supplies exactly such a pair); the `Ttame` form below is a wrapper.
-
theoremdefined in GQ2/RegularSummand/Involution.leancomplete
theorem GQ2.lemma_6_11 {C : Type} [Group C] [TopologicalSpace C] [Finite C] {V : Type} [AddCommGroup V] [Finite V] [DistribMulAction C V] (c : ↑GQ2.Ttame.toProfinite.toTop →ₜ* C) (hgen : Subgroup.closure {c GQ2.tameSigma, c GQ2.tameTau} = ⊤) (hV2 : ∀ (v : V), v + v = 0) (hfaith : ∀ (h : C), (∀ (v : V), h • v = v) → h = 1) (hsimple : ∀ (W : AddSubgroup V), (∀ (h : C), ∀ w ∈ W, h • w ∈ W) → W = ⊥ ∨ W = ⊤) (hram : ∃ v, c GQ2.tameTau • v ≠ v) : ∃ N ι r, (∀ (h : C) (v : V) (n : Fin N) (x : C), ι (h • v) n x = ι v n (h⁻¹ * x)) ∧ (∀ (h : C) (F : Fin N → C → ZMod 2), (r fun n x => F n (h⁻¹ * x)) = h • r F) ∧ ∀ (v : V), r (ι v) = v
theorem GQ2.lemma_6_11 {C : Type} [Group C] [TopologicalSpace C] [Finite C] {V : Type} [AddCommGroup V] [Finite V] [DistribMulAction C V] (c : ↑GQ2.Ttame.toProfinite.toTop →ₜ* C) (hgen : Subgroup.closure {c GQ2.tameSigma, c GQ2.tameTau} = ⊤) (hV2 : ∀ (v : V), v + v = 0) (hfaith : ∀ (h : C), (∀ (v : V), h • v = v) → h = 1) (hsimple : ∀ (W : AddSubgroup V), (∀ (h : C), ∀ w ∈ W, h • w ∈ W) → W = ⊥ ∨ W = ⊤) (hram : ∃ v, c GQ2.tameTau • v ≠ v) : ∃ N ι r, (∀ (h : C) (v : V) (n : Fin N) (x : C), ι (h • v) n x = ι v n (h⁻¹ * x)) ∧ (∀ (h : C) (F : Fin N → C → ZMod 2), (r fun n x => F n (h⁻¹ * x)) = h • r F) ∧ ∀ (v : V), r (ι v) = v
**Lemma 6.11 (paper node, §6.3)**: a ramified simple faithful 2-torsion module over the tame image is an equivariant split summand of a regular module. The regular module `𝔽₂[C]^N` is `Fin N → C → ZMod 2` with the left-translation action written inline; `ι` is the equivariant embedding, `r` the equivariant retraction. The proof composes the odd-index relative trace `regular_summand_of_subgroup_summand` at a Sylow 2-subgroup (`Sylow.not_dvd_index` gives the odd index) composed with the weight-orbit kernel `sylow_split_pair_of_ramified` above. From this the deep-count multiplicativity (`Hom(V^∨, −)`-exactness) follows — `equivariant_lift_of_regular_summand` below — which is the sole remaining input to `lemma_6_17_dim`'s lower bound `#X₊ ≥ 2^m`. Applied at `V := V^∨` (also ramified simple faithful) by the consumer.
Lemma7.6
Group: Quadratic determinant obstructions (12)
Associated Lean declarations
-
GQ2.SectionSix.lemma_6_13_dihedral[complete] -
GQ2.SectionSix.lemma_6_13_evens[complete]
Lemma 6.13 of the paper (Universal two-point normalization and the index-two Evens norm).
Let
J=\langle s\rangle\cong C_2, \qquad E_2=\F_2e_1\oplus\F_2e_s, \qquad s(x_1,x_s)=(x_s,x_1),
and put
q_{\mathrm{hyp}}(x_1,x_s)=x_1x_s, \qquad f_J(x,y)=x_1y_s, \qquad m_1=0, \qquad m_s(y)=y_1y_s.
Then
\kappa_J((x,c),(y,d))=f_J(x,cy)+m_c(y)
is a normalized 2-cocycle on E_2\rtimes J. It restricts to the quadratic
map q_{\mathrm{hyp}} on E_2 and to zero on the zero section J. Its fibre
extension is the dihedral group D_8: the two coordinate lifts are
involutions, their commutator is the central involution, and their product has
square equal to that involution. Moreover
[\kappa_J]=N_{E_2}^{E_2\rtimes J,\mathrm{Ev}}(e_1^\vee) \quad\text{in }H^2(E_2\rtimes J,\F_2).
Now let N\triangleleft G have index 2, identify G/N with J, and let
\alpha\in Z^1(N,\F_2). Choose lifts \widetilde1=1 and
\widetilde s\in G, and define the normalized Shapiro cocycle
b(\gamma)_u= \alpha\!\left(\widetilde u^{-1}\gamma \widetilde{\bar\gamma^{-1}u}\right), \qquad u\in J.
This is the degree-one normalized Shapiro map (163). The graph pullback of (95) is
\nu_\alpha(\gamma,\eta) =b(\gamma)_1b(\eta)_{\bar\gamma^{-1}s} +\varepsilon(\bar\gamma)b(\eta)_1b(\eta)_s,
where \varepsilon(1)=0 and \varepsilon(s)=1. Its class is the index-two Evens norm:
[\nu_\alpha]=N_N^{G,\mathrm{Ev}}([\alpha])\in H^2(G,\F_2).
Equivalently, the normalization is
N_N^G(1+[\alpha]) =1+\operatorname{cor}_N^G[\alpha] +N_N^{G,\mathrm{Ev}}([\alpha]).
Finally, if g\in H is an involution, M=\F_2[H], J=\langle g\rangle,
and \pi:M\to\F_2[J] selects the coordinates indexed by 1 and g, then
for every right-coset transversal \mathcal R,
[\kappa_g^{\mathcal R}] =\operatorname{cor}_{M\rtimes J}^{M\rtimes H} (\pi\rtimes1)^*[\kappa_J].
Lean code for Lemma7.6●2 theorems
Associated Lean declarations
-
GQ2.SectionSix.lemma_6_13_dihedral[complete]
-
GQ2.SectionSix.lemma_6_13_evens[complete]
Associated Lean declarations
-
GQ2.SectionSix.lemma_6_13_dihedral[complete] -
GQ2.SectionSix.lemma_6_13_evens[complete]
-
theoremdefined in GQ2/SectionSix.leancomplete
theorem GQ2.SectionSix.lemma_6_13_dihedral : Nonempty (GQ2.SectionSix.twoPointExt ≃* DihedralGroup 4)
theorem GQ2.SectionSix.lemma_6_13_dihedral : Nonempty (GQ2.SectionSix.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.]
-
theoremdefined in GQ2/SectionSix.leancomplete
theorem GQ2.SectionSix.lemma_6_13_evens (sJ : GQ2.SectionSix.SemiProd (Multiplicative (ZMod 2)) GQ2.SectionSix.swapE) (hsJ : sJ = (0, Multiplicative.ofAdd 1)) (hUi : GQ2.SectionSix.SemiProd.fibre.index = 2) (hUo : IsOpen ↑GQ2.SectionSix.SemiProd.fibre) (hs : sJ ∉ GQ2.SectionSix.SemiProd.fibre) (htriv : ∀ (g : GQ2.SectionSix.SemiProd (Multiplicative (ZMod 2)) GQ2.SectionSix.swapE) (m : ZMod 2), g • m = m) (hα : ∀ (u v : ↥GQ2.SectionSix.SemiProd.fibre), GQ2.SectionSix.fibreCoord (u * v) = GQ2.SectionSix.fibreCoord u + GQ2.SectionSix.fibreCoord v) (hαc : Continuous GQ2.SectionSix.fibreCoord) : (GQ2.H2ofFun (GQ2.SectionSix.SemiProd (Multiplicative (ZMod 2)) GQ2.SectionSix.swapE) fun p => GQ2.kappa0 GQ2.SectionSix.twoPointDatum p.1 p.2) = GQ2.evensNormH2 htriv hUo hUi hs GQ2.SectionSix.fibreCoord hα hαc
theorem GQ2.SectionSix.lemma_6_13_evens (sJ : GQ2.SectionSix.SemiProd (Multiplicative (ZMod 2)) GQ2.SectionSix.swapE) (hsJ : sJ = (0, Multiplicative.ofAdd 1)) (hUi : GQ2.SectionSix.SemiProd.fibre.index = 2) (hUo : IsOpen ↑GQ2.SectionSix.SemiProd.fibre) (hs : sJ ∉ GQ2.SectionSix.SemiProd.fibre) (htriv : ∀ (g : GQ2.SectionSix.SemiProd (Multiplicative (ZMod 2)) GQ2.SectionSix.swapE) (m : ZMod 2), g • m = m) (hα : ∀ (u v : ↥GQ2.SectionSix.SemiProd.fibre), GQ2.SectionSix.fibreCoord (u * v) = GQ2.SectionSix.fibreCoord u + GQ2.SectionSix.fibreCoord v) (hαc : Continuous GQ2.SectionSix.fibreCoord) : (GQ2.H2ofFun (GQ2.SectionSix.SemiProd (Multiplicative (ZMod 2)) GQ2.SectionSix.swapE) fun p => GQ2.kappa0 GQ2.SectionSix.twoPointDatum p.1 p.2) = GQ2.evensNormH2 htriv hUo hUi hs GQ2.SectionSix.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.]
Lemma7.7
Group: Quadratic determinant obstructions (12)
Associated Lean declarations
-
GQ2.RepIndependence.lemma_6_14[complete]
Lemma 6.14 of the paper (Regular-module realization of the base local connecting map).
With notation as in Lemma 6.3, the base local determinant form
satisfies, for every x\in H^1(\Qtwo,V),
Q^0_{\mathrm{loc},q}(x)=Q^0_{\mathrm{loc},q_W}(i_*x).
Under Kummer theory and the normalized Shapiro cochain map, the right side is
obtained by applying the orbit operations of Lemma 7.8 to the
scalar Shapiro coordinates. Thus the regular-module computation evaluates the
actual base equivariant central class \kappa_q^0, including the m_c-terms;
it is not merely a polynomial with the same polarization.
Lean code for Lemma7.7●1 theorem
Associated Lean declarations
-
GQ2.RepIndependence.lemma_6_14[complete]
Associated Lean declarations
-
GQ2.RepIndependence.lemma_6_14[complete]
-
theoremdefined in GQ2/RepIndependence.leancomplete
theorem GQ2.RepIndependence.lemma_6_14 {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] {V : Type} [AddCommGroup V] [TopologicalSpace V] [DiscreteTopology V] [DistribMulAction GQ2.AbsGalQ2 V] [ContinuousSMul GQ2.AbsGalQ2 V] [DistribMulAction C V] {W : Type} [AddCommGroup W] [TopologicalSpace W] [DiscreteTopology W] [DistribMulAction GQ2.AbsGalQ2 W] [ContinuousSMul GQ2.AbsGalQ2 W] [DistribMulAction C W] (D : GQ2.TateDuality 2) (datW : GQ2.FactorSet C W) (ρ : GQ2.AbsGalQ2 →ₜ* C) (i : V →+ W) (hic : Continuous ⇑i) (hicompat : ∀ (g : GQ2.AbsGalQ2) (v : V), i (g • v) = g • i v) {q : W → ZMod 2} (hdatW : GQ2.IsEquivariantFactorSet q datW) (hiC : ∀ (c : C) (v : V), i (c • v) = c • i v) (hρW : ∀ (g : GQ2.AbsGalQ2) (w : W), g • w = ρ g • w) (x : GQ2.ContCoh.H1 GQ2.AbsGalQ2 V) : GQ2.SectionSix.Q0loc D (datW.comap i) ρ x = GQ2.SectionSix.Q0loc D datW ρ ((GQ2.ContCoh.mapCoeff1 i hic hicompat) x)
theorem GQ2.RepIndependence.lemma_6_14 {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] {V : Type} [AddCommGroup V] [TopologicalSpace V] [DiscreteTopology V] [DistribMulAction GQ2.AbsGalQ2 V] [ContinuousSMul GQ2.AbsGalQ2 V] [DistribMulAction C V] {W : Type} [AddCommGroup W] [TopologicalSpace W] [DiscreteTopology W] [DistribMulAction GQ2.AbsGalQ2 W] [ContinuousSMul GQ2.AbsGalQ2 W] [DistribMulAction C W] (D : GQ2.TateDuality 2) (datW : GQ2.FactorSet C W) (ρ : GQ2.AbsGalQ2 →ₜ* C) (i : V →+ W) (hic : Continuous ⇑i) (hicompat : ∀ (g : GQ2.AbsGalQ2) (v : V), i (g • v) = g • i v) {q : W → ZMod 2} (hdatW : GQ2.IsEquivariantFactorSet q datW) (hiC : ∀ (c : C) (v : V), i (c • v) = c • i v) (hρW : ∀ (g : GQ2.AbsGalQ2) (w : W), g • w = ρ g • w) (x : GQ2.ContCoh.H1 GQ2.AbsGalQ2 V) : GQ2.SectionSix.Q0loc D (datW.comap i) ρ x = GQ2.SectionSix.Q0loc D datW ρ ((GQ2.ContCoh.mapCoeff1 i hic hicompat) x)
**Lemma 6.14 (regular-module realization), eq. (102).** Amended (documented) with the compatibility hypotheses `Q⁰_loc` requires: `hdatW` (equivariant factor set on `W`), `hiC` (`i` a `C`-module map, eq. (77)'s `i ⋊ 1`), `hρW` (`G_ℚ₂` acts on `W` through `ρ`).
Lemma7.8
Group: Quadratic determinant obstructions (12)
Associated Lean declarations
-
GQ2.SectionSix.lemma_6_15_square[complete] -
GQ2.SectionSix.lemma_6_15_free[complete] -
GQ2.SectionSix.lemma_6_15_involution[complete] -
GQ2.ShapiroLedger.lemma_6_15_free_aux[complete] -
GQ2.ShapiroLedger.lemma_6_15_involution_aux[complete]
Lemma 6.15 of the paper (Quadratic orbit–stabilizer Shapiro).
Let W=\F_2[H]^N have coordinates X_{r,h} with H acting by left
translation on h. If K/F is the H-extension and
\alpha_r\in H^1(K,\F_2) is the scalar Shapiro coordinate, then the orbit
classes of Lemma 6.3 evaluate as follows. For g\in H, choose
any lift \widetilde g\in G_F and use the convention
(g\alpha_s)(n)=\alpha_s(\widetilde g^{-1}n\widetilde g) \qquad(n\in G_K).
This is independent of the chosen lift and is the convention fixed in (164):
S_r&longmapsto cor_{K/F}(alpha_r^2), C_{r,s,g}&longmapsto cor_{K/F}(alpha_rsmile galpha_s), E_{r,g}&longmapsto cor_{K_0/F}Evens_{K/K_0}(alpha_r), qquad K_0=K^{langle grangle}.
Lean code for Lemma7.8●5 theorems
Associated Lean declarations
-
GQ2.SectionSix.lemma_6_15_square[complete]
-
GQ2.SectionSix.lemma_6_15_free[complete]
-
GQ2.SectionSix.lemma_6_15_involution[complete]
-
GQ2.ShapiroLedger.lemma_6_15_free_aux[complete]
-
GQ2.ShapiroLedger.lemma_6_15_involution_aux[complete]
Associated Lean declarations
-
GQ2.SectionSix.lemma_6_15_square[complete] -
GQ2.SectionSix.lemma_6_15_free[complete] -
GQ2.SectionSix.lemma_6_15_involution[complete] -
GQ2.ShapiroLedger.lemma_6_15_free_aux[complete] -
GQ2.ShapiroLedger.lemma_6_15_involution_aux[complete]
-
theoremdefined in GQ2/SectionSix.leancomplete
theorem GQ2.SectionSix.lemma_6_15_square.{u_1} {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 → ∀ (α : ↥(GQ2.ContCoh.Z1 (↥N) (ZMod 2))), GQ2.H2ofFun G (GQ2.graphPullback (GQ2.squareOrbitDatum N) (⇑(QuotientGroup.mk' N)) (GQ2.Corestriction.shapiroFun N ↑α)) = GQ2.H2ofFun G (GQ2.Corestriction.cor2Fun N fun p => ↑α p.1 * ↑α p.2)
theorem GQ2.SectionSix.lemma_6_15_square.{u_1} {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 → ∀ (α : ↥(GQ2.ContCoh.Z1 (↥N) (ZMod 2))), GQ2.H2ofFun G (GQ2.graphPullback (GQ2.squareOrbitDatum N) (⇑(QuotientGroup.mk' N)) (GQ2.Corestriction.shapiroFun N ↑α)) = GQ2.H2ofFun G (GQ2.Corestriction.cor2Fun N fun p => ↑α 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.]
-
theoremdefined in GQ2/SectionSix.leancomplete
theorem GQ2.SectionSix.lemma_6_15_free.{u_1} {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) (α β : ↥(GQ2.ContCoh.Z1 (↥N) (ZMod 2))) (ghat : G) : GQ2.H2ofFun G (GQ2.graphPullback (GQ2.freeOrbitDatum N ((QuotientGroup.mk' N) ghat)) ⇑(QuotientGroup.mk' N) fun γ => (GQ2.Corestriction.shapiroFun N (↑α) γ, GQ2.Corestriction.shapiroFun N (↑β) γ)) = GQ2.H2ofFun G (GQ2.Corestriction.cor2Fun N fun p => ↑α p.1 * ↑β ⟨ghat⁻¹ * ↑p.2 * ghat, ⋯⟩)
theorem GQ2.SectionSix.lemma_6_15_free.{u_1} {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) (α β : ↥(GQ2.ContCoh.Z1 (↥N) (ZMod 2))) (ghat : G) : GQ2.H2ofFun G (GQ2.graphPullback (GQ2.freeOrbitDatum N ((QuotientGroup.mk' N) ghat)) ⇑(QuotientGroup.mk' N) fun γ => (GQ2.Corestriction.shapiroFun N (↑α) γ, GQ2.Corestriction.shapiroFun N (↑β) γ)) = GQ2.H2ofFun G (GQ2.Corestriction.cor2Fun N fun p => ↑α 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.]
-
theoremdefined in GQ2/SectionSix.leancomplete
theorem GQ2.SectionSix.lemma_6_15_involution.{u_1} {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) (α : ↥(GQ2.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₀) : GQ2.H2ofFun G (GQ2.graphPullback (GQ2.invOrbitDatum N ((QuotientGroup.mk' N) ghat)) (⇑(QuotientGroup.mk' N)) (GQ2.Corestriction.shapiroFun N ↑α)) = GQ2.H2ofFun G (GQ2.Corestriction.cor2Fun U₀ fun p => GQ2.evensNormFun (N.subgroupOf U₀) ⟨ghat, ⋯⟩ (fun u => ↑α ⟨↑↑u, ⋯⟩) (p.1, p.2))
theorem GQ2.SectionSix.lemma_6_15_involution.{u_1} {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) (α : ↥(GQ2.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₀) : GQ2.H2ofFun G (GQ2.graphPullback (GQ2.invOrbitDatum N ((QuotientGroup.mk' N) ghat)) (⇑(QuotientGroup.mk' N)) (GQ2.Corestriction.shapiroFun N ↑α)) = GQ2.H2ofFun G (GQ2.Corestriction.cor2Fun U₀ fun p => GQ2.evensNormFun (N.subgroupOf U₀) ⟨ghat, ⋯⟩ (fun 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.] -
theoremdefined in GQ2/Shapiro/Ledger/Free.leancomplete
theorem GQ2.ShapiroLedger.lemma_6_15_free_aux.{u_1} {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) (α β : ↥(GQ2.ContCoh.Z1 (↥N) (ZMod 2))) (ghat : G) : GQ2.H2ofFun G (GQ2.graphPullback (GQ2.freeOrbitDatum N ((QuotientGroup.mk' N) ghat)) ⇑(QuotientGroup.mk' N) fun γ => (GQ2.Corestriction.shapiroFun N (↑α) γ, GQ2.Corestriction.shapiroFun N (↑β) γ)) = GQ2.H2ofFun G (GQ2.Corestriction.cor2Fun N fun p => ↑α p.1 * ↑β ⟨ghat⁻¹ * ↑p.2 * ghat, ⋯⟩)
theorem GQ2.ShapiroLedger.lemma_6_15_free_aux.{u_1} {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) (α β : ↥(GQ2.ContCoh.Z1 (↥N) (ZMod 2))) (ghat : G) : GQ2.H2ofFun G (GQ2.graphPullback (GQ2.freeOrbitDatum N ((QuotientGroup.mk' N) ghat)) ⇑(QuotientGroup.mk' N) fun γ => (GQ2.Corestriction.shapiroFun N (↑α) γ, GQ2.Corestriction.shapiroFun N (↑β) γ)) = GQ2.H2ofFun G (GQ2.Corestriction.cor2Fun N fun p => ↑α p.1 * ↑β ⟨ghat⁻¹ * ↑p.2 * ghat, ⋯⟩)
**Lemma 6.15, free orbits (104)**: proved via the coboundary `δ¹Λ` with the explicit `Λ = freeLambda`. (the §§6–7 statement; the Shapiro-ledger proof, `Ax = ∅`.)
-
theoremdefined in GQ2/Shapiro/Ledger/Involution.leancomplete
theorem GQ2.ShapiroLedger.lemma_6_15_involution_aux.{u_1} {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) (α : ↥(GQ2.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₀) : GQ2.H2ofFun G (GQ2.graphPullback (GQ2.invOrbitDatum N ((QuotientGroup.mk' N) ghat)) (⇑(QuotientGroup.mk' N)) (GQ2.Corestriction.shapiroFun N ↑α)) = GQ2.H2ofFun G (GQ2.Corestriction.cor2Fun U₀ fun p => GQ2.evensNormFun (N.subgroupOf U₀) ⟨ghat, ⋯⟩ (fun u => ↑α ⟨↑↑u, ⋯⟩) (p.1, p.2))
theorem GQ2.ShapiroLedger.lemma_6_15_involution_aux.{u_1} {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) (α : ↥(GQ2.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₀) : GQ2.H2ofFun G (GQ2.graphPullback (GQ2.invOrbitDatum N ((QuotientGroup.mk' N) ghat)) (⇑(QuotientGroup.mk' N)) (GQ2.Corestriction.shapiroFun N ↑α)) = GQ2.H2ofFun G (GQ2.Corestriction.cor2Fun U₀ fun p => GQ2.evensNormFun (N.subgroupOf U₀) ⟨ghat, ⋯⟩ (fun u => ↑α ⟨↑↑u, ⋯⟩) (p.1, p.2))
**Lemma 6.15, involution orbits (105)** — the graph pullback of the involution orbit datum equals the corestriction of the index-two Evens norm, as `H2ofFun`-classes. Chains the compatible-transversal coboundary (`graphPullback_sub_cor2FunT_mem_B2`) with the transversal-change coboundary (`cor2FunT_sub_cor2Fun_mem_B2`).
Lemma7.9
Group: Quadratic determinant obstructions (12)
Associated Lean declarations
-
GQ2.SectionSix.lemma_6_16[complete]
Lemma 6.16 of the paper (Deep-unit Evens norm).
Let L/k be an unramified quadratic extension of finite dyadic local fields
and put e=v_k(2). Then
\Evens_{L/k}(\alpha)=0 \qquad(\alpha\in U_{e+1}(L)\subset L^\times/L^{\times2}).
Lean code for Lemma7.9●1 theorem
Associated Lean declarations
-
GQ2.SectionSix.lemma_6_16[complete]
Associated Lean declarations
-
GQ2.SectionSix.lemma_6_16[complete]
-
theoremdefined in GQ2/SectionSix.leancomplete
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, y ≠ 0 ∧ y ∈ k ∧ ‖x‖ = ‖y‖) (d : (↥k)ˣ) (δ : AlgebraicClosure ℚ_[2]) (hδ : δ ^ 2 = ↑↑d) (hδL : δ ∈ L) (hLδ : L.fixingSubgroup.subgroupOf k.fixingSubgroup = (MulAction.stabilizer (GQ2.Kummer.GaloisGroup ℚ_[2]) δ).subgroupOf k.fixingSubgroup) (A β : AlgebraicClosure ℚ_[2]) (hdeep : GQ2.SectionSix.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)), GQ2.Kummer.kummerCocycleFun β ↑(↑u * ↑v) = GQ2.Kummer.kummerCocycleFun β ↑↑u + GQ2.Kummer.kummerCocycleFun β ↑↑v) (hαc : Continuous fun u => GQ2.Kummer.kummerCocycleFun β ↑↑u) : GQ2.evensNormH2 htriv hUo hindex hs (fun u => GQ2.Kummer.kummerCocycleFun β ↑↑u) hα hαc = 0
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, y ≠ 0 ∧ y ∈ k ∧ ‖x‖ = ‖y‖) (d : (↥k)ˣ) (δ : AlgebraicClosure ℚ_[2]) (hδ : δ ^ 2 = ↑↑d) (hδL : δ ∈ L) (hLδ : L.fixingSubgroup.subgroupOf k.fixingSubgroup = (MulAction.stabilizer (GQ2.Kummer.GaloisGroup ℚ_[2]) δ).subgroupOf k.fixingSubgroup) (A β : AlgebraicClosure ℚ_[2]) (hdeep : GQ2.SectionSix.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)), GQ2.Kummer.kummerCocycleFun β ↑(↑u * ↑v) = GQ2.Kummer.kummerCocycleFun β ↑↑u + GQ2.Kummer.kummerCocycleFun β ↑↑v) (hαc : Continuous fun u => GQ2.Kummer.kummerCocycleFun β ↑↑u) : GQ2.evensNormH2 htriv hUo hindex hs (fun u => GQ2.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`.]
Proof for Lemma 7.9
Proof uses 3
Proved in §6 of the paper. Ingredients: Proposition 1.3 Proposition 1.6 Lemma 7.6.
Lemma7.10
Group: Quadratic determinant obstructions (12)
Associated Lean declarations
-
GQ2.DimAssembly.lemma_6_17_dim_of_hext_hduality[complete] -
GQ2.DimAssembly.lemma_6_17_dim_of_hduality[complete] -
GQ2.DimClose.lemma_6_17_dim_of_residueLift[complete] -
GQ2.ResidueLift.lemma_6_17_dim_final[complete] -
GQ2.VanishClose.lemma_6_17_vanish_final[complete]
Lemma 6.17 of the paper (The deep half is totally singular).
Assume V is ramified and put
X_+=\Hom_{H_V}(V^\vee,U_{e+1})\subset H^1(\Qtwo,V).
Then
\dim X_+=\frac12\dim H^1(\Qtwo,V), \qquad Q^0_{\mathrm{loc}}|_{X_+}=0.
Lean code for Lemma7.10●5 theorems
Associated Lean declarations
-
GQ2.DimAssembly.lemma_6_17_dim_of_hext_hduality[complete]
-
GQ2.DimAssembly.lemma_6_17_dim_of_hduality[complete]
-
GQ2.DimClose.lemma_6_17_dim_of_residueLift[complete]
-
GQ2.ResidueLift.lemma_6_17_dim_final[complete]
-
GQ2.VanishClose.lemma_6_17_vanish_final[complete]
Associated Lean declarations
-
GQ2.DimAssembly.lemma_6_17_dim_of_hext_hduality[complete] -
GQ2.DimAssembly.lemma_6_17_dim_of_hduality[complete] -
GQ2.DimClose.lemma_6_17_dim_of_residueLift[complete] -
GQ2.ResidueLift.lemma_6_17_dim_final[complete] -
GQ2.VanishClose.lemma_6_17_vanish_final[complete]
-
theoremdefined in GQ2/DimAssembly.leancomplete
theorem GQ2.DimAssembly.lemma_6_17_dim_of_hext_hduality {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] {V : Type} [AddCommGroup V] [TopologicalSpace V] [DiscreteTopology V] [Finite V] [DistribMulAction GQ2.AbsGalQ2 V] [ContinuousSMul GQ2.AbsGalQ2 V] [DistribMulAction C V] (B : GQ2.BoundaryMaps) (c : ↑GQ2.Ttame.toProfinite.toTop →ₜ* C) (hc : Function.Surjective ⇑c) (ρ : GQ2.AbsGalQ2 →ₜ* C) (hfac : ∀ (g : GQ2.AbsGalQ2), ρ g = c (B.tameF g)) (hρ : ∀ (g : GQ2.AbsGalQ2) (v : V), g • v = ρ g • v) (hV2 : ∀ (v : V), v + v = 0) (hfaith : ∀ (h : C), (∀ (v : V), h • v = v) → h = 1) (hsimple : ∀ (W : AddSubgroup V), (∀ (h : C), ∀ w ∈ W, h • w ∈ W) → W = ⊥ ∨ W = ⊤) (hram : ∃ v, c GQ2.tameTau • v ≠ v) [Finite (GQ2.ContCoh.H1 (↥ρ.ker) (ZMod 2))] (hext : GQ2.LocalKummer.FamiliesExtend ρ) (hduality : Nat.card ↥(GQ2.equivHoms C (V →+ ZMod 2) ↥(GQ2.deepClassesSubgroup ρ.ker)) = Nat.card ↥(GQ2.equivHoms C (V →+ ZMod 2) (GQ2.ContCoh.H1 (↥ρ.ker) (ZMod 2) ⧸ GQ2.deepClassesSubgroup ρ.ker))) : Nat.card ↑(GQ2.SectionSix.deepPart ρ) ^ 2 = Nat.card (GQ2.ContCoh.H1 GQ2.AbsGalQ2 V)
theorem GQ2.DimAssembly.lemma_6_17_dim_of_hext_hduality {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] {V : Type} [AddCommGroup V] [TopologicalSpace V] [DiscreteTopology V] [Finite V] [DistribMulAction GQ2.AbsGalQ2 V] [ContinuousSMul GQ2.AbsGalQ2 V] [DistribMulAction C V] (B : GQ2.BoundaryMaps) (c : ↑GQ2.Ttame.toProfinite.toTop →ₜ* C) (hc : Function.Surjective ⇑c) (ρ : GQ2.AbsGalQ2 →ₜ* C) (hfac : ∀ (g : GQ2.AbsGalQ2), ρ g = c (B.tameF g)) (hρ : ∀ (g : GQ2.AbsGalQ2) (v : V), g • v = ρ g • v) (hV2 : ∀ (v : V), v + v = 0) (hfaith : ∀ (h : C), (∀ (v : V), h • v = v) → h = 1) (hsimple : ∀ (W : AddSubgroup V), (∀ (h : C), ∀ w ∈ W, h • w ∈ W) → W = ⊥ ∨ W = ⊤) (hram : ∃ v, c GQ2.tameTau • v ≠ v) [Finite (GQ2.ContCoh.H1 (↥ρ.ker) (ZMod 2))] (hext : GQ2.LocalKummer.FamiliesExtend ρ) (hduality : Nat.card ↥(GQ2.equivHoms C (V →+ ZMod 2) ↥(GQ2.deepClassesSubgroup ρ.ker)) = Nat.card ↥(GQ2.equivHoms C (V →+ ZMod 2) (GQ2.ContCoh.H1 (↥ρ.ker) (ZMod 2) ⧸ GQ2.deepClassesSubgroup ρ.ker))) : Nat.card ↑(GQ2.SectionSix.deepPart ρ) ^ 2 = Nat.card (GQ2.ContCoh.H1 GQ2.AbsGalQ2 V)
**`lemma_6_17_dim`, parametric over `hext` and `hduality`** (the deep-part proof, increment 1): from `lemma_6_17_dim`'s own hypothesis set, discharge `hρsurj`/`hgen`/`hinf` (profinite plumbing + `inflationVanishes_ramifiedTame`) and the `V^∨` regular-summand package (`lemma_6_11_of_tame_pair` at `dualModule`, via the 𝔽₂-dual transport bricks), and apply the f6 capstone. The parameters are `hext` (`FamiliesExtend`) and `hduality` (the deep-part proof's result).
-
theoremdefined in GQ2/DimAssembly.leancomplete
theorem GQ2.DimAssembly.lemma_6_17_dim_of_hduality {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] {V : Type} [AddCommGroup V] [TopologicalSpace V] [DiscreteTopology V] [Finite V] [DistribMulAction GQ2.AbsGalQ2 V] [ContinuousSMul GQ2.AbsGalQ2 V] [DistribMulAction C V] (B : GQ2.BoundaryMaps) (c : ↑GQ2.Ttame.toProfinite.toTop →ₜ* C) (hc : Function.Surjective ⇑c) (ρ : GQ2.AbsGalQ2 →ₜ* C) (hfac : ∀ (g : GQ2.AbsGalQ2), ρ g = c (B.tameF g)) (hρ : ∀ (g : GQ2.AbsGalQ2) (v : V), g • v = ρ g • v) (hV2 : ∀ (v : V), v + v = 0) (hfaith : ∀ (h : C), (∀ (v : V), h • v = v) → h = 1) (hsimple : ∀ (W : AddSubgroup V), (∀ (h : C), ∀ w ∈ W, h • w ∈ W) → W = ⊥ ∨ W = ⊤) (hram : ∃ v, c GQ2.tameTau • v ≠ v) [Finite (GQ2.ContCoh.H1 (↥ρ.ker) (ZMod 2))] (hduality : Nat.card ↥(GQ2.equivHoms C (V →+ ZMod 2) ↥(GQ2.deepClassesSubgroup ρ.ker)) = Nat.card ↥(GQ2.equivHoms C (V →+ ZMod 2) (GQ2.ContCoh.H1 (↥ρ.ker) (ZMod 2) ⧸ GQ2.deepClassesSubgroup ρ.ker))) : Nat.card ↑(GQ2.SectionSix.deepPart ρ) ^ 2 = Nat.card (GQ2.ContCoh.H1 GQ2.AbsGalQ2 V)
theorem GQ2.DimAssembly.lemma_6_17_dim_of_hduality {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] {V : Type} [AddCommGroup V] [TopologicalSpace V] [DiscreteTopology V] [Finite V] [DistribMulAction GQ2.AbsGalQ2 V] [ContinuousSMul GQ2.AbsGalQ2 V] [DistribMulAction C V] (B : GQ2.BoundaryMaps) (c : ↑GQ2.Ttame.toProfinite.toTop →ₜ* C) (hc : Function.Surjective ⇑c) (ρ : GQ2.AbsGalQ2 →ₜ* C) (hfac : ∀ (g : GQ2.AbsGalQ2), ρ g = c (B.tameF g)) (hρ : ∀ (g : GQ2.AbsGalQ2) (v : V), g • v = ρ g • v) (hV2 : ∀ (v : V), v + v = 0) (hfaith : ∀ (h : C), (∀ (v : V), h • v = v) → h = 1) (hsimple : ∀ (W : AddSubgroup V), (∀ (h : C), ∀ w ∈ W, h • w ∈ W) → W = ⊥ ∨ W = ⊤) (hram : ∃ v, c GQ2.tameTau • v ≠ v) [Finite (GQ2.ContCoh.H1 (↥ρ.ker) (ZMod 2))] (hduality : Nat.card ↥(GQ2.equivHoms C (V →+ ZMod 2) ↥(GQ2.deepClassesSubgroup ρ.ker)) = Nat.card ↥(GQ2.equivHoms C (V →+ ZMod 2) (GQ2.ContCoh.H1 (↥ρ.ker) (ZMod 2) ⧸ GQ2.deepClassesSubgroup ρ.ker))) : Nat.card ↑(GQ2.SectionSix.deepPart ρ) ^ 2 = Nat.card (GQ2.ContCoh.H1 GQ2.AbsGalQ2 V)
**`lemma_6_17_dim`, parametric over `hduality` alone** (the deep-part proof, increment 2): the `hext` parameter of `lemma_6_17_dim_of_hext_hduality` is now **discharged** — the `V`-side regular-summand package (`lemma_6_11_of_tame_pair` at `V` itself, whose hypotheses are the theorem's own) feeds `ShapiroExtend.familiesExtend_of_package` (inverse Shapiro at the regular module + the retract transfer). The final parameter is the deep-part duality hypothesis `hduality`.
-
theoremdefined in GQ2/DimClose.leancomplete
theorem GQ2.DimClose.lemma_6_17_dim_of_residueLift {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] {V : Type} [AddCommGroup V] [TopologicalSpace V] [DiscreteTopology V] [Finite V] [DistribMulAction GQ2.AbsGalQ2 V] [ContinuousSMul GQ2.AbsGalQ2 V] [DistribMulAction C V] (B : GQ2.BoundaryMaps) (c : ↑GQ2.Ttame.toProfinite.toTop →ₜ* C) (hc : Function.Surjective ⇑c) (ρ : GQ2.AbsGalQ2 →ₜ* C) (hfac : ∀ (g : GQ2.AbsGalQ2), ρ g = c (B.tameF g)) (hρ : ∀ (g : GQ2.AbsGalQ2) (v : V), g • v = ρ g • v) (hV2 : ∀ (v : V), v + v = 0) (hfaith : ∀ (h : C), (∀ (v : V), h • v = v) → h = 1) (hsimple : ∀ (W : AddSubgroup V), (∀ (h : C), ∀ w ∈ W, h • w ∈ W) → W = ⊥ ∨ W = ⊤) (hram : ∃ v, c GQ2.tameTau • v ≠ v) (q : V → ZMod 2) (hq : GQ2.QuadraticFp2.IsQuadraticFp2 q) (hns : GQ2.QuadraticFp2.Nonsingular q) (hinv : GQ2.QuadraticFp2.IsInvariant C q) [Finite (GQ2.ContCoh.H1 (↥ρ.ker) (ZMod 2))] (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) [FiniteDimensional ℚ_[2] ↥k] (htriv : ∀ (g : ↥k.fixingSubgroup) (m : ZMod 2), g • m = m) (hker : ∀ (x : GQ2.Kummer.GaloisGroup ℚ_[2]), x ∈ ρ.ker ↔ x ∈ k.fixingSubgroup) (g₀ : GQ2.AbsGalQ2) (hg₀ : ρ g₀ = c GQ2.tameTau) (hg₀rt : GQ2.IsResidueTrivial ρ.ker g₀) : Nat.card ↑(GQ2.SectionSix.deepPart ρ) ^ 2 = Nat.card (GQ2.ContCoh.H1 GQ2.AbsGalQ2 V)
theorem GQ2.DimClose.lemma_6_17_dim_of_residueLift {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] {V : Type} [AddCommGroup V] [TopologicalSpace V] [DiscreteTopology V] [Finite V] [DistribMulAction GQ2.AbsGalQ2 V] [ContinuousSMul GQ2.AbsGalQ2 V] [DistribMulAction C V] (B : GQ2.BoundaryMaps) (c : ↑GQ2.Ttame.toProfinite.toTop →ₜ* C) (hc : Function.Surjective ⇑c) (ρ : GQ2.AbsGalQ2 →ₜ* C) (hfac : ∀ (g : GQ2.AbsGalQ2), ρ g = c (B.tameF g)) (hρ : ∀ (g : GQ2.AbsGalQ2) (v : V), g • v = ρ g • v) (hV2 : ∀ (v : V), v + v = 0) (hfaith : ∀ (h : C), (∀ (v : V), h • v = v) → h = 1) (hsimple : ∀ (W : AddSubgroup V), (∀ (h : C), ∀ w ∈ W, h • w ∈ W) → W = ⊥ ∨ W = ⊤) (hram : ∃ v, c GQ2.tameTau • v ≠ v) (q : V → ZMod 2) (hq : GQ2.QuadraticFp2.IsQuadraticFp2 q) (hns : GQ2.QuadraticFp2.Nonsingular q) (hinv : GQ2.QuadraticFp2.IsInvariant C q) [Finite (GQ2.ContCoh.H1 (↥ρ.ker) (ZMod 2))] (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) [FiniteDimensional ℚ_[2] ↥k] (htriv : ∀ (g : ↥k.fixingSubgroup) (m : ZMod 2), g • m = m) (hker : ∀ (x : GQ2.Kummer.GaloisGroup ℚ_[2]), x ∈ ρ.ker ↔ x ∈ k.fixingSubgroup) (g₀ : GQ2.AbsGalQ2) (hg₀ : ρ g₀ = c GQ2.tameTau) (hg₀rt : GQ2.IsResidueTrivial ρ.ker g₀) : Nat.card ↑(GQ2.SectionSix.deepPart ρ) ^ 2 = Nat.card (GQ2.ContCoh.H1 GQ2.AbsGalQ2 V)
**`lemma_6_17_dim`, reduced to the residue-trivial tame lift** (the deep-part proof finale): the §6.3 deep-half dimension identity `#X₊² = #H¹(ℚ₂, V)`, assembled from f7's `hduality_of_data` + f8's `lemma_6_17_dim_of_hduality`, with the single arithmetic input — a residue-trivial lift of tame inertia — threaded as a hypothesis, alongside the standard Galois-correspondence `k`-plumbing.
-
theoremdefined in GQ2/ResidueLift.leancomplete
theorem GQ2.ResidueLift.lemma_6_17_dim_final {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] {V : Type} [AddCommGroup V] [TopologicalSpace V] [DiscreteTopology V] [Finite V] [DistribMulAction GQ2.AbsGalQ2 V] [ContinuousSMul GQ2.AbsGalQ2 V] [DistribMulAction C V] (B : GQ2.BoundaryMaps) (c : ↑GQ2.Ttame.toProfinite.toTop →ₜ* C) (hc : Function.Surjective ⇑c) (ρ : GQ2.AbsGalQ2 →ₜ* C) (hfac : ∀ (g : GQ2.AbsGalQ2), ρ g = c (B.tameF g)) (hρ : ∀ (g : GQ2.AbsGalQ2) (v : V), g • v = ρ g • v) (hV2 : ∀ (v : V), v + v = 0) (hfaith : ∀ (h : C), (∀ (v : V), h • v = v) → h = 1) (hsimple : ∀ (W : AddSubgroup V), (∀ (h : C), ∀ w ∈ W, h • w ∈ W) → W = ⊥ ∨ W = ⊤) (hram : ∃ v, c GQ2.tameTau • v ≠ v) (q : V → ZMod 2) (hq : GQ2.QuadraticFp2.IsQuadraticFp2 q) (hns : GQ2.QuadraticFp2.Nonsingular q) (hinv : GQ2.QuadraticFp2.IsInvariant C q) : Nat.card ↑(GQ2.SectionSix.deepPart ρ) ^ 2 = Nat.card (GQ2.ContCoh.H1 GQ2.AbsGalQ2 V)
theorem GQ2.ResidueLift.lemma_6_17_dim_final {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] {V : Type} [AddCommGroup V] [TopologicalSpace V] [DiscreteTopology V] [Finite V] [DistribMulAction GQ2.AbsGalQ2 V] [ContinuousSMul GQ2.AbsGalQ2 V] [DistribMulAction C V] (B : GQ2.BoundaryMaps) (c : ↑GQ2.Ttame.toProfinite.toTop →ₜ* C) (hc : Function.Surjective ⇑c) (ρ : GQ2.AbsGalQ2 →ₜ* C) (hfac : ∀ (g : GQ2.AbsGalQ2), ρ g = c (B.tameF g)) (hρ : ∀ (g : GQ2.AbsGalQ2) (v : V), g • v = ρ g • v) (hV2 : ∀ (v : V), v + v = 0) (hfaith : ∀ (h : C), (∀ (v : V), h • v = v) → h = 1) (hsimple : ∀ (W : AddSubgroup V), (∀ (h : C), ∀ w ∈ W, h • w ∈ W) → W = ⊥ ∨ W = ⊤) (hram : ∃ v, c GQ2.tameTau • v ≠ v) (q : V → ZMod 2) (hq : GQ2.QuadraticFp2.IsQuadraticFp2 q) (hns : GQ2.QuadraticFp2.Nonsingular q) (hinv : GQ2.QuadraticFp2.IsInvariant C q) : Nat.card ↑(GQ2.SectionSix.deepPart ρ) ^ 2 = Nat.card (GQ2.ContCoh.H1 GQ2.AbsGalQ2 V)
**`lemma_6_17_dim`, closed** (the deep-part proof + the residue-lift derivation): the §6.3 deep-half dimension identity `#X₊² = #H¹(ℚ₂, V)`, from `SectionSix.lemma_6_17_dim`'s own hypothesis set plus only the finiteness instance `[Finite (H¹(ker ρ, 𝔽₂))]` (the local finiteness `H¹(G_K, 𝔽₂) ≅ K^×/2`, supplied by the B12/B13 interface). No new axiom: the residue-trivial tame lift is `exists_residueTrivial_tameLift`, and the splitting field with its Galois-correspondence data is `splitField`.
-
theoremdefined in GQ2/VanishClose.leancomplete
theorem GQ2.VanishClose.lemma_6_17_vanish_final {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] {V : Type} [AddCommGroup V] [TopologicalSpace V] [DiscreteTopology V] [Finite V] [DistribMulAction GQ2.AbsGalQ2 V] [ContinuousSMul GQ2.AbsGalQ2 V] [DistribMulAction C V] (D : GQ2.TateDuality 2) (R : GQ2.LocalReciprocity) (B : GQ2.BoundaryMaps) (c : ↑GQ2.Ttame.toProfinite.toTop →ₜ* C) (hc : Function.Surjective ⇑c) (ρ : GQ2.AbsGalQ2 →ₜ* C) (hfac : ∀ (g : GQ2.AbsGalQ2), ρ g = c (B.tameF g)) (horient : GQ2.TameUnitOrientation R B.tameF) (hρ : ∀ (g : GQ2.AbsGalQ2) (v : V), g • v = ρ g • v) (hV2 : ∀ (v : V), v + v = 0) (hfaith : ∀ (h : C), (∀ (v : V), h • v = v) → h = 1) (hsimple : ∀ (W : AddSubgroup V), (∀ (h : C), ∀ w ∈ W, h • w ∈ W) → W = ⊥ ∨ W = ⊤) (hram : ∃ v, c GQ2.tameTau • v ≠ v) (q : V → ZMod 2) (hq : GQ2.QuadraticFp2.IsQuadraticFp2 q) (hinv : GQ2.QuadraticFp2.IsInvariant C q) (dat : GQ2.FactorSet C V) (hdat : GQ2.IsEquivariantFactorSet q dat) (x : GQ2.ContCoh.H1 GQ2.AbsGalQ2 V) (hx : x ∈ GQ2.SectionSix.deepPart ρ) : GQ2.SectionSix.Q0loc D dat ρ x = 0
theorem GQ2.VanishClose.lemma_6_17_vanish_final {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] {V : Type} [AddCommGroup V] [TopologicalSpace V] [DiscreteTopology V] [Finite V] [DistribMulAction GQ2.AbsGalQ2 V] [ContinuousSMul GQ2.AbsGalQ2 V] [DistribMulAction C V] (D : GQ2.TateDuality 2) (R : GQ2.LocalReciprocity) (B : GQ2.BoundaryMaps) (c : ↑GQ2.Ttame.toProfinite.toTop →ₜ* C) (hc : Function.Surjective ⇑c) (ρ : GQ2.AbsGalQ2 →ₜ* C) (hfac : ∀ (g : GQ2.AbsGalQ2), ρ g = c (B.tameF g)) (horient : GQ2.TameUnitOrientation R B.tameF) (hρ : ∀ (g : GQ2.AbsGalQ2) (v : V), g • v = ρ g • v) (hV2 : ∀ (v : V), v + v = 0) (hfaith : ∀ (h : C), (∀ (v : V), h • v = v) → h = 1) (hsimple : ∀ (W : AddSubgroup V), (∀ (h : C), ∀ w ∈ W, h • w ∈ W) → W = ⊥ ∨ W = ⊤) (hram : ∃ v, c GQ2.tameTau • v ≠ v) (q : V → ZMod 2) (hq : GQ2.QuadraticFp2.IsQuadraticFp2 q) (hinv : GQ2.QuadraticFp2.IsInvariant C q) (dat : GQ2.FactorSet C V) (hdat : GQ2.IsEquivariantFactorSet q dat) (x : GQ2.ContCoh.H1 GQ2.AbsGalQ2 V) (hx : x ∈ GQ2.SectionSix.deepPart ρ) : GQ2.SectionSix.Q0loc D dat ρ x = 0
**`lemma_6_17_vanish`, closed downstream** (the Lemma 6.17 vanishing proof): the base connecting map `Q⁰loc` vanishes on the deep half, from `lemma_6_17_vanish`'s own hypotheses plus the reciprocity datum `(R, horient)` threaded per the c2c4 consumer note (the architecture review flag).
Proof for Lemma 7.10
Proof uses 5
Proved in §6 of the paper. Ingredients: Proposition 1.4 Proposition 1.9 Lemma 7.9 Lemma 7.5 Lemma 7.7.
Proposition7.11
Group: Quadratic determinant obstructions (12)
Associated Lean declarations
-
GQ2.DeepPart.card_Q0loc_zero_eq_of_dim_of_vanish[complete] -
GQ2.DetRamified.prop_6_18_ramified[complete] -
GQ2.UnramifiedModel.prop_6_18_unramified[complete]
Proposition 6.18 of the paper (Dyadic base determinant theorem).
If d=\dim V, then
\#(Q^0_{\mathrm{loc}})^{-1}(0)= \begin{cases} 2^{d-1}-2^{d/2-1},&V\text{ unramified},\\ 2^{d-1}+2^{d/2-1},&V\text{ ramified}. \end{cases}
Equivalently, the base local Gauss sum is negative in the unramified case and
positive in the ramified case. The candidate base form Q_A^0 has the same
Gauss sum by Proposition 7.4.
Lean code for Proposition7.11●3 theorems
Associated Lean declarations
-
GQ2.DeepPart.card_Q0loc_zero_eq_of_dim_of_vanish[complete]
-
GQ2.DetRamified.prop_6_18_ramified[complete]
-
GQ2.UnramifiedModel.prop_6_18_unramified[complete]
Associated Lean declarations
-
GQ2.DeepPart.card_Q0loc_zero_eq_of_dim_of_vanish[complete] -
GQ2.DetRamified.prop_6_18_ramified[complete] -
GQ2.UnramifiedModel.prop_6_18_unramified[complete]
-
theoremdefined in GQ2/DeepPart/Q0locLayer.leancomplete
theorem GQ2.DeepPart.card_Q0loc_zero_eq_of_dim_of_vanish {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] {V : Type} [AddCommGroup V] [TopologicalSpace V] [DiscreteTopology V] [Finite V] [DistribMulAction GQ2.AbsGalQ2 V] [ContinuousSMul GQ2.AbsGalQ2 V] [DistribMulAction C V] (D : GQ2.TateDuality 2) (q : V → ZMod 2) (hq : GQ2.QuadraticFp2.IsQuadraticFp2 q) (hns : GQ2.QuadraticFp2.Nonsingular q) (dat : GQ2.FactorSet C V) (hdat : GQ2.IsEquivariantFactorSet q dat) (ρ : GQ2.AbsGalQ2 →ₜ* C) (hρ : ∀ (g : GQ2.AbsGalQ2) (v : V), g • v = ρ g • v) (hρsurj : Function.Surjective ⇑ρ) (hsimple : ∀ (W : AddSubgroup V), (∀ (h : C), ∀ w ∈ W, h • w ∈ W) → W = ⊥ ∨ W = ⊤) (h₀ : C) (hmoves : ∃ v, h₀ • v ≠ v) (hinv : ∀ (c : C) (v : V), q (c • v) = q v) (hV2 : ∀ (v : V), v + v = 0) (hdim : Nat.card ↑(GQ2.SectionSix.deepPart ρ) ^ 2 = Nat.card (GQ2.ContCoh.H1 GQ2.AbsGalQ2 V)) (hvanish : ∀ x ∈ GQ2.SectionSix.deepPart ρ, GQ2.SectionSix.Q0loc D dat ρ x = 0) (m : ℕ) (hm : 1 ≤ m) (hcard : Nat.card V = 2 ^ (2 * m)) : Nat.card { x // GQ2.SectionSix.Q0loc D dat ρ x = 0 } = 2 ^ (2 * m - 1) + 2 ^ (m - 1)
theorem GQ2.DeepPart.card_Q0loc_zero_eq_of_dim_of_vanish {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] {V : Type} [AddCommGroup V] [TopologicalSpace V] [DiscreteTopology V] [Finite V] [DistribMulAction GQ2.AbsGalQ2 V] [ContinuousSMul GQ2.AbsGalQ2 V] [DistribMulAction C V] (D : GQ2.TateDuality 2) (q : V → ZMod 2) (hq : GQ2.QuadraticFp2.IsQuadraticFp2 q) (hns : GQ2.QuadraticFp2.Nonsingular q) (dat : GQ2.FactorSet C V) (hdat : GQ2.IsEquivariantFactorSet q dat) (ρ : GQ2.AbsGalQ2 →ₜ* C) (hρ : ∀ (g : GQ2.AbsGalQ2) (v : V), g • v = ρ g • v) (hρsurj : Function.Surjective ⇑ρ) (hsimple : ∀ (W : AddSubgroup V), (∀ (h : C), ∀ w ∈ W, h • w ∈ W) → W = ⊥ ∨ W = ⊤) (h₀ : C) (hmoves : ∃ v, h₀ • v ≠ v) (hinv : ∀ (c : C) (v : V), q (c • v) = q v) (hV2 : ∀ (v : V), v + v = 0) (hdim : Nat.card ↑(GQ2.SectionSix.deepPart ρ) ^ 2 = Nat.card (GQ2.ContCoh.H1 GQ2.AbsGalQ2 V)) (hvanish : ∀ x ∈ GQ2.SectionSix.deepPart ρ, GQ2.SectionSix.Q0loc D dat ρ x = 0) (m : ℕ) (hm : 1 ≤ m) (hcard : Nat.card V = 2 ^ (2 * m)) : Nat.card { x // GQ2.SectionSix.Q0loc D dat ρ x = 0 } = 2 ^ (2 * m - 1) + 2 ^ (m - 1)
**Prop 6.18 (eq. (115), ramified) from Lemma 6.17**: given the dim clause (`hdim`, `#X₊² = #H¹`) and the vanishing clause (`hvanish`, `Q⁰_loc|X₊ = 0`), the zero-count of `Q⁰_loc` is `2^{2m−1} + 2^{m−1}` — the positive Gauss sign, via the Lagrangian Arf package (`arf_zero_of_card_sq`) and the Euler-characteristic count. Ax: **B6** (via `D`), **B7**. -
theoremdefined in GQ2/DetRamified.leancomplete
theorem GQ2.DetRamified.prop_6_18_ramified {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] {V : Type} [AddCommGroup V] [TopologicalSpace V] [DiscreteTopology V] [Finite V] [DistribMulAction GQ2.AbsGalQ2 V] [ContinuousSMul GQ2.AbsGalQ2 V] [DistribMulAction C V] (D : GQ2.TateDuality 2) (R : GQ2.LocalReciprocity) (B : GQ2.BoundaryMaps) (c : ↑GQ2.Ttame.toProfinite.toTop →ₜ* C) (hc : Function.Surjective ⇑c) (ρ : GQ2.AbsGalQ2 →ₜ* C) (hfac : ∀ (g : GQ2.AbsGalQ2), ρ g = c (B.tameF g)) (horient : GQ2.TameUnitOrientation R B.tameF) (hρ : ∀ (g : GQ2.AbsGalQ2) (v : V), g • v = ρ g • v) (hfaith : ∀ (h : C), (∀ (v : V), h • v = v) → h = 1) (hsimple : ∀ (W : AddSubgroup V), (∀ (h : C), ∀ w ∈ W, h • w ∈ W) → W = ⊥ ∨ W = ⊤) (hram : ∃ v, c GQ2.tameTau • v ≠ v) (q : V → ZMod 2) (hq : GQ2.QuadraticFp2.IsQuadraticFp2 q) (hns : GQ2.QuadraticFp2.Nonsingular q) (hinv : GQ2.QuadraticFp2.IsInvariant C q) (dat : GQ2.FactorSet C V) (hdat : GQ2.IsEquivariantFactorSet q dat) (m : ℕ) (hm : 1 ≤ m) (hcard : Nat.card V = 2 ^ (2 * m)) : Nat.card { x // GQ2.SectionSix.Q0loc D dat ρ x = 0 } = 2 ^ (2 * m - 1) + 2 ^ (m - 1)
theorem GQ2.DetRamified.prop_6_18_ramified {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] {V : Type} [AddCommGroup V] [TopologicalSpace V] [DiscreteTopology V] [Finite V] [DistribMulAction GQ2.AbsGalQ2 V] [ContinuousSMul GQ2.AbsGalQ2 V] [DistribMulAction C V] (D : GQ2.TateDuality 2) (R : GQ2.LocalReciprocity) (B : GQ2.BoundaryMaps) (c : ↑GQ2.Ttame.toProfinite.toTop →ₜ* C) (hc : Function.Surjective ⇑c) (ρ : GQ2.AbsGalQ2 →ₜ* C) (hfac : ∀ (g : GQ2.AbsGalQ2), ρ g = c (B.tameF g)) (horient : GQ2.TameUnitOrientation R B.tameF) (hρ : ∀ (g : GQ2.AbsGalQ2) (v : V), g • v = ρ g • v) (hfaith : ∀ (h : C), (∀ (v : V), h • v = v) → h = 1) (hsimple : ∀ (W : AddSubgroup V), (∀ (h : C), ∀ w ∈ W, h • w ∈ W) → W = ⊥ ∨ W = ⊤) (hram : ∃ v, c GQ2.tameTau • v ≠ v) (q : V → ZMod 2) (hq : GQ2.QuadraticFp2.IsQuadraticFp2 q) (hns : GQ2.QuadraticFp2.Nonsingular q) (hinv : GQ2.QuadraticFp2.IsInvariant C q) (dat : GQ2.FactorSet C V) (hdat : GQ2.IsEquivariantFactorSet q dat) (m : ℕ) (hm : 1 ≤ m) (hcard : Nat.card V = 2 ^ (2 * m)) : Nat.card { x // GQ2.SectionSix.Q0loc D dat ρ x = 0 } = 2 ^ (2 * m - 1) + 2 ^ (m - 1)
**Proposition 6.18 (dyadic base determinant theorem), eq. (115), ramified case** — wired downstream (the deep-part proof/f2d statement-move): the local base determinant form has the positive Gauss sign, `#(Q⁰_loc)⁻¹(0) = 2^{2m−1} + 2^{m−1}` (`#V = 2^{2m}`). With Prop 6.9 this is Corollary 6.19(iv): the two sources have equal base Gauss sums. Proved from the two §6.3 Kummer cores now that both are proved downstream: `ResidueLift.lemma_6_17_dim_final` (`#X₊² = #H¹`) and `VanishClose.lemma_6_17_vanish_final` (`Q⁰_loc|X₊ = 0`), fed to the banked Lagrangian-Arf count `card_Q0loc_zero_eq_of_dim_of_vanish`. Amended (the architecture review flag) with `(R, horient)` — the reciprocity datum `lemma_6_17_vanish_final` requires; consumers discharge it at the boundary-maps witness. -
theoremdefined in GQ2/UnramifiedModel.leancomplete
theorem GQ2.UnramifiedModel.prop_6_18_unramified {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] {V : Type} [AddCommGroup V] [TopologicalSpace V] [DiscreteTopology V] [Finite V] [DistribMulAction GQ2.AbsGalQ2 V] [ContinuousSMul GQ2.AbsGalQ2 V] [DistribMulAction C V] (D : GQ2.TateDuality 2) (B : GQ2.BoundaryMaps) (c : ↑GQ2.Ttame.toProfinite.toTop →ₜ* C) (hc : Function.Surjective ⇑c) (ρ : GQ2.AbsGalQ2 →ₜ* C) (hfac : ∀ (g : GQ2.AbsGalQ2), ρ g = c (B.tameF g)) (hρ : ∀ (g : GQ2.AbsGalQ2) (v : V), g • v = ρ g • v) (hfaith : ∀ (h : C), (∀ (v : V), h • v = v) → h = 1) (hsimple : ∀ (W : AddSubgroup V), (∀ (h : C), ∀ w ∈ W, h • w ∈ W) → W = ⊥ ∨ W = ⊤) (hV : ∃ v, v ≠ 0) (hunram : ∀ (v : V), c GQ2.tameTau • v = v) (q : V → ZMod 2) (hq : GQ2.QuadraticFp2.IsQuadraticFp2 q) (hns : GQ2.QuadraticFp2.Nonsingular q) (hinv : GQ2.QuadraticFp2.IsInvariant C q) (dat : GQ2.FactorSet C V) (hdat : GQ2.IsEquivariantFactorSet q dat) (m : ℕ) (hm : 1 ≤ m) (hcard : Nat.card V = 2 ^ (2 * m)) : Nat.card { x // GQ2.SectionSix.Q0loc D dat ρ x = 0 } = 2 ^ (2 * m - 1) - 2 ^ (m - 1)
theorem GQ2.UnramifiedModel.prop_6_18_unramified {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] {V : Type} [AddCommGroup V] [TopologicalSpace V] [DiscreteTopology V] [Finite V] [DistribMulAction GQ2.AbsGalQ2 V] [ContinuousSMul GQ2.AbsGalQ2 V] [DistribMulAction C V] (D : GQ2.TateDuality 2) (B : GQ2.BoundaryMaps) (c : ↑GQ2.Ttame.toProfinite.toTop →ₜ* C) (hc : Function.Surjective ⇑c) (ρ : GQ2.AbsGalQ2 →ₜ* C) (hfac : ∀ (g : GQ2.AbsGalQ2), ρ g = c (B.tameF g)) (hρ : ∀ (g : GQ2.AbsGalQ2) (v : V), g • v = ρ g • v) (hfaith : ∀ (h : C), (∀ (v : V), h • v = v) → h = 1) (hsimple : ∀ (W : AddSubgroup V), (∀ (h : C), ∀ w ∈ W, h • w ∈ W) → W = ⊥ ∨ W = ⊤) (hV : ∃ v, v ≠ 0) (hunram : ∀ (v : V), c GQ2.tameTau • v = v) (q : V → ZMod 2) (hq : GQ2.QuadraticFp2.IsQuadraticFp2 q) (hns : GQ2.QuadraticFp2.Nonsingular q) (hinv : GQ2.QuadraticFp2.IsInvariant C q) (dat : GQ2.FactorSet C V) (hdat : GQ2.IsEquivariantFactorSet q dat) (m : ℕ) (hm : 1 ≤ m) (hcard : Nat.card V = 2 ^ (2 * m)) : Nat.card { x // GQ2.SectionSix.Q0loc D dat ρ x = 0 } = 2 ^ (2 * m - 1) - 2 ^ (m - 1)
**Proposition 6.18, eq. (115), unramified case**: negative Gauss sign, `#(Q⁰_loc)⁻¹(0) = 2^{2m−1} − 2^{m−1}`. Proved via the Hermitian-line model (see the file docstring): identify `V` with `𝔽_{2^{2m}}`, transport `Q⁰_loc` to a norm-one-invariant nonsingular form, and count zeros with `card_normOne_invariant_form_zero`. [the §§6–7 statement; proof the deep-part proof, Ax: B6, B7.] **Signature note:** the hypothesis `hc : Function.Surjective ⇑c` (as in `prop_6_18_ramified`).
Proof for Proposition 7.11
Proof uses 2
Proved in §6 of the paper. Ingredients: Lemma 7.10 Lemma 7.2.
Lemma7.12
Group: Quadratic determinant obstructions (12)
Associated Lean declarations
-
GQ2.SectionSix.lemma_6_21[complete]
Lemma 6.21 of the paper (Determinant transgression relative to the fixed equivariant class).
Let q be a nonsingular C-invariant quadratic form on V, and assume that
a zero-section-normalized equivariant class
\kappa_q^0\in H^2(V\rtimes C,\F_2)
restricting to q on V has been fixed. Let
1\to V\to G_\eta\to C\to1
have extension class \eta\in H^2(C,V). Relative to the fixed equivariant
lift \kappa_q^0, the obstruction to extending the fibre class over G_\eta is
d_2(q)=b_q^\flat{}_*\eta\in H^2(C,V^\vee).
Consequently, if q is the restriction of an actual class in
H^2(G_\eta,\F_2), then \eta=0 and G_\eta\cong V\rtimes C over C.
Lean code for Lemma7.12●1 theorem
Associated Lean declarations
-
GQ2.SectionSix.lemma_6_21[complete]
Associated Lean declarations
-
GQ2.SectionSix.lemma_6_21[complete]
-
theoremdefined in GQ2/SectionSix.leancomplete
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 : GQ2.QuadraticFp2.IsQuadraticFp2 q) (hns : GQ2.QuadraticFp2.Nonsingular q) (dat : GQ2.FactorSet C V) (hdat : GQ2.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, ∀ (cc : C), p (s cc) = cc
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 : GQ2.QuadraticFp2.IsQuadraticFp2 q) (hns : GQ2.QuadraticFp2.Nonsingular q) (dat : GQ2.FactorSet C V) (hdat : GQ2.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, ∀ (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.]
Lemma7.13
Group: Quadratic determinant obstructions (12)
Associated Lean declarations
-
GQ2.SectionSix.lemma_6_22[complete]
Lemma 6.22 of the paper (Marking-preserving shear of the difference data).
Let a\in Z^1(C,V) and define
s_a(v,c)=(v+a(c),c).
If
\kappa=\kappa_q^0+\Gamma_\gamma+\operatorname{inf}\delta, then, in cohomology,
s_a^*\kappa= \kappa_q^0+ \Gamma_{\gamma+b_q^\flat a}+ \operatorname{inf}\bigl(\delta+ \Theta_q^0(a)+\gamma\smile a\bigr),
where
\Theta_q^0(a)=(a,\id_C)^*\kappa_q^0\in Z^2(C,\F_2)
and
(\gamma\smile a)(c,d)=\gamma(c)(c a(d)).
In particular, if q\ne0, a unique cohomology class a kills the edge
\gamma, and the scalar phase then becomes
\delta+\Theta_q^0(a)+\gamma\smile a.
Lean code for Lemma7.13●1 theorem
Associated Lean declarations
-
GQ2.SectionSix.lemma_6_22[complete]
Associated Lean declarations
-
GQ2.SectionSix.lemma_6_22[complete]
-
theoremdefined in GQ2/SectionSix.leancomplete
theorem GQ2.SectionSix.lemma_6_22 {C : Type} [Group C] {V : Type} [AddCommGroup V] [DistribMulAction C V] (q : V → ZMod 2) (hq : GQ2.QuadraticFp2.IsQuadraticFp2 q) (dat : GQ2.FactorSet C V) (hdat : GQ2.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, ∀ (p q' : V × C), GQ2.kappa0 dat (GQ2.SectionSix.shear a p) (GQ2.SectionSix.shear a q') + GQ2.SectionSix.gammaEdge γ (GQ2.SectionSix.shear a p) (GQ2.SectionSix.shear a q') + GQ2.SectionSix.inflScalar δ (GQ2.SectionSix.shear a p) (GQ2.SectionSix.shear a q') = GQ2.kappa0 dat p q' + GQ2.SectionSix.gammaEdge (fun c => γ c + AddMonoidHom.mk' (GQ2.QuadraticFp2.polar q (a c)) ⋯) p q' + GQ2.SectionSix.inflScalar (fun cd => δ cd + GQ2.SectionSix.thetaPhase dat a cd + GQ2.SectionSix.gammaCupA γ a cd) p q' + (w (p.1 + p.2 • q'.1, p.2 * q'.2) + w p + w q')
theorem GQ2.SectionSix.lemma_6_22 {C : Type} [Group C] {V : Type} [AddCommGroup V] [DistribMulAction C V] (q : V → ZMod 2) (hq : GQ2.QuadraticFp2.IsQuadraticFp2 q) (dat : GQ2.FactorSet C V) (hdat : GQ2.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, ∀ (p q' : V × C), GQ2.kappa0 dat (GQ2.SectionSix.shear a p) (GQ2.SectionSix.shear a q') + GQ2.SectionSix.gammaEdge γ (GQ2.SectionSix.shear a p) (GQ2.SectionSix.shear a q') + GQ2.SectionSix.inflScalar δ (GQ2.SectionSix.shear a p) (GQ2.SectionSix.shear a q') = GQ2.kappa0 dat p q' + GQ2.SectionSix.gammaEdge (fun c => γ c + AddMonoidHom.mk' (GQ2.QuadraticFp2.polar q (a c)) ⋯) p q' + GQ2.SectionSix.inflScalar (fun cd => δ cd + GQ2.SectionSix.thetaPhase dat a cd + GQ2.SectionSix.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.]