N8 — the Gauss-sum radical fibration G(Q) = |U| · G(Q̄) (R4b unit ZeroEdgeGaussDescent)

Unit N8 of audit/BLOCKR_R4B_DESIGN.md (§4-N8, §6.1; dependency: the green value layer only). This file is fully abstract quadratic-form algebra over ZMod 2 carriers — no R4b/zero-edge carrier is imported or mentioned — so it lands independently of the Induction wave (N1–N7). Contents:

• gaussSum_of_radical_fibration — the design's headline: if a QuadF2 M annihilates a submodule U (form vanishes on U and U lies in the polar radical — the green Annihilates of Induction/MinimalBlock.lean), then the Gauss sum fibres over the U-cosets: G(Q) = |U| · G(Q̄), with Q̄ = h.descend the green descended form on M ⧸ U. No nonsingularity is needed for the raw fibration.
• gaussSum_of_radical_fibration_pow — the §2.1 spelling G(Q_W) = 2^d · G(Q̄) (d = dim U): this is the factor that fuses the B¹(V)-part of the multiplicity μ = |B¹(V)|·|Z¹(T′)| (eq:mumultiplicity, manuscript l.4065) into the engine's |W|-term so that the pointwise identity rearranges to the keep's muT·(2^d + G(Q̄)·Σ_χ …) shape (design §2.1).
• gaussSum_of_radical_fibration_value (+ _of_rad_le, _of_nontrivial) — the applied value form of §4-N8: with the descended form nonsingular (in the application: edgeHeadForm_nonsingular-transport, done by N7) and the descended dimension positive (in the application: from edgeHead_nontrivial), gaussSum_eq_sign_two_pow gives G(Q) = 2^{dim U} · (baseGaussSign (gaussType Q̄) · 2^{d̄/2}).

The F1 / audit-§A sign discipline (load-bearing)

gaussType (h.descend) is carried below as an opaque value — the Gauss type is LEFT FREE. Per design §4-N8 and audit/CITABILITY_AUDIT_20260708.md §A: the type of the base-problem form on the descended cocycle carrier is never identified with gaussType (edgeHeadForm …) (that identification is refuted: eq:ramifiedarfq vs eq:relativeArf), never pinned to ram/a sign, and its value is never sourced from the Poonen–Rains self-cup cluster (opposite sign). The §5 sign floors (F-sgn-L1/C1/X1) own constancy and value; this unit only produces the factor.

Proof idioms mirror the green Quadratic/WallDoubling.lean / Quadratic/ConstrainedGauss.lean (qualified Dickson.gaussSum, unfold + Finset calculus, Nat.card_congr coset equivalences). Everything is proven — no axioms, no sorry.

theorem Q2Presentation.Induction.natCard_mk_fibre {M : Type u_1} [AddCommGroup M] [Module (ZMod 2) M] (U : Submodule (ZMod 2) M) (m₀ : M) : Nat.card { v : M // Submodule.Quotient.mk v = Submodule.Quotient.mk m₀ } = Nat.card ↥U

Each fibre of M → M ⧸ U over a class mk m₀ is a U-coset, hence equinumerous with U (the coset leg of the design-§2.1 fibration; no finiteness needed).

theorem Q2Presentation.Induction.gaussSum_of_radical_fibration {M : Type u_1} [AddCommGroup M] [Module (ZMod 2) M] [Fintype M] {U : Submodule (ZMod 2) M} [Fintype (M ⧸ U)] {q : Quadratic.QuadF2 M} (h : Annihilates q U) : Quadratic.Dickson.gaussSum q = ↑(Nat.card ↥U) * Quadratic.Dickson.gaussSum h.descend

The Gauss-sum radical fibration (design §4-N8): a QuadF2 M that annihilates a submodule U inside its polar radical (Annihilates q U — the two clauses q|_U = 0, b_q(U, M) = 0) has Gauss sum

  G(Q) = |U| · G(Q̄),

Q̄ = h.descend the green descended form on M ⧸ U: the quadratic map is constant on U-cosets (form_add_mem), so the sign-character sum fibres over the quotient with |U|-fold multiplicity. No nonsingularity hypothesis.

theorem Q2Presentation.Induction.gaussSum_of_radical_fibration_pow {M : Type u_1} [AddCommGroup M] [Module (ZMod 2) M] [Fintype M] {U : Submodule (ZMod 2) M} [Fintype (M ⧸ U)] {q : Quadratic.QuadF2 M} (h : Annihilates q U) : Quadratic.Dickson.gaussSum q = 2 ^ Module.finrank (ZMod 2) ↥U * Quadratic.Dickson.gaussSum h.descend

The 2^d spelling G(Q_W) = 2^{dim U} · G(Q̄) (design §2.1): the radical-fibration factor as the power of 2 that fuses the B¹(V)-part of μ = |B¹(V)|·|Z¹(T′)| (eq:mumultiplicity, l.4065) into the engine's |W|-term when the pointwise identity is rearranged to the keep's muT·(2^d + G(Q̄)·Σ_χ …) shape.

theorem Q2Presentation.Induction.gaussSum_of_radical_fibration_value {M : Type u_1} [AddCommGroup M] [Module (ZMod 2) M] [Fintype M] {U : Submodule (ZMod 2) M} [Fintype (M ⧸ U)] {q : Quadratic.QuadF2 M} (h : Annihilates q U) (hns : h.descend.Nonsingular) (hpos : 0 < Module.finrank (ZMod 2) (M ⧸ U)) : Quadratic.Dickson.gaussSum q = 2 ^ Module.finrank (ZMod 2) ↥U * (Quadratic.baseGaussSign (Quadratic.gaussType h.descend) * 2 ^ (Module.finrank (ZMod 2) (M ⧸ U) / 2))

The applied value form of §4-N8 — with the descended form nonsingular and of positive dimension, gaussSum_eq_sign_two_pow evaluates the descended factor:

  G(Q) = 2^{dim U} · (baseGaussSign (gaussType Q̄) · 2^{d̄/2}),   d̄ = dim (M ⧸ U).

gaussType (h.descend) is the Gauss type of the descended (base-problem) form and is LEFT FREE here (F1 + audit-§A discipline; see the file header): its constancy/value belong to the §5 sign floors, never to this unit. In the R4b application (N7) the nonsingularity hypothesis is discharged by edgeHeadForm_nonsingular-transport and hpos from edgeHead_nontrivial.

theorem Q2Presentation.Induction.gaussSum_of_radical_fibration_value_of_rad_le {M : Type u_1} [AddCommGroup M] [Module (ZMod 2) M] [Fintype M] {U : Submodule (ZMod 2) M} [Fintype (M ⧸ U)] {q : Quadratic.QuadF2 M} (h : Annihilates q U) (hrad : ∀ (m : M), (∀ (m' : M), (q.polar m) m' = 0) → m ∈ U) (hpos : 0 < Module.finrank (ZMod 2) (M ⧸ U)) : Quadratic.Dickson.gaussSum q = 2 ^ Module.finrank (ZMod 2) ↥U * (Quadratic.baseGaussSign (Quadratic.gaussType h.descend) * 2 ^ (Module.finrank (ZMod 2) (M ⧸ U) / 2))

The value form with nonsingularity derived: if in addition the polar radical of q lies inside U (so U is the radical, given Annihilates), the descended form is nonsingular (Annihilates.descend_nonsingular) and the value formula holds. This is the exact hypothesis shape of the design's "polar radical = coboundary part" step (§2.1).

theorem Q2Presentation.Induction.finrank_pos_of_finite_nontrivial (W : Type u_2) [AddCommGroup W] [Module (ZMod 2) W] [Finite W] [Nontrivial W] : 0 < Module.finrank (ZMod 2) W

0 < dim W for a finite nontrivial F₂-module — the abstract residue of the design's "0 < d from edgeHead_nontrivial" leg (§4-N8): N7 feeds a Nontrivial (M ⧸ U) fact (e.g. transported from edgeHead_nontrivial) into the hpos slots above through this bridge.

theorem Q2Presentation.Induction.gaussSum_of_radical_fibration_value_of_nontrivial {M : Type u_1} [AddCommGroup M] [Module (ZMod 2) M] [Fintype M] {U : Submodule (ZMod 2) M} [Fintype (M ⧸ U)] [Nontrivial (M ⧸ U)] {q : Quadratic.QuadF2 M} (h : Annihilates q U) (hrad : ∀ (m : M), (∀ (m' : M), (q.polar m) m' = 0) → m ∈ U) : Quadratic.Dickson.gaussSum q = 2 ^ Module.finrank (ZMod 2) ↥U * (Quadratic.baseGaussSign (Quadratic.gaussType h.descend) * 2 ^ (Module.finrank (ZMod 2) (M ⧸ U) / 2))

Consumer-facing package: Annihilates + radical-inside-U + nontrivial head give the full three-factor value with the Gauss type left free — the exact plug-in shape for N7's per-ρ engine fire (design §4-N7/§4-N8).