Head, tail, and assembly bounds for the deep count #
The tail survivor, the head bound, and their assembly into the structural inequality.
See GQ2.DeepCount for the paper-facing overview, source citations, and deviations.
The tail survivor: #Dc_{2e} ≥ 2 #
The graded squaring at i = e kills [−1] ≠ [1] (‖−1 − 1‖ = ‖2‖ = ‖π‖^e exactly), so it
is NOT injective; on equal-card grs it is then not surjective, and any unit class outside
its range is a NONZERO element of Dc_{2e}: were it zero, the Kummer kernel would make the
unit a square w² with w ∈ U_e (the dichotomy), putting it back in the range.
−1 is a depth-e unit: ‖−1 − 1‖ = ‖2‖ = ‖π‖^e.
−1 is NOT a depth-(e+1) unit (‖π‖^e > ‖π‖^{e+1}).
The tail survivor: some depth-2e Kummer class is nonzero. The graded squaring at
i = e has [−1] in its kernel but [−1] ≠ [1], so it is not injective, hence (equal-card
grs) not surjective; a unit class [a] outside the range gives kummerClassK a ≠ 0 — were
it zero, the Kummer kernel would write a = w² with w ∈ U_e (norm-one by taking norms;
depth-e by the dichotomy), and [a] = grSq [w].
The head: #(M ⧸ Dc_1) ≤ 2 #
Two inputs: the level-0 collapse Dc_0 ≤ Dc_1 (the residue group U⁰/U¹ has ODD order
2^f − 1, so squaring is bijective on it — grSq at i = 0 is the squaring map of the
gr-group itself), and the π-parity decomposition (every a ∈ k^× is u·π^m with u
norm-one, by discreteness), which makes M ⧸ Dc_1 generated by the single 2-torsion class
mk [π].
The ℕ-valuation from discreteness: a nonzero integral k-element has norm an exact
power of ‖π‖. Take the least m with ‖π‖^{m+1} < ‖x‖; then x/π^m is integral of norm
> ‖π‖, hence norm one by hπ_max.
The level-0 collapse Dc_0 ≤ Dc_1: the residue group U⁰/U¹ has odd order
2^f − 1 (B13 card_gr_zero, as a hypothesis over the depthUnits 0-form), so squaring is
bijective on it and every norm-one unit is a square times a principal unit.
kummerClassK of a power: [a^m] = m • [a].
2-torsion nsmul reduction: m • ξ = (m % 2) • ξ.
The uniformizer as a unit of k.
Equations
- GQ2.piUnit k π hπk hπ0 = Units.mk0 ⟨π, hπk⟩ ⋯
Instances For
The head bound: M ⧸ Dc_1 is generated by the single 2-torsion class of the
uniformizer (π-parity via the ℕ-valuation, unit part into Dc_1 by the level-0
collapse), so it has at most 2 elements.
The assembly: #(M ⧸ Dc_{e+1}) ≤ #Dc_e #
The paired descent: R(s) : #(M⧸Dc_{e+1})·#Dc_{e+1+s} ≤ #Dc_e·#(M⧸Dc_{e−s}) holds at
s = 0 with equality (double Lagrange), and each step trades the level e−s−1 on the right
for the level e+1+s on the left — same-parity levels summing to 2e, where the class-gr
counts compare (= 2^f odd / = 1 ≤ even). At s = e−1 the head (≤ 2) and the tail
survivor (≥ 2) close the inequality.
Lagrange step-down for the class filtration:
#Dc_j = #(Dc_j/Dc_{j+1}) · #Dc_{j+1}.
Lagrange step-up for the ambient quotients:
#(M⧸Dc_{j+1}) = #(M⧸Dc_j) · #(Dc_j/Dc_{j+1}).
The paired level comparison: for 1 ≤ j ≤ e − 1, the class-gr at j is at most the
class-gr at 2e − j (same parity: odd levels are both 2^f, even levels collapse to 1).
THE STRUCTURAL COUNT — the single remaining input of (H4)'s sharpness:
#(M ⧸ Dc_{e+1}) ≤ #Dc_e, by the paired descent between the double-Lagrange identity at
s = 0 and the head/tail comparison at s = e − 1.