Gauss signs: assembly layer for Lemma 6.8 / Proposition 6.9 #
Proof-side bricks for the Gauss-sign pair (§6.2), stated below GQ2/SectionSix.lean in the
public import order (this file must not import SectionSix, which will consume it — the Shapiro-ledger proof cycle
lesson). Everything here is abstract over the acting group / the isometry; the SectionSix
splices instantiate U := powOmega2 (c tameSigma) and G := Hf.
arf_qDouble_eq_zero— the final clause of Lemma 6.8 from (87) + (88): ifarf q = sand the rank exponentkof1 + Uhask ≡ s (mod 2), thenarf (q_U) = 0. This consumes the now-proved Wall sign (gaussSum_qDouble, the Wall and Gauss-count proof).zeroCount_qDouble_of_arf_zero— the ramified count of Proposition 6.9 fromarf (q_U) = 0: the doubling of a nonsingular form by a 2-power isometry is nonsingular (qDouble_nonsingular), so the engine'szeroCount_of_arf_zeroevaluates#(q_U)⁻¹(0).central_two_pow_smul_eq_one— a central element of 2-power order acting on a nontrivial faithful simple exponent-2 module is trivial (its fixed space is a nonzero submodule byexists_fixed_ne_zero). This is the source of the oddness of tame images in both branches of 6.8/6.9 (the paper's "cyclic 2-group acting in characteristic 2 has nonzero fixed vectors" step).
No sorry in this file.
The cyclic-operator crux #
For the unramified branch we need the arithmetic input #Hf ∤ 2^m − 1 (equivalently, the
generator is not contained in the proper subfield 𝔽_{2^m}). The heart of it, stated for a
single 𝔽₂-linear operator, is: an irreducible operator on a 2m-dimensional 𝔽₂-space
cannot satisfy T^(2^m − 1) = 1. Proof: minpoly T is irreducible (no proper invariant
subspace) of degree 2m (the cyclic bridge finrank = natDegree), yet T^(2^m−1) = 1 forces
minpoly T ∣ X^{2^m} − X, so its degree divides m — impossible for m ≥ 1.
The minimal polynomial of an irreducible operator is irreducible.
For an irreducible operator, finrank = natDegree (minpoly) (the cyclic bridge): the map
p ↦ aeval T p v for a nonzero v is a surjection 𝔽₂[X] ↠ V with kernel (minpoly T).
The cyclic-operator crux of the Gauss-sign proof (U2): an irreducible 𝔽₂-operator on a
2m-dimensional space (m ≥ 1) cannot satisfy T^(2^m − 1) = 1.
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.)
The ramified count of Proposition 6.9 from arf (q_U) = 0: the doubling is
nonsingular, and a nonsingular form of trivial Arf invariant on 2^(2m) points has
2^(2m−1) + 2^(m−1) zeros.
The Arf pinch (unramified 6.9, arithmetic half): if both the nonzero zeros and the
nonzeros of a nonsingular q on 2^(2m) points come in packets of size n (as they do for
the free action of an invariance group of odd order n), then arf q = 0 would force
n ∣ 2^m − 1; so if that is excluded, arf q = 1. (The two candidate zero counts
2^(2m−1) ± 2^(m−1) differ from the divisibility constraints by exactly 2^m ∓ 1.)
Free-action orbit divisibility #
The arithmetic pinch is fed by a group U acting on V, freely on V ∖ 0, preserving q —
this is the norm-one group of the endomorphism field in the paper's unramified proof. A free
action of a finite group has all orbits of size #U, so #U divides the cardinality of any
U-stable subset.
A free action of a finite group divides the cardinality of the set acted on: every orbit is equivalent to the group.
A U-stable subtype inherits the free-action divisibility.
Free-action zero-count divisibilities: a finite group acting on V (#V = 2^(2m))
fixing 0, preserving q, and freely on V ∖ 0, divides both zeroCount q − 1 (nonzero zeros)
and 2^(2m) − zeroCount q (nonzeros). (Factored from prop_6_9_unramified_of_free.)
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.
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).
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).
The ramified Arf-parity engine (Lemma 6.8 (87), Hermitian-model-free) #
For the ramified branch, arf q = s (mod 2) is forced by the same free-action machinery run
with a dual pinch: a norm-one group of order 2^{m'} + 1 (m' = f/2) acting diagonally on
V ≅ W^{⊕s} gives orbit-divisibilities, and 2^{m'}+1 divides 2^{m'·s} − 1 iff s is even
and 2^{m'·s} + 1 iff s is odd — pinning arf q to the parity of s with no Hermitian
diagonalization.
2^{m'·s} ≡ (−1)^s modulo 2^{m'}+1.
If s is odd then 2^{m'}+1 ∤ 2^{m'·s} − 1 (for m' ≥ 1).
If s is even then 2^{m'}+1 ∤ 2^{m'·s} + 1 (for m' ≥ 1).
The dual Arf pinch: free-action packets of size n with n ∤ 2^m + 1 force arf q = 0
(mirror of arf_eq_one_of_dvd; the arf = 1 branch would give n ∣ 2^m + 1).
The norm-one Arf-parity engine (Lemma 6.8 (87), Hermitian-model-free): if a finite group
U of order 2^{m'} + 1 acts on V (#V = 2^{2·m'·s}, m' ≥ 1, s ≥ 1) fixing 0,
preserving a nonsingular q, and freely on V ∖ 0, then arf q = s (mod 2).
In the ramified application U is the norm-one group of the endomorphism field D = End_I(W)
acting diagonally on V ≅ W^{⊕s}; the parity of s decides which of the two Arf pinches fires.
The general Arf-parity engine (any group generating past the middle subfield) #
Generalizing arf_eq_of_free_norm_one: the acting group need not have order exactly 2^{m'}+1.
It suffices that #U ∣ 2^{2m'} − 1, #U ∤ 2^{m'} − 1, and #U > 2 — i.e. #U "generates past
the subfield 𝔽_{2^{m'}}". This lets the invariance group ⟨T⟩ (tame inertia) itself serve as
U in the ramified proof, so the endomorphism-field involution and norm-one subgroup are not
needed: T acts irreducibly on W (dim 2m' = f), so ord(T) ∤ 2^{m'} − 1
(irreducible_operator_pow_ne_one) and ord(T) ∣ 2^{2m'} − 1 (T a unit of the field 𝔽₂[T]).
With g := (2 : ZMod n)^{m'} satisfying g² = 1 and g ≠ 1, an odd s gives
n ∤ 2^{m'·s} − 1.
With (2 : ZMod n)^{2m'} = 1 and n > 2, an even s gives n ∤ 2^{m'·s} + 1.
The general Arf-parity engine: a finite group U acting on V (#V = 2^{2·m'·s},
m' ≥ 1, s ≥ 1) fixing 0, preserving nonsingular q, freely on V ∖ 0, with
#U ∣ 2^{2m'} − 1, #U ∤ 2^{m'} − 1, #U > 2, forces arf q = s (mod 2).
A central element of 2-power order acts trivially on a nontrivial faithful simple
exponent-2 module: its fixed space is nonzero (exists_fixed_ne_zero) and a submodule (by
centrality), hence everything by simplicity, hence the element is 1 by faithfulness.
Paper-tag ledger (auto-generated by paperforge; do not edit) #
- Lemma 6.8 = ⟦lem-ramifiedhermitian⟧
- Proposition 6.9 = ⟦prop-candidatezero⟧