Stage G / P6 — the constrained quadratic Gauss transform (lem:constrainedgauss) #
This file formalizes the finite quadratic-form algebra consumed by the §8
zero-edge formula (prop:zeroedge, reference/q2_manuscript.tex l.4314–4369):
lem:constrainedgauss(l.3876–3906,eq:constrainedgaussl.3888–3894): for a surjectionL : W ↠ Eof finiteF₂-spaces and a quadratic formQonWwith polar formb_Q,2·|E|·#{x : L x = κ, Q(x) = ε} = |W| + G(Q⁰)·∑_{χ ∈ E^∨} (-1)^{χ(κ)+ε+Q⁰(a_χ)},where
b_Q(a_χ, ·) = χ ∘ L (+ linear part)andG(Q⁰) = ∑_x (-1)^{Q⁰(x)}is the Gauss sum (Dickson.gaussSum). We prove the affine form directly (constrainedGauss_count): the quadratic function isQ⁰ + ℓwithℓlinear (theeq:Qkappadifferenceshape, l.2158–2163:Q_κ = Q⁰ + ⟨·,ρ*γ_κ⟩ + const, constants being absorbed intoε), the representing vectors solveb_Q(a_χ, ·) = χ∘L + ℓ(manuscripta_{χ,κ} = (b_q^♭)^{-1}(γ_χ + γ_κ), l.4089–4094), and the surviving phase is the base-form valueQ⁰(a_χ)(manuscriptΘ_q^0(a_{χ,κ}),eq:Theta0phasel.4097–4100). Atℓ = 0this islem:constrainedgaussverbatim (constrainedGauss_count_pure).the completed square (
QuadF2.completedSquare):Q(x) + b_Q(a,x) = Q(x+a) + Q(a)— the algebraic core ofprop:phaseidentity(l.4108–4146, the display at l.4137–4142) and of thelem:constrainedgaussproof step (l.3899–3904).existence and uniqueness of the representing vectors
a_χfrom nonsingularity (QuadF2.polar_bijective,QuadF2.exists_polarRep,QuadF2.polarRep_unique) — the manuscript's "leta_χbe uniquely determined byb_Q(a_χ,x) = χ(Lx)" (l.3883–3885).the linear-shift constructor
QuadF2.addLinear(eq:Qkappadifferenceat form level): adding a linear term keeps the polar form, hence nonsingularity — this is whyprop:zeroedgemay complete the square against the base form.
Everything here is pure finite linear algebra over F₂ — no arithmetic
input, no axioms; the two sources enter only later, through the common value of
G(Q⁰) (prop:candidatezero l.2731 / prop:localzero l.3349, see
Quadratic/GaussSumValue.lean and audit/BLOCKR_P6_DESIGN.md).
Proof idioms deliberately mirror the green Quadratic/DicksonCount.lean
(sign-character expansion, translation reindexing, Finset calculus).
Part 0 — char-2 and dual-space helpers #
The dual of a finite F₂-module is finite.
Finite F₂ duality preserves cardinality: |E^∨| = |E|.
1 + χ(a) = 2·[a = 0] for the sign character (the ε-indicator expansion of
lem:constrainedgauss, l.3898–3899).
Dual orthogonality over F₂: ∑_{χ ∈ E^∨} (-1)^{χ(v)} is |E^∨| at
v = 0 and 0 otherwise (the κ-indicator expansion of lem:constrainedgauss,
l.3898–3899; nontrivial characters cancel by translation).
Part 1 — completed square, linear shifts, and representing vectors #
The completed square (prop:phaseidentity's algebraic core, l.4137–4142;
the square-completion step of lem:constrainedgauss, l.3899–3904):
Q(x) + b_Q(a, x) = Q(x + a) + Q(a).
Adding a linear term to a QuadF2 (eq:Qkappadifference l.2158–2163 /
eq:candidategeneralQ l.2487–2491 at form level, constants dropped): the polar
form is unchanged.
Equations
Instances For
A linear shift preserves nonsingularity (same polar form). This is why the
zero-edge count of the actual pushout form Q_κ may be computed against the
base form Q⁰ (prop:zeroedge l.4358–4366).
Nonsingularity makes the polar map a ↦ b_Q(a, ·) injective into the
dual.
Nonsingularity + finiteness make the polar map a bijection onto the dual
(existence-uniqueness of the representing vectors a_χ, lem:constrainedgauss
l.3883–3885).
Every functional on a finite nonsingular quadratic space is represented by the
polar form: ∃ a, b_Q(a, ·) = ψ.
The representing vector is unique, so the phase Q(a_χ) of
eq:constrainedgauss is well-defined.
Part 2 — the constrained zero count and the Gauss transform #
N(κ, ε) — the constrained count of lem:constrainedgauss (l.3879–3882),
with an affine (linear-term) refinement: #{x : L x = κ ∧ Q(x) + ℓ(x) = ε}.
At ℓ = 0 this is the manuscript's N(κ,ε); the affine form is what
prop:zeroedge consumes through eq:Qkappadifference (the actual pushout form
Q_κ is base-plus-linear, its constant part being absorbed into ε).
Equations
Instances For
The constrained quadratic Gauss transform (lem:constrainedgauss,
eq:constrainedgauss l.3888–3894, in the affine form consumed by
eq:pointwiseconstrained l.4332–4340):
2·|E|·N(κ,ε) = |W| + G(Q⁰)·∑_{χ ∈ E^∨} (-1)^{χ(κ) + ε + Q⁰(a_χ)}
for L : W ↠ E, Q⁰ a quadratic form with representing vectors
b_{Q⁰}(a_χ, ·) = χ∘L + ℓ, and N(κ,ε) = #{x : Lx = κ, Q⁰(x) + ℓ(x) = ε}.
The Gauss sum G(Q⁰) = ∑_x (-1)^{Q⁰(x)} is Dickson.gaussSum; the phase
Q⁰(a_χ) is the manuscript's Θ_q^0(a_{χ,κ})-value (eq:Theta0phase).
Note the hypotheses are weaker than the manuscript's: nonsingularity is not
needed once the representing vectors A are supplied (it is needed only for
their existence — constrainedGauss_count_exists), and surjectivity of L is
used only to cancel nontrivial characters.
lem:constrainedgauss verbatim (eq:constrainedgauss, l.3888–3894): the
pure case ℓ = 0, i.e. 2·|E|·#{x : Lx = κ, Q(x) = ε} = |W| + G(Q)·∑_χ (-1)^{χ(κ)+ε+Q(a_χ)} with b_Q(a_χ,·) = χ∘L.
lem:constrainedgauss in existential form: for a nonsingular Q the
representing vectors exist (b_Q(a_χ,·) = χ∘L + ℓ, unique by
QuadF2.polarRep_unique) and the transform holds for them. This is the exact
package prop:zeroedge consumes at W := H¹-model, E := H²(T)-model,
L := ∂, κ := ρ*e, ℓ := ⟨·, ρ*γ_κ⟩ (eq:pointwiseconstrained).