Split-pack and final Γ_A Gauss-residue assembly #
The split hypothesis package and the final discharge against the tame package.
See GQ2.GaussZ.FinalGammaA for the paper-facing overview, source citations, and deviations.
A-4.5c: the split hypothesis pack — V^σ = 0 and the trivial σ₂-action #
Unramified structure: with the acting group generated by {s, t} (gen_ttame_quotient
at the tame package) and inertia t acting trivially, every element acts as an integer
power of s — the action image is cyclic. Fixed spaces of powers of s are therefore
invariant submodules, and simplicity forces the dichotomy: V^s = 0 (else the whole
action is trivial, contradicting hnt), while the fixed space of the 2-primary part
σ₂ = powOmega2 s is NONZERO (a 2-group acting on a finite 2-group) hence everything.
These are the hVS/hU inputs of lemma_5_13_split / x0Section_bijective_split /
liftMark_kappa0_wildValue_fib_split.
With C = ⟨s, t⟩ and t acting trivially, every element acts as an integer power
of s.
The cyclic-image commutation: every element's action commutes with powers of s.
The split Frobenius-freeness (hVS): V^s = 0 — the s-fixed space is an
invariant submodule (cyclic image), and = ⊤ would make the whole action trivial,
contradicting hnt.
The split σ₂-triviality (hU): the 2-primary part powOmega2 s acts trivially —
its fixed space is an invariant submodule (cyclic image), NONZERO because a 2-group acting
on a finite even-order module has even fixed count and fixes 0, hence ⊤ by simplicity.
The reverse tame conjugate is a t-power (odd-order square root): if
s⁻¹ * t * s = t² and t has odd order d, then s * t * s⁻¹ is the square root
t^{(d+1)/2} of t (squaring is invertible on the odd-order cyclic group ⟨t⟩), hence
lies in ⟨t⟩.
⟨t⟩ is normalized by every group element (both directions): with C = ⟨s, t⟩,
s⁻¹ * t * s = t², and t of odd order, every g conjugates t into ⟨t⟩ from either
side, proved by closure induction over the generating set {s, t}.
The ramified inertia-freeness (htauf): with C = ⟨s, t⟩, the tame relation
s⁻¹ts = t², and t of odd order, every conjugate of t is a power of t
(⟨t⟩ is normal: s-conjugation squares, and the reverse conjugate is the square ROOT
t^{(d+1)/2} — odd order makes squaring invertible on ⟨t⟩), so the t-fixed space is
an invariant submodule; if t moves anything, simplicity forces it to ⊥ — V^t = 0.
A-4.6: the G0-obtain discharge against the c3-G0 tame package #
The ThmFourTwo ⟨G0, hGaussZA, hGaussZF⟩-obtain, decomposed: everything except the
per-block tame-structure package is proved. The package fields mirror the residue
theorems' hpack shapes VERBATIM (per-lift factorizations with the dichotomy clause);
hfaith is carried for the LOCAL twins only (the Γ_A twins run hfaith-free), and the
ramified flavor carries the orientation (provable only at the concrete
boundaryMapsWitness — tameUnitOrientation_witness).
The c3-G0 tame package, unramified flavor: per-lift tame factorizations for both sources with trivially-acting inertia, plus the form-level constants and the local-side faithfulness.
- m : ℕ
- hm : 1 ≤ self.m
Instances For
The c3-G0 tame package, ramified flavor: inertia moves the module; the local
side additionally needs the tame-unit orientation (at R := localReciprocity).
- m : ℕ
- hm : 1 ≤ self.m
- horient : TameUnitOrientation localReciprocity B.tameF