Candidate-side Arf / Gauss-sum: de-axiomatization of candidate_base_zeroCount

This file targets the axiom Q2Presentation.Quadratic.candidate_base_zeroCount (Quadratic/GaussSign.lean, l.418), the Lean rendering of manuscript prop:candidatezero: a nonsingular quadratic form over F₂ in dimension d has 2^{d-1} + (-1)^{Arf} 2^{d/2-1} zeros, with the sign determined by the Arf invariant of the form.

STATUS (post-fix). The inconsistency diagnosed in this file has been corrected in Quadratic/GaussSign.lean: the two count axioms are now the consistent existential form ∃ ram, # = baseZeroCount ram d (the ram recovered as the form-tied gaussType), so the project no longer derives False. This file is retained as the diagnosis/record; the single now-stale False derivation (project_axiom_yields_false) is neutralized below.

Outcome: the verbatim free-ram axiom statement was FALSE (now fixed)

The axiom is

(qA : QuadF2 V) (hns : qA.Nonsingular) (ram : Bool) :
    (numZeros qA : ℤ) = baseZeroCount ram (Module.finrank (ZMod 2) V)

Its bug: ram : Bool is a free argument, decoupled from qA. The manuscript's sign is (-1)^{Arf(Q)}, where the ramification flag is a property of the form (unramified ⟹ Arf=1 ⟹ minus type; ramified ⟹ Arf=0 ⟹ plus type). As written, the axiom asserts that the single integer numZeros qA equals baseZeroCount ram d for both ram = true and ram = false, forcing baseZeroCount true d = baseZeroCount false d — contradicting baseZeroCount_ne (proven in the same file). So no theorem candidate_base_zeroCount_proven with the verbatim statement can exist: it would prove False.

This file establishes that rigorously, axiom-clean:

• hyp — the hyperbolic plane q(a,b)=ab on (ZMod 2)², a genuinely nonsingular QuadF2 (hyp_nonsingular), with concrete zero count numZeros hyp = 3 (numZeros_hyp);
• hyp_count_eq_plus / hyp_count_ne_minus — its true count is the plus type (3), not the minus type (1): the bug made concrete;
• candidate_base_zeroCount_unsound — the verbatim statement (at V = (ZMod 2)²) implies False (closure ⊆ {propext, Classical.choice, Quot.sound}: the statement is outright refutable, not merely unprovable);
• project_axiom_yields_false (NEUTRALIZED below — the bug is fixed) — this once derived False from the actual project axiom (the free ram instantiated at both values). With the corrected ∃ ram, … axiom it no longer typechecks; project_axiom_no_longer_yields_false records the now-sound existential in its place.

The honest replacement

hyp_correct_existential records the correct shape (∃ ram, numZeros = baseZeroCount ram d, ram tied to the form) for the witness. The GENERAL corrected theorem — that this ∃ holds for every nonsingular QuadF2 — is the Dickson zero-count via the Arf invariant + Witt/Wall decomposition over F₂. mathlib has neither Arf nor the quadratic-form zero count, so the general statement must be built from scratch; it is out of scope for a verbatim de-axiomatization (which is impossible regardless). GaussSign.lean has now been fixed to constrain ram to the form — the existential candidate_base_zeroCount/q2_local_base_zeroCount plus the form-tied gaussType — so the downstream candidate_gauss_eq_local_gauss is now sound and the project is consistent again.

@[reducible, inline]

abbrev Q2Presentation.Quadratic.CandidateArf.W : Type

Carrier of the explicit witness: the hyperbolic plane (ZMod 2)².

Equations

• Q2Presentation.Quadratic.CandidateArf.W = (ZMod 2 × ZMod 2)

def Q2Presentation.Quadratic.CandidateArf.hypPolar : W →ₗ[ZMod 2] W →ₗ[ZMod 2] ZMod 2

Hyperbolic-plane polar form b((a,b),(c,d)) = a*d + b*c as a genuine bilinear map.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Q2Presentation.Quadratic.CandidateArf.hypPolar_apply (a b : W) : (hypPolar a) b = a.1 * b.2 + a.2 * b.1

def Q2Presentation.Quadratic.CandidateArf.hyp : QuadF2 W

The hyperbolic quadratic form q(a,b) = a*b on (ZMod 2)². A genuinely nonsingular QuadF2 (its polar form is the standard symplectic form).

Equations

• One or more equations did not get rendered due to their size.

theorem Q2Presentation.Quadratic.CandidateArf.hyp_nonsingular : hyp.Nonsingular

The witness form is nonsingular.

theorem Q2Presentation.Quadratic.CandidateArf.finrank_W : Module.finrank (ZMod 2) W = 2

theorem Q2Presentation.Quadratic.CandidateArf.numZeros_hyp : numZeros hyp = 3

theorem Q2Presentation.Quadratic.CandidateArf.hyp_count_eq_plus : ↑(numZeros hyp) = baseZeroCount true (Module.finrank (ZMod 2) W)

The witness's genuine zero count is the PLUS type (ram = true): # = 2^{d-1} + 2^{d/2-1} = 3, matching prop:candidatezero for this (hyperbolic ⇒ Arf = 0 ⇒ plus) form.

theorem Q2Presentation.Quadratic.CandidateArf.hyp_count_ne_minus : ↑(numZeros hyp) ≠ baseZeroCount false (Module.finrank (ZMod 2) W)

...and it does NOT equal the MINUS type (ram = false): 3 ≠ 1. So no single number can satisfy the axiom for both ramification flags.

theorem Q2Presentation.Quadratic.CandidateArf.candidate_base_zeroCount_unsound : ¬∀ {V : Type} [inst : AddCommGroup V] [inst_1 : Module (ZMod 2) V] [Module.Finite (ZMod 2) V] (qA : QuadF2 V), qA.Nonsingular → ∀ (ram : Bool), ↑(numZeros qA) = baseZeroCount ram (Module.finrank (ZMod 2) V)

The exact statement of candidate_base_zeroCount is FALSE.

The axiom (GaussSign.lean l.418) takes the ramification flag ram : Bool as a free argument decoupled from the form qA, asserting # qA⁻¹(0) = baseZeroCount ram d for every ram. But numZeros qA is a single integer while baseZeroCount false d ≠ baseZeroCount true d (baseZeroCount_ne, same file). Instantiating at the genuinely nonsingular hyperbolic form hyp on (ZMod 2)² forces baseZeroCount false 2 = baseZeroCount true 2, i.e. 1 = 3 — a contradiction.

Hence the axiom cannot be de-axiomatized as stated: there is no candidate_base_zeroCount_proven with the verbatim statement (it would prove False). The manuscript (prop:candidatezero, # Q⁻¹(0) = 2^{d-1} + (-1)^{Arf(Q)} 2^{d/2-1}) ties the sign to Arf(Q); the Lean axiom's bug is that ram is not constrained to the form's Arf invariant.

theorem Q2Presentation.Quadratic.CandidateArf.hyp_correct_existential : ∃ (ram : Bool), ↑(numZeros hyp) = baseZeroCount ram (Module.finrank (ZMod 2) W)

The mathematically correct statement (manuscript prop:candidatezero): the zero count equals baseZeroCount ram d for the unique ram determined by the form's Arf invariant — phrased here existentially (the honest replacement for the broken axiom). Proven for the witness with ram = true. The GENERAL theorem (this ∃ holds for every nonsingular QuadF2) is the Dickson zero-count, requiring the Arf invariant + Witt/Wall decomposition over F₂, neither of which is in mathlib.

theorem Q2Presentation.Quadratic.CandidateArf.project_axiom_no_longer_yields_false : ∃ (ram : Bool), ↑(numZeros hyp) = baseZeroCount ram (Module.finrank (ZMod 2) W)

[HISTORICAL RECORD — two repair rounds.] Round 1: the ORIGINAL free-ram candidate_base_zeroCount derived False by instantiating one form at both flags (the commented derivation below). Round 2 (2026-07-08 adversarial keep audit): the ∃-form replacement was STILL refutable at V = 0 (count 1 vs base values), so both zero-count axioms were DELETED from GaussSign.lean; the counts are now the [Nontrivial V]-guarded Dickson THEOREMS (DicksonCount.lean), and this witness statement is discharged by the local computation hyp_correct_existential.

theorem project_axiom_yields_false : False :=
  baseZeroCount_ne (Module.finrank (ZMod 2) W)
    ((candidate_base_zeroCount hyp hyp_nonsingular false).symm.trans
      (candidate_base_zeroCount hyp hyp_nonsingular true))