Lemma 5.14 (mixed Hessian), normal forms, and the main duality #
Split off from GQ2.FoxHeisenberg, building on GQ2.FoxHeisenberg.WildRow. This file provides:
- Lemma 5.14, the mixed Hessian in the split case via
agHom/lgHomnaturality (section HessianRow), including the shared fixed-point-free surjectivity helpersurjective_smul_sub_of_fixedPointFree; - the Heisenberg normal forms (
section NormalForms); - the main duality conclusion (
section MainDuality).
See GQ2.FoxHeisenberg for the umbrella module docstring.
Lemma 5.14: the mixed Hessian (split case) via agHom/lgHom naturality #
The .a and .l coordinates of the Heisenberg-evaluated aux words come free from the WordLift
wild-row results: agHom/lgHom are homs pushing heisMarking to liftMarking (over V, resp.
V^∨), so (heisMarking t x y).W.a = (liftMarking t x).W.u and .l = (liftMarking t y).W.u. On
the x₀-supported rep (x₁ = x₃ = 0 slots) these vanish for every aux word, leaving a pure central
computation.
The degree-one tuple supported on the x₀-slot (display (53)'s normal form).
Equations
- GQ2.FoxH.x0Supported c = ![0, 0, c, 0]
Instances For
Naturality: the .a of an aux word at heisMarking is the liftMarking .u (via agHom);
.l is the dual liftMarking .u (via lgHom); .g agrees (both project the base).
On the x₀-supported rep, σ (index 0) lands in the base slice, so σ₂ and g₀ are pure base
elements: their .a, .l, .z all vanish (via secHom-slice + the square for z).
Base-triviality of the Heisenberg aux words (transferred from liftMarking). #
g₀ = σ₂² is a base-slice element on the x₀-supported rep (a = l = z = 0). #
h₀ ↦ λ(c) (Lemma 5.14, the h₀-shadow central contribution): on the x₀-supported rep the
central coordinate of the wild h₀ word is λ(c). With g₀ in the base slice, φ = conj by g₀
preserves all Heisenberg coordinates, so in the class-two peel
h₀ = φ(x₀)·x₀·φ(d₀)·d₀·d₀²·[φ(d₀),d₀]
every factor but the leading φ(x₀)·x₀ cross-term vanishes (d₀.a = d₀.l = 0; the paired z's
cancel in char 2), leaving φ(x₀).l(x₀.a) = λ(c).
[d₀,z₀] ↦ 0 in the split case: c₀'s central coordinate vanishes since d₀.a = d₀.l = 0
(the paper's P + 1 = 0 collapse for T = 1).
u₁ is a base-slice element on the x₀-rep, so its central coordinate vanishes.
x₁^σ is a base-slice element on the x₀-rep, so its central coordinate vanishes.
The split mixed pairing, wild summand: B_{ρ,A}(x₀-supported) central coordinate is λ(c).
Outer peel of wildValue = h₀·u₁⁻¹·x₁^σ·c₀: all four factors are trivially-based with vanishing
.a (naturality/base-slice), so .z is additive, and only h₀.z = λ(c) survives (u₁⁻¹, x₁^σ, c₀
have .z = 0).
Ramified mixed Hessian: U = σ₂ acts nontrivially #
The ramified degree-one pairing B(c,λ) = λ((1 + U + U⁻¹)c). Two central contributions:
h₀ ↦ λ(c) (the shadow, with all U²-twisted cross-terms cancelling in char 2) and
[d₀,z₀] ↦ λ(Uc) + λ(U⁻¹c) (the symplectic commutator, now nonzero since Dd₀ = c ≠ 0). Unlike
the split case g₀ = σ₂² is not g-slice, so the peel uses conjP_*_of_slice to track the
U-action.
Fixed-point-freeness makes σ − 1 surjective on a finite module: if σ • v = v forces
v = 0 then v ↦ σ • v − v is injective (difference-telescope), hence surjective on the
finite V. The canonical form of the hand-rolled hsurj/hτsurj derivations.
Contragredient fixed-point-freeness: if T = τ has no nonzero fixed vector on the finite
module V (V^T = 0), then the same holds on the dual V^∨. (T − 1 injective ⟹ surjective on
finite V; the dual T^∨ − 1 is then injective.) Supplies the ramified d₀.l = λ computation.
h₀ ↦ λ(c) (ramified Lemma 5.14). Unlike the split case, g₀ = σ₂² acts nontrivially
(U²), so the conjugation φ = ·^{g₀} shifts the A/A^∨ coordinates by U⁻²; but every
Heisenberg base still acts trivially on V (the conjugation cancels U²), so the class-two peel is
a mul_z_of_trivial computation whose U²-twisted cross-terms cancel in char 2, leaving λ(c).
[d₀,z₀] ↦ λ(Uc) + λ(U⁻¹c) (ramified Lemma 5.14, U = σ₂). On the x₀-rep Dd₀ = c and
Dz₀ = U⁻¹c; the Heisenberg commutator symplectic form commP_z_of_trivial gives
[d₀,z₀].z = d₀.l(z₀.a) + z₀.l(d₀.a) = λ(U⁻¹c) + (U⁻¹λ)(c) = λ(U⁻¹c) + λ(Uc).
The ramified mixed pairing, wild summand: wildValue.z = λ((1 + U + U⁻¹)c). The peel
wildValue = h₀·u₁⁻¹·(x₁^σ)·c₀: u₁⁻¹ and x₁^σ are pure secHom base elements
(a = l = z = 0),
so right-multiplication by them preserves .z; only h₀.z = λ(c) and c₀.z = λ(Uc) + λ(U⁻¹c)
survive.
The marked wild generators act trivially on a simple module — the admissibility input the
normal-form and pairing lemmas below need. This is the paper's Lemma 5.12 ("simple char-2 modules
are tame") applied to the normal 2-subgroup L = ⟨⟨x₀, x₁⟩⟩: L is normal (a normal closure) and
a 2-group (the Pro2Core clause hcore), and contains x₀, x₁.
The tame row in the split case, closed form (unconditional — needs only T = 1 and char
2, no wild-core input): L_t(x) = S⁻¹·x₁. This is the x 1 = 0 half of lemma_5_13_split's
Z¹ description, and holds verbatim from the general tame row d1Fun_tame with T = 1.
The B¹ coboundary shape when the wild generators act trivially (the paper's B¹ in
Lemma 5.13(i), with the trivial wild action made an explicit hypothesis — however it is obtained:
directly, or via the proved lemma_5_12 from Pro2Core; see
docs/orchestration/p13-normal-form-hypothesis-gap.md). Under T = 1 and x₀, x₁ acting trivially, every
coboundary d⁰v is supported on the σ-slot: B¹ = {((S−1)v, 0, 0, 0)}.
On classes supported away from the σ, τ slots (x 0 = x 1 = 0, y 0 = y 1 = 0), the tame
relator value lies in the base slice secHom '' C (all its σ, τ inputs do), so its central
coordinate vanishes. Hence the mixedB pairing on the x₀-supported normal forms is carried
entirely by the wild relator — the split/ramified Hessian is a pure wild-relator computation.
Lemma 5.13, split case (i), cocycle shape: if T = 1 (trivial τ-action on a
nontrivial simple module), Z¹ = {(a, 0, c, 0)} and B¹ = {((S−1)v, 0, 0, 0)}.
Hypotheses (per docs/orchestration/p13-normal-form-hypothesis-gap.md): hcore supplies trivial wild action
(wild_acts_trivially); hVS is V^S = 0, i.e. 1 + S⁻¹ invertible — it excludes the trivial
module 𝔽₂ (where 1 + S⁻¹ = 0 and the x 3 = 0 clause would fail; that module is handled
separately in prop_5_15). hU is the σ-tameness (σ₂ = U acts trivially). Both hVS and hU
are derivable in the split case — with τ, x₀, x₁ acting trivially the C-action factors through
the cyclic ⟨σ̄⟩, so a nontrivial simple V is a simple 𝔽₂[⟨σ⟩]-module: V^S = V^C = 0 and σ
has odd order (⇒ σ₂ = 1). Those derivations need t.Generates and simple-cyclic rep theory, so
they are factored out as hypotheses here, keeping the normal-form proof pure finite-Fox calculus.
See docs/orchestration/p13-normal-form-hypothesis-gap.md §7.
Proved (the §5 proof layer): B¹ half from b1w_split_shape; Z¹ half from the tame row d1Fun_tame_split
(= S⁻¹·x₁) and the wild row liftMarking_wildValue_u (= x₁ + (1+S⁻¹)·x₃), with x 1 = 0 from
S⁻¹ injective and x 3 = 0 from hVS.
Lemma 5.13, ramified case (ii), unique normal form: if V^T = 0, every degree-one
class has a unique representative supported on x₀ (display (53)).
Hypothesis hcore supplies trivial wild action (wild_acts_trivially); the ramified condition
V^T = 0 (htau) gives 1 + T invertible.
Hypothesis hTodd: τ's 2-primary part powOmega2 t.τ acts
trivially on V, i.e. τ acts with odd order on V. This is the ramified analogue of the
split case's hU : ∀ v, t.sigma2 • v = v (sigma2 = powOmega2 t.σ), and is the arithmetic fact
that τ = tame inertia is prime-to-2, so acts through an odd quotient on the 𝔽₂-module V.
It is required (not implied by V^T = 0, which admits even-order fixed-point-free actions):
the wild-row aux offset (powOmega2 p).u is a geometric sum whose length is the ω₂-exponent,
and it collapses to 0 (via the P = 0 norm ledger WordLift.norm_eq_zero_of_fixedPointFree)
exactly because the odd action-period divides that length. Like hU/hVS in the split case,
this is factored out as an explicit hypothesis, supplied by the simple-factor analysis.
See docs/orchestration/p13-normal-form-hypothesis-gap.md for the counterexample and rationale.
Signature note: the trivial wild action is taken as hypotheses
hx0/hx1 rather than derived from (hsimple, hcore) via wild_acts_trivially — so the lemma
applies to the contragredient dual A∨ (whose wild-triviality transfers from A's) without a
"dual of simple is simple" detour, mirroring the split-side split_shapes_of_wild.
No hU hypothesis is needed: the σ-tameness ∀ v, σ₂ • v = v is not derivable from
admissibility (S₃ on its 2-dim simple module and C₅⋊C₄ on 𝔽₁₆, markings x₀=x₁=1,
are admissible ramified counterexamples), and it is not needed: the h₀-row x₂-cancellation
happens in g₀-conjugate pairs (liftMarking_h0_u_ramified, via conjP_u_of_base_trivial).
Lemma 5.13, pairing display (54), split case: on x₀-supported representatives the
degree-one pairing is (c, λ) ↦ λ(c) when T = 1.
The proof uses the mixed Hessian ledger, Lemma 5.14 — h₀ ↦ λ(c) via
classTwoIdentity [needs g₀ = σ₂² trivial, i.e. hU], and the [d₀,z₀] term vanishes since
P + 1 = 0 in char 2 for T = 1. hsimple/hcore give the trivial wild action
(wild_acts_trivially); hU is the σ-tameness (derivable in split; see lemma_5_13_split).
Lemma 5.13, pairing display (54), ramified case: when V^T = 0 the pairing on
x₀-supported representatives is (c, λ) ↦ λ((1 + U + U⁻¹)c) for U = S₂^ω
(Marking.sigma2).
The tame relator's central coordinate vanishes on the x₀-supported rep
(heisMarking_tameValue_z_eq_zero), so the pairing is carried entirely by the wild relator
(heisMarking_wildValue_z_ramified): h₀ ↦ λ(c) (the shadow) plus the [d₀,z₀] symplectic term
λ(Uc) + λ(U⁻¹c) (nonzero here because Dd₀ = c ≠ 0, unlike the split P + 1 = 0 collapse).
Hypothesis hTodd (added the §5 proof layer, mirroring the §5 proof layer's lemma_5_13_ramified): τ's 2-primary part
acts trivially on V (tame inertia is prime-to-2), needed for the ramified Dd₀ = c via the
P = 0 ledger. Supplied per simple factor by the tame representation-theory proof. The trivial wild action is taken as
hypotheses hx0/hx1 (the Prop. 5.15 proof signature note on lemma_5_13_ramified).