Lemma 5.4/5.5: the finite Fox derivatives of the wild aux words (tame case) #
Split off from GQ2.FoxHeisenberg, building on GQ2.FoxHeisenberg.Traced. At a tame lower map
(the wild inertia x₀, x₁ and, in the split case, σ₂ acting trivially) the ω₂-powers in the
auxiliary words collapse to their offsets, so the first Fox derivatives become plain
𝔽₂-combinations of the lift offsets, mirroring the paper's Lemma 5.4 ledger.
See GQ2.FoxHeisenberg for the umbrella module docstring.
Lemma 5.4/5.5: the finite Fox derivatives of the wild aux words (tame case) #
At a tame lower map (the wild inertia x₀, x₁ and, in the split case, σ₂ acting trivially), the
ω₂-powers in the auxiliary words collapse to their offsets via WordLift.powOmega2_u_of_trivial,
so the first Fox derivatives D(·) become plain 𝔽₂-combinations of the lift offsets x. These
mirror the paper's Lemma 5.4 ledger D(uᵢ) = P(Dxᵢ + Dτ), D(d₀) = Pb + (P+1)c at P = 1.
D(u₀) = x₂ + x₁ (tame case): with x₀, τ acting trivially the ω₂-power in
u₀ = (x₀τ)^{ω₂} collapses (odd exponent, char 2), leaving the plain product offset.
D(u₁) = x₃ + x₁ (tame case), the x₁-analogue of liftMarking_u0_u.
Ramified (V^T = 0) aux-word offsets #
In the ramified case τ acts non-trivially, but its 2-primary part is trivial (hTodd), so the
ω₂-power bases u0 = (x₀τ)^{ω₂}, u1 = (x₁τ)^{ω₂} still act trivially on V (their base is the
2-part of the τ-action) while their offsets vanish (powOmega2_u_of_oddFixedPointFree). Thus
every wild aux word remains trivially-based (so the split .u-additivity toolkit applies), only the
u0/u1 offsets change to 0.
Ramified base-g triviality: u0's base acts trivially on V (it is powOmega2 (t.x₀ t.τ),
whose action is τ's 2-part, killed by hTodd).
Ramified base-g triviality: u1's base acts trivially on V.
Ramified D(u₀) = 0 (the ω₂-norm of the fixed-point-free τ-base vanishes).
Ramified D(u₁) = 0.
D(d₀) = x₁ (tame case, P = 1): from d₀ = u₀·x₀⁻¹, D(d₀) = D(u₀) − x₂ = (x₂+x₁) − x₂ = x₁. This is the paper's Dd₀ = Pb + (P+1)c = b at the split value P = 1 (c-terms cancel).
σ₂'s base is exactly t.sigma2 — the ω₂-exponent taken in WordLift V C agrees
with the one in C (Lemma 5.1, finite-exponent independence): orderOf t.σ ∣ orderOf σ_WL, so
powOmega2_pow_eq identifies the two representatives. Hence the σ-tameness hU (stated on
t.sigma2) transfers to the wild-row evaluation — hU v gives (liftMarking t x).sigma2.g • v = v
after rw [liftMarking_sigma2_g].
D(x₁^σ) = S⁻¹·x₃ (tame case): conjugating by σ shifts the x₁-offset by t.σ⁻¹, and
the x₀-offsets contributed by the two σ's cancel. This is the sole surviving S⁻¹ in the wild
row
(the paper's xσ₁ ledger row 0 0 0 S⁻¹).
Base-triviality of the wild aux words (tame case) #
Each aux word evaluates to a trivially-based element, so .u-additivity (mul_u_of_trivial etc.)
applies. g₀ = σ₂² and z₀ = x₀^{σ₂} use σ-tameness hU; the rest use the wild-core
triviality.
D(h₀) = 0 (tame case): the paper's h₀-shadow (Lemma 5.3(i)). With every base acting
trivially, .u is additive, so D(h₀) = D(x₀^{g₀}) + D(x₀) + D(d_g) + D(d₀) + D(d₀²) + D([d_g,d₀]) = x₂ + x₂ + x₁ + x₁ + 0 + 0 = 0 (conjugates keep the offset, d₀² and the commutator vanish).
D(c₀) = 0 (tame case): c₀ = [d₀,z₀] is a commutator of trivially-based elements.
The split wild row (Lemma 5.5): L_w = D(h₀) + D(u₁⁻¹) + D(x₁^σ) + D(c₀) = 0 + (x₃+x₁) + S⁻¹·x₃ + 0 = x₁ + (1 + S⁻¹)·x₃. This is (d1Fun t x).2 at a split (T = 1) simple
tame module — the wild half of lemma_5_13_split's Z¹ characterisation.
Ramified wild row: L_w = S⁻¹·d #
With u0.u = u1.u = 0 (collapse) and every aux base trivial, the ramified aux offsets are
d0.u = x₂ (vs x₁ split), h0.u = 0, c0.u = 0, and conjP(x₁,σ).u = S⁻¹·x₃ (the split lemma,
τ-free). So the wild value collapses to S⁻¹·x₃ — the display (53) wild row.
Ramified d0.g acts trivially (via the hTodd u0.g-triviality).
Ramified D(d₀) = x₂ (= Pb + (P+1)c = c at P = 0; c-term survives, b-term dies).
Ramified D(c₀) = 0 (c₀ = [d₀,z₀], both trivially-based; z0.g reuses the split lemma).
Ramified h₀.g acts trivially (all sub-word bases trivial; only hd0g differs from split).
Ramified D(h₀) = 0 without an hU hypothesis: the cancellation happens in
g₀-conjugate pairs, (g₀⁻¹•x₂ + x₂) + (g₀⁻¹•x₂ + x₂) = 0, via conjP_u_of_base_trivial —
the x₀^{g₀}/dg terms carry the same g₀⁻¹ prefix as each other, so no triviality of g₀'s
action is needed. (hU is not derivable from admissibility: S₃ on its 2-dimensional simple
module, marking x₀=x₁=1, is admissible with σ₂ = σ acting nontrivially.)
The ramified wild row (Lemma 5.5, V^T = 0): L_w = D(h₀) + D(u₁⁻¹) + D(x₁^σ) + D(c₀) = 0 + 0 + S⁻¹·x₃ + 0 = S⁻¹·x₃. This is (d1Fun t x).2 at a ramified simple module — the wild half
forcing d = x₃ = 0 in the normal form.