Stage G / P6 — the Gauss-sum value G(Q) = ±2^{d/2} and agreement glue

prop:candidatezero (l.2731) and prop:localzero (l.3349) of reference/q2_manuscript.tex are zero-count statements; the §8 zero-edge formula (prop:zeroedge, eq:recursionR4b l.4342–4349) consumes them through the Gauss sum G(Q⁰) = ∑_x (-1)^{Q⁰(x)}: "the base local Gauss sum is negative in the unramified case and positive in the ramified case" (prop:localzero, l.3358–3360). This file supplies the value- and agreement-level glue, all proven (no axioms):

• gaussType_eq_of_zeroCount — the Gauss type (Bool-valued Arf type of GaussSign.lean) is pinned by any realized zero count (extraction of the pinning step inside candidate_numZeros_eq_gaussType);
• nonsingular_numZeros_eq_gaussType — the axiom-free Dickson restatement: #Q⁻¹(0) = baseZeroCount (gaussType Q) d for every nonsingular form with 0 < d (via nonsingular_numZeros_dickson);
• gaussSum_eq_sign_two_pow — G(Q) = (-1)^{Arf(Q)}·2^{d/2} in the project spelling gaussSum Q = baseGaussSign (gaussType Q) * 2^(d/2);
• two_mul_numZeros_eq — the unsigned bridge 2·#Q⁻¹(0) = 2^d + baseGaussSign (gaussType Q)·2^{d/2} (for ℕ-valued consumers of the §8 recursion formulas);
• gaussSum_eq_of_numZeros_eq / gaussSum_eq_of_gaussType_eq — the common-G(Q⁰) glue: two nonsingular forms of the same (positive) dimension with the same zero count, or the same Gauss type, have the same Gauss sum. The still-missing §6 content is exactly the two type-pinning inputs (gaussType Q_A⁰ = gaussType Q⁰_loc = ramification type of V) — see audit/BLOCKR_P6_DESIGN.md for their status and provenance (prop:candidatezero = lem:wall + lem:unitaryline + lem:ramifiedhermitian; prop:localzero = local CFT + lem:shapirodet).

Everything below is finite F₂ linear algebra plus integer arithmetic; proof idioms mirror the green Quadratic/DicksonCount.lean.

The Gauss type is pinned by a realized zero count

theorem Q2Presentation.Quadratic.gaussType_eq_of_zeroCount {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] (q : QuadF2 V) (ram : Bool) (h : ↑(numZeros q) = baseZeroCount ram (Module.finrank (ZMod 2) V)) : gaussType q = ram

If the zero count of q realizes baseZeroCount ram d, then gaussType q = ram (uniqueness via baseZeroCount_ne). Extraction of the pinning step used inside candidate_numZeros_eq_gaussType / q2_local_numZeros_eq_gaussType (GaussSign.lean).

theorem Q2Presentation.Quadratic.nonsingular_numZeros_eq_gaussType {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] [Finite V] (q : QuadF2 V) (hns : q.Nonsingular) (hpos : 0 < Module.finrank (ZMod 2) V) : ↑(numZeros q) = baseZeroCount (gaussType q) (Module.finrank (ZMod 2) V)

Axiom-free Dickson restatement: the zero count of a nonsingular form realizes its own Gauss type, #Q⁻¹(0) = baseZeroCount (gaussType Q) d (0 < d). This is the sorry-free, axiom-free counterpart of candidate_numZeros_eq_gaussType / q2_local_numZeros_eq_gaussType (which still route through the two dead GaussSign.lean axioms — see the swap plan in audit/BLOCKR_P6_DESIGN.md).

The Gauss-sum value ±2^{d/2}

theorem Q2Presentation.Quadratic.sq_eq_two_pow_forces_even {d : ℕ} {D : ℤ} (hpos : 0 < d) (hsq : D ^ 2 = 2 ^ d) : 0 < d / 2 ∧ d % 2 = 0

Arithmetic core: D² = 2^d with 0 < d forces d even and d/2 ≥ 1 (the exponent-extraction step of Dickson.dickson_arith).

theorem Q2Presentation.Quadratic.gaussSum_eq_sign_two_pow {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] [Fintype V] (q : QuadF2 V) (hns : q.Nonsingular) (hpos : 0 < Module.finrank (ZMod 2) V) : Dickson.gaussSum q = baseGaussSign (gaussType q) * 2 ^ (Module.finrank (ZMod 2) V / 2)

The Gauss-sum value (prop:localzero l.3358–3360 reading: G(Q) = (-1)^{Arf(Q)}·2^{d/2}): for a nonsingular form on a finite space of positive dimension,

  gaussSum Q = baseGaussSign (gaussType Q) * 2^(d/2).

Combines the Dickson count with the counting identity 2·#Q⁻¹(0) = 2^d + G.

theorem Q2Presentation.Quadratic.two_mul_numZeros_eq {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] [Fintype V] (q : QuadF2 V) (hns : q.Nonsingular) (hpos : 0 < Module.finrank (ZMod 2) V) : 2 * ↑(numZeros q) = 2 ^ Module.finrank (ZMod 2) V + baseGaussSign (gaussType q) * 2 ^ (Module.finrank (ZMod 2) V / 2)

Unsigned bridge for the ℕ-valued §8 recursion formulas: 2·#Q⁻¹(0) = 2^d + baseGaussSign (gaussType Q)·2^{d/2} — the zero count carries the signed Gauss sum without signed subtraction on the count side.

Agreement glue: common G(Q⁰) from matched counts or matched types

theorem Q2Presentation.Quadratic.gaussSum_eq_of_numZeros_eq {Vc : Type u_1} {Vl : Type u_2} [AddCommGroup Vc] [Module (ZMod 2) Vc] [Fintype Vc] [AddCommGroup Vl] [Module (ZMod 2) Vl] [Fintype Vl] (qc : QuadF2 Vc) (ql : QuadF2 Vl) (hcard : ↑(Fintype.card Vc) = ↑(Fintype.card Vl)) (hn : ↑(numZeros qc) = ↑(numZeros ql)) : Dickson.gaussSum qc = Dickson.gaussSum ql

Gauss sums agree whenever the ambient cardinalities and zero counts do (the bridge from candidate_numZeros_eq_local-style outputs to the G(Q⁰) spelling of eq:recursionR4b). No nonsingularity needed.

theorem Q2Presentation.Quadratic.gaussSum_eq_of_gaussType_eq {Vc : Type u_1} {Vl : Type u_2} [AddCommGroup Vc] [Module (ZMod 2) Vc] [Fintype Vc] [AddCommGroup Vl] [Module (ZMod 2) Vl] [Fintype Vl] (qc : QuadF2 Vc) (hnsc : qc.Nonsingular) (ql : QuadF2 Vl) (hnsl : ql.Nonsingular) (hdim : Module.finrank (ZMod 2) Vc = Module.finrank (ZMod 2) Vl) (hpos : 0 < Module.finrank (ZMod 2) Vc) (htype : gaussType qc = gaussType ql) : Dickson.gaussSum qc = Dickson.gaussSum ql

The common-Gauss-sum glue for prop:zeroedge (eq:recursionR4b l.4342–4349): two nonsingular forms of the same positive dimension and the same Gauss type have the same Gauss sum G(Q⁰) = ±2^{d/2}. The two §6 type-pinning inputs (gaussType Q_A⁰ = ram(V) from prop:candidatezero, gaussType Q⁰_loc = ram(V) from prop:localzero) plug in here to produce the single common factor G(Q⁰) of the zero-edge formula.