Documentation

GQ2.SectionEight

§8: central covers, affine fibres, and Fourier inversion — statements #

Statement-first extraction of the paper's §8 (pages 38–44): the half-torsor count (Lemma 8.6) and the closed exact-image recursion (Prop 8.9, displays (136)–(142)), together with the finite Fourier/Gauss engines they run on (Lemmas 8.4/8.5) and the central-cover bookkeeping (Lemma 8.2/8.3). The §9 induction consumes only the boxed system of Prop. 8.9 plus Lemma 8.3.

Setting (§8 opening): the simple-head block of §7 (GQ2.SectionSeven.MinimalBlock) on a boundary-framed marked target 𝒴 = (Y, L_Y, π_Y, θ_Y) (GQ2.MarkedTarget), with R = Φ(K), M = K/R, 0 → T → M → V → 0, B = Y/R, C = Y/K, and T = T₀ = (K∩S)R/R (Lemma 7.1). All counts are the exact-image counts e^β_Γ(·) of eq. (29) (GQ2.exactImageCount) for the two sources Γ ∈ {Γ_A, G_ℚ₂} through a BoundaryMaps witness (the boundary-frame design).

Encoding decisions and deviations #

  1. Lemmas 8.4/8.5 are proved, in multiplied-out integer form. (125) is stated as |D| · #{o = 0} = Σ_λ (2 m_λ − |X|) over ℤ (no division), with D the 𝔽₂-linear dual; (126) as 2|E| · N(κ,ε) = |W| + G(Q) Σ_χ (−1)^{χ(κ)+ε+Q(a_χ)}. In (126) the paper defines a_χ from nonsingularity; here a is data with the defining spec B_Q(a_χ, x) = χ(L x) (house style, cf. prop_7_4's lam), and nonsingularity is not needed for the identity itself.
  2. Central double covers are a structure (CentralCover): a surjection p : Ỹ ↠ Y with central kernel ⟨z⟩ of order 2. The pulled-back boundary-framed structure of Lemma 8.3 is CentralCover.pullTarget; the paper's side condition "the central kernel lies in ker(π̃, θ̃)" holds by construction (π̃ = π_Y ∘ p kills ker p).
  3. "Scalar pushout vanishes" / "pullback cover is split" is encoded as liftability: u^β_Γ(p, J) (liftableCount) counts boundary-framed exact-image maps to the J-stratum that lift through p as continuous homomorphisms. This is the paper's torsor description verbatim (an unobstructed map has a lift, and its exact-image lifts are the summands of (124)).
  4. Lemma 8.6's edge class is carried operationally. The H¹-valued edge [ε̄] of (128) exists iff the cover does not descend to B/T; the paper's own descent clause says a descended cover is exactly a normal complement to the preimage of T. We therefore phrase "edge ≠ 0" as ¬∃ N ◁ B̃, N.map p = T ∧ z ∉ N, and state the half-torsor count in consequence form, per source (the degree-one duality that makes the variation functional (127) nonzero is B6 on the local side and §5 content on the candidate side, so a source-generic statement would need a duality hypothesis — flagged deviation; the H¹-form (128)/(127) is the internal §8 proof).
  5. Lemma 8.7 and Prop 8.8 are not separately stated (the §§6–7 statement layer precedent: 6.7/6.10/6.11): they are proof mechanisms for the (140)-clause of Prop 8.9. Their content enters the statement layer only through the ∃-form of (140) below. If the §9 induction needs (131)/(135) as standalone statements, that is a reviewed addition.
  6. Prop 8.9 is frozen as the boxed system. (136)–(139) are stated verbatim (integer multiplied-out forms, target-side data from the §7 block). The scalar characters λ ∈ D_R = (R^∨)^C are encoded as Y-normal subgroups R' ≤ R of index ≤ 2 (the kernel of λ; Y-normality = C-invariance — same encoding as lemma_7_1_dual), and the scalar cover p_λ : B_λ ↠ B is the quotient map Y/R' ↠ Y/R. (140)–(142) are frozen in ∃-family form: there exist a constant μ and a target-side family of central covers of the C-stratum, indexed by the scalar duals of T, satisfying (140) with s_Γ folded through (141)/(142) (the n_{Γ,0}-liftability form). The family is target-side data, so one witness serves both sources — which is all the §9 induction uses. Pinning the family to the phase classes Δ_{χ,κ} of (133)/(134) is the O-half's work (via 6.21/6.22/8.8).

Axioms: none in this file (statement layer; the Ax budget B6/B7/B9 was consumed by the O-half proofs, which all proved).

Paper-tag ledger (auto-generated by paperforge; do not edit) #