Principal declarations
theorem ClassicalBoundary.parityNotAC0_of_hastad
Module Classical
(lean/phase6/Classical.lean, lines 333–350) · file SHA-256 ee9d365e1611d40c… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound
WORST-CASE HARDNESS FROM THE EXTERNAL INPUT: HastadNegl ⇒ ParityNotAC0.
Statement as elaborated and printed by Lean 4.26.0
NimAudit.ClassicalBoundary.HastadNegl → NimAudit.Barrier.ParityNotAC0
Exact source text, lines 333–350
333/-- WORST-CASE HARDNESS FROM THE EXTERNAL INPUT: HastadNegl ⇒ ParityNotAC0. -/334theorem parityNotAC0_of_hastad (hH : HastadNegl) : ParityNotAC0 := by335 intro d c k336 obtain ⟨δ, ⟨hnn, hneg⟩, hcorr⟩ := hH d c k337 obtain ⟨n0, hn0⟩ := hneg 1338 refine ⟨max n0 1, fun m hm => hard_of_premise (ε := 1 / 4) (by omega) (by grind)339 (premise_mono (premise_of_classical (by omega) (hcorr m (by omega))) ?_)⟩340 have h1 := hn0 m (by omega)341 have hm1 : (1 : Rat) ≤ (m : Rat) := by exact_mod_cast (show 1 ≤ m by omega)342 have hpos := hnn m343 simp only [Rat.pow_one] at h1344 -- δ m · (m + 1) ≤ 1 with m ≥ 1 gives δ m ≤ 1/2 < 1345 have : δ m ≤ 1 / 2 := by346 have h2 : δ m * 2 ≤ δ m * ((m : Rat) + 1) := Rat.mul_le_mul_of_nonneg_left (by grind) hpos347 grind348 have h3 := div_le_div_of_le (show (0 : Rat) < 2 by decide) this349 have e : (1 / 2 : Rat) / 2 = 1 / 4 := by grind350 rw [e] at h3; exact h3
Project declarations in the statement: Barrier.ParityNotAC0, ClassicalBoundary.HastadNegl
Project declarations used by the proof or definition body
ClassicalBoundary.ClassicalCorr, ClassicalBoundary.HastadNegl, ClassicalBoundary.Negligible, ClassicalBoundary.premise_mono, ClassicalBoundary.premise_of_classical, ParityCircuit.ParityHard, ParityCircuit.hard_of_premise, Prob.div_le_div_of_le
Definitions these statements use
def ClassicalBoundary.HastadNegl
Module Classical
(lean/phase6/Classical.lean, lines 282–286) · file SHA-256 ee9d365e1611d40c…
THE EXTERNAL CLASSICAL THEOREM (Håstad 2014, Cor. 3.2, negligible family form), a
hypothesis: for every depth d and polynomial gate bound c·m^k there is a negligible δ
with ClassicalCorr d (c·m^k) m (δ m) for all m ≥ 1.
Statement as elaborated and printed by Lean 4.26.0
Prop
Exact source text, lines 282–286
282/-- THE EXTERNAL CLASSICAL THEOREM (Håstad 2014, Cor. 3.2, negligible family form), a283 hypothesis: for every depth d and polynomial gate bound c·m^k there is a negligible δ284 with ClassicalCorr d (c·m^k) m (δ m) for all m ≥ 1. -/285def HastadNegl : Prop :=286 ∀ d c k : Nat, ∃ δ : Nat → Rat, Negligible δ ∧ ∀ m, 1 ≤ m → ClassicalCorr d (c * m ^ k) m (δ m)
Project declarations in the statement: none
Project declarations used by the proof or definition body
ClassicalBoundary.ClassicalCorr, ClassicalBoundary.Negligible
def Barrier.ParityNotAC0
Module Barrier
(lean/phase6/Barrier.lean, lines 36–37) · file SHA-256 474ac44cf86dd7e7…
CLASSICAL WORST-CASE PARITY HARDNESS, family form (EXTERNAL HYPOTHESIS).
Statement as elaborated and printed by Lean 4.26.0
Prop
Exact source text, lines 36–37
36/-- CLASSICAL WORST-CASE PARITY HARDNESS, family form (EXTERNAL HYPOTHESIS). -/37def ParityNotAC0 : Prop := ∀ d c k : Nat, ∃ m0 : Nat, ∀ m, m0 ≤ m → ParityHard d (c * m ^ k) m
Project declarations in the statement: none
Project declarations used by the proof or definition body
ParityCircuit.ParityHard
Full modules
Build evidence: fresh isolated rebuild of all 38 bundled modules with Lean (version 4.26.0, started 2026-10-10T15:21:56Z, finished 2026-10-10T15:27:00Z: 38/38 modules compiled, 1588 axiom reports, no errors. See Build for the commands and the independent audit of 2026-10-10 (dated evidence).