The ramified isotypic pack and descent count #
The pack interface, self-reciprocity, semilinear descent, and the final fixed-point count.
See GQ2.RamifiedPack for the paper-facing overview, source citations, and deviations.
§PackInterface: the ⟨t⟩-module structure on Wt := AdjoinRoot P #
The pack-facing layer (design doc §0's field shapes): the Subgroup.zpowers t-action on
D := AdjoinRoot P by root-multiplication (rootAction, through the choice-exponent hom
zpowHom : ⟨t⟩ →* Dˣ — well-defined because root P ^ orderOf t = 1), the char-2 field
hWt2 (adjoinRoot_add_self), simplicity hWtsimple (isSimpleModTwo_rootAction: a
t-stable additive subgroup of D = 𝔽₂[root P] is a D-subspace of the line), and the
pack-shaped equivariance he (equiv_zpowers_smul, upgrading exists_isotypic_equiv's
per-coordinate root-equivariance).
Char 2 on AdjoinRoot P: every element is 2-torsion (the hWt2 pack field).
Every element of ⟨t⟩ is a ℕ-power of t (finite order: reduce the ℤ-exponent
mod orderOf t).
The choice exponent of an element of ⟨t⟩: (σ : C) = t ^ powExp t hpos σ.
Equations
- GQ2.RamifiedPack.powExp t hpos σ = ⋯.choose
Instances For
root P ^ orderOf t = 1 from P ∣ X^{orderOf t} − 1 (via AdjoinRoot.mk_eq_zero).
ℕ-power upgrade of exists_isotypic_equiv's per-coordinate root-equivariance.
The root is nonzero (else 0 = root^{orderOf t} = 1).
The root as a unit of the field AdjoinRoot P.
Equations
- GQ2.RamifiedPack.rootUnit t P hpos hdvd = Units.mk0 (AdjoinRoot.root P) ⋯
Instances For
Well-definedness core: equal t-powers give equal rootUnit-powers
(orderOf rootUnit ∣ orderOf t, then pow_eq_pow_iff_modEq both ways).
The ⟨t⟩ →* Dˣ hom t^k ↦ root^k (choice-exponent; well-defined by
rootUnit_pow_congr).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The ⟨t⟩-module structure on Wt := AdjoinRoot P (the pack instance argument):
t^k acts as multiplication by root P ^ k. Consumers letI it.
Equations
- GQ2.RamifiedPack.rootAction t P hpos hdvd = DistribMulAction.compHom (AdjoinRoot P) (GQ2.RamifiedPack.zpowHom t P hpos hdvd)
Instances For
Computation rule for rootAction at a ℕ-power presentation of σ.
The generator acts as root-multiplication.
Wt is a simple ⟨t⟩-module (the hWtsimple pack field): a t-stable additive
subgroup of D = 𝔽₂[root P] is stable under multiplication by every mk P g, hence a
D-subspace of the line D — so ⊥ or ⊤.
The pack-shaped equivariance he: the per-coordinate root-equivariance of
exists_isotypic_equiv upgrades to full ⟨t⟩-equivariance for the rootAction
module structure on Wt — prop_6_9_ramified's he field verbatim.
§SelfReciprocity: f = deg P is EVEN (design doc §4) #
The nonsingular t-invariant polar pairing makes the t̂-adjoint t̂⁻¹, so P(t̂) = 0
forces P(t̂⁻¹) = 0 (A); transported through the isotypic equivalence this says x⁻¹ is a
root of P in D = 𝔽₂[x], x := root P (B); the induced 𝔽₂-algebra involution
x ↦ x⁻¹ of D is a genuine order-2 element of Aut(D/𝔽₂) (nontrivial since x ≠ 1 —
the ramified exclusion of P = X + 1), and #Aut(D/𝔽₂) = f (finite fields are Galois:
GaloisField.instIsGaloisOfFinite), so Lagrange gives 2 ∣ f (C). The numerology
f = 2^a·r, a ≥ 1, r odd then feeds the pack's hWcard shape.
Invariance of q under t extends to all powers.
The adjoint shift: for g preserving q, the polar pairing trades g on the left
for g⁻¹ on the right.
(A) the operator-adjoint identity: B(P(t̂)w, v) = B(w, P(t̂⁻¹)v) for the polar
pairing of a t-invariant quadratic map.
(A) closed: P(t̂) = 0 forces P(t̂⁻¹) = 0 (nonsingularity kills the orthogonal
complement of everything).
Generalized ℕ-power transport (any group element acting per-coordinate as a fixed scalar).
(B) transport to D: P(t̂⁻¹) = 0 on V ≅ D^s (s ≥ 1) evaluates, on the
first basis vector, to P(x⁻¹) = 0 in D.
(C) f is even: the involution x ↦ x⁻¹ of D = AdjoinRoot P (an 𝔽₂-algebra
automorphism since x⁻¹ is again a root of P) has order 2 in Aut(D/𝔽₂) when x ≠ 1,
and finite fields are Galois, so 2 ∣ #Aut = finrank = natDegree P.
The pack numerology: an even nonzero f is 2^a · r with a ≥ 1 and r odd.
§UKill: U^{2^a} = 1 for U := powOmega2 s (design doc §5, common first step) #
The 2-primary part U = s^{ω₂} of s, raised to 2^a, centralizes t — the twist exponent
2^{ω·2^a} is ≡ 1 (mod orderOf t) because f = deg P ∣ ω·2^a (via f ∣ orderOf s from the
Frobenius order on D, and r ∣ ω from the ω₂ ≡ 0-on-odd-part congruence) and
orderOf t ∣ 2^f − 1 (Lagrange in Dˣ). Commuting with both generators makes U^{2^a}
central; its fixed space is then a nonzero C-submodule (the 2-group fixed-point count), so
simplicity + faithfulness kill it.
Iterating the tame twist: (s^n)⁻¹ t s^n = t^{2^n}.
Equal t-powers pin equal root-powers (evaluate the isotypic equivalence on the first
basis vector).
Equal root-powers pin equal t-powers (via faithfulness through the equivalence).
With a faithful action, the root has the same order as t.
AdjoinRoot P of a monic polynomial over 𝔽₂ is finite.
The Frobenius square map as an 𝔽₂-algebra endomorphism of AdjoinRoot P
(hand-rolled: char 2 makes squaring additive via adjoinRoot_add_self).
Equations
- GQ2.RamifiedPack.frobAlg P = { toFun := fun (y : AdjoinRoot P) => y ^ 2, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }
Instances For
The Frobenius as an algebra automorphism (injective self-map of a finite field).
Equations
- GQ2.RamifiedPack.frobEquiv P hmon = AlgEquiv.ofBijective (GQ2.RamifiedPack.frobAlg P) ⋯
Instances For
The Frobenius has order exactly f = deg P in Aut(D/𝔽₂): Lagrange bounds it by f
(#Aut = f, Galois), and φ^m = 1 makes all 2^f elements roots of X^{2^m} − X, so
f ≤ m.
A Frobenius power fixing the root fixes everything (AdjoinRoot.algHom_ext).
f = deg P divides any m with x^{2^m} = x (Frobenius order pinning).
Lagrange in Dˣ: orderOf t ∣ 2^f − 1.
U^{2^a} = 1 (design doc §5, the centrality kill): the 2^a-th power of the
2-primary part U = powOmega2 s centralizes both generators, so its (nonzero) fixed space
is a C-submodule; simplicity and faithfulness force U^{2^a} = 1.
§DescentKit: the D-side inputs of the descent count (design doc §5, Route A) #
For the twist σ := frobEquiv^ω (order 2^a, since gcd(ω, f) = r for odd ω with
r ∣ ω): the fixed field F := fixedField ⟨σ⟩ has exactly 2^r elements (Artin's lemma
finrank_fixedField_eq_card + the card tower), and the vector-valued Dedekind/Artin
independence engine — a family annihilated by all twisted evaluations Σᵢ σⁱ(y)•wᵢ = 0
vanishes — which powers both halves of the dim_F V^U = s argument in §5b-ii.
Vector-valued Artin independence: if the powers σ⁰, …, σ^{m−1} are pairwise
distinct and ∑ i, σⁱ(y) • wᵢ = 0 for every scalar y, then every wᵢ = 0.
(Minimal-support descent: a second nonzero index is killed by the μ-twist difference
system; a single nonzero index dies at y = 1.)
The twist frobEquiv^ω has order exactly 2^a when ω is odd with r ∣ ω
(gcd(f, ω) = r at f = 2^a·r).
Membership in the fixed field of ⟨σ⟩ is fixedness under σ itself.
The fixed field of the twist has 2^r elements: [D : F] = #⟨σ⟩ = 2^a (Artin) and
#D = #F^{[D:F]} pin #F = 2^r at f = 2^a·r.
§DescentCount: #(fixed points of a σ-semilinear automorphism of D^n) = #F^n #
The abstract Route-A descent (design doc §5): for β : AddAut (D^n) that is σ-semilinear
(β(y•w) = σ(y)•β(w)) with β^{2^a} = 1 and σ of order 2^a, the fixed set of β is an
F-form of D^n — F-independent fixed vectors are D-independent (Dedekind shortening) and
the fixed set D-spans (the trace projector through the artin_vector engine on the quotient) —
so #Fix(β) = #F^n.
Distinct powers of σ below its order.
The ↥F-scalar bridge on D^n: the subfield scalar acts as its coercion.
The fixed set of β as an ↥F-submodule of D^n (F := fixedField ⟨σ⟩):
σ-fixed scalars pass through β.
Equations
- GQ2.RamifiedPack.fixedSubmodule P σ β hσpos hsemi = { carrier := {w : Fin n → AdjoinRoot P | β w = w}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
Instances For
The Dedekind shortening: F-independent β-fixed vectors are D-independent.
The fixed set D-spans (the trace projector through the artin_vector engine on the
quotient): every vector lies in the D-span of the β-fixed set.
The descent count: the fixed points of a σ-semilinear automorphism of D^n of
order dividing 2^a = orderOf σ number exactly #F^n.
Semilinearity follows from the root case (additive + polynomial bootstrap).
§VUCount: the pack hVU — #V^U = 2^{r·sV} (design doc §5, assembled) #
The pack hVU: at a faithful simple isotypic ramified tame action, the fixed
vectors of U := powOmega2 s number exactly 2^{r·sV} — the σ-semilinear descent count
transported through the isotypic equivalence.