Ramified Arf value (Lemma 6.8 (87)): arf q = s via the ⟨T⟩ route

The ramified Arf value is computed without the Hermitian model, involution, or norm-one group: tame inertia ⟨T⟩ itself acts diagonally on V ≅ W^{⊕s} (the isotypic decomposition), freely on V ∖ 0 (T fixes only 0 in the simple faithful W), preserving q. Feeding GaussSigns.arf_eq_of_free with U = ⟨T⟩ and n = ord(T) — using ord(T) ∣ 2^{2m'} − 1 (T a unit of the field 𝔽₂[T] ≅ 𝔽_{2^f}) and ord(T) ∤ 2^{m'} − 1 (irreducible_operator_pow_ne_one) — pins arf q = s.

Reuses the tame representation-theory proof (GQ2/TameSimple.lean): IsSimpleModTwo.

No sorry.

The field-order lemma: an irreducible operator is a unit of 𝔽₂[T] ≅ 𝔽_{2^f}

theorem GQ2.GaussSigns.irreducible_operator_pow_card_sub_one {W : Type u_1} [AddCommGroup W] [Module (ZMod 2) W] [FiniteDimensional (ZMod 2) W] (m : ℕ) (hdim : Module.finrank (ZMod 2) W = 2 * m) (T : Module.End (ZMod 2) W) (hV : Nontrivial W) (hirr : ∀ (U : Submodule (ZMod 2) W), U ≠ ⊥ → U ≠ ⊤ → ∃ w ∈ U, T w ∉ U) : T ^ (2 ^ (2 * m) - 1) = 1

An irreducible 𝔽₂-operator on a 2m-dimensional space has T^{2^{2m} − 1} = 1: T is a nonzero element of the field 𝔽₂[T] ≅ AdjoinRoot(minpoly T) ≅ 𝔽_{2^{2m}}, so T^{#field − 1} = 1. Hence ord(T) ∣ 2^{2m} − 1.

Lemma 6.8 (87): arf q = s via the ⟨T⟩ route

theorem GQ2.GaussSigns.arf_eq_s_ramified {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 : FoxH.IsSimpleModTwo G W) : (∀ (v : V), v + v = 0) → ∀ (hW2 : ∀ (w : W), w + w = 0) (q : V → ZMod 2) (hq : QuadraticFp2.IsQuadraticFp2 q) (hns : 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), 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.

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

• Lemma 6.8 = ⟦lem-ramifiedhermitian⟧