Appendix HFull proof of Theorem 5.12: uniform σ, character expansion, finite bound, Håstad input, attainability

Checked conditional theorem using named classical input Lean checks the implication from a named, unproved classical hypothesis.

1 Paper text

Appendix H. Proof of Theorem 5.12

Generated from paper_jmlr.tex, lines 1659–1659.

2 Explain this

The full proof of Theorem 5.12 has three parts.

(i) With uniform independent heaps, the nim-sum is exactly uniform on $\mathbb F_2^B$ . Fix the observed bit $b$ : the readout becomes a fixed shallow circuit proposing a move, which determines a proposed nim-sum $g_b(P)$ ; the move wins exactly when $g_\beta(P)=\sigma(P)$ . Expand the event $\sigma=a$ into its $2^B$ parity characters; each nonconstant character is a parity on at least $N$ input bits, so a shallow indicator has tiny correlation with it (the classical input). Summing the disjoint events and conditioning on $\sigma\ne0$ gives $2/(q-1)+(q-1)\eta_N$ . Fixing all coordinates outside a character's support keeps the circuit shallow, which is how the classical bound for full parity applies. Guessing one nonzero value per fibre attains the leading constant; for $B=2$ and $\pi_0$ the guesses $a_0=2$ , $a_1=1$ win with probability exactly $2/3$ .

(ii) and (iii) are the multi-head and two-frame constructions.

3 How this is formalised

Prob.success_bound: the finite calculation, including uniformity of $\sigma$ , character orthogonality, the exact-value expansion, disjointness and conditioning.
CorrBridge.circuit_readout_bound: the circuit indicators, restriction to a character's support and averaging over fixed coordinates, from the parity-correlation premise.
ClassicalBoundary.search_gap_asymptotic: the asymptotic conclusion from the named input HastadNegl.
Attain.attain_exact and Attain.paper_example_two_thirds: attainability, and the $B=2$ example with success exactly $2/3$ for every $N\ge1$ .

Parts (ii) and (iii) are Theorem 5.12 (ii) and Theorem 5.12 (iii).

Coverage record
Paper anchor	`app:search-gap-proof` (manuscript label)
Displayed as	Appendix H
Claim	Full proof of Theorem 5.12: uniform σ, character expansion, finite bound, Håstad input, attainability
Coverage category	Checked conditional theorem using named classical input
Statement source	paper_jmlr.tex lines 1659–1659; SHA-256 of the normalised block source `7e8cd3062b734b54…`
Lean declarations	`NimAudit.Prob.success_bound` (NimProbability, lines 834–871, file `1d5d7977a43e…`) `NimAudit.CorrBridge.circuit_readout_bound` (NimCorrBridge, lines 873–882, file `d3fb2e4a64db…`) `NimAudit.ClassicalBoundary.search_gap_asymptotic` (Classical, lines 472–510, file `ee9d365e1611…`) `NimAudit.Attain.attain_exact` (NimAttain, lines 563–576, file `dd978aa0cd3d…`) `NimAudit.Attain.paper_example_two_thirds` (NimAttain, lines 600–609, file `dd978aa0cd3d…`)
Named classical inputs	`HastadNegl`
Depends on	Theorem 5.12 (i)
Audited correspondence rows	`app:search-gap-proof`
Explanations	`explain/app:search-gap-proof`, `formal/app:search-gap-proof`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

Principal declarations

theorem `Prob.success_bound`

Module NimProbability (lean/phase2/NimProbability.lean, lines 834–871) · file SHA-256 1d5d7977a43e854d… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

MAIN THEOREM (Appendix G(i), finite form). For every B ≥ 1, N ≥ 1 (written N + 1), every readout F, every vector w (the head's linear functional ell(sigma) = <w, sigma>), and every η, the parity-correlation premise implies Pr[legal winning move | sigma ≠ 0] ≤ 2/(q-1) + (q-1) η, q = 2^B.

Statement as elaborated and printed by Lean 4.26.0

∀ {B N : ℕ},
  1 ≤ B →
    ∀ (F : NimAudit.Prob.Readout) (w : ℕ) {η : ℚ},
      NimAudit.Prob.CorrHyp B (N + 1) F η →
        NimAudit.Prob.succCount B (N + 1) F w / NimAudit.Prob.nonzeroCount B (N + 1) ≤
          2 / (↑(2 ^ B) - 1) + (↑(2 ^ B) - 1) * η

Exact source text, lines 834–871

834/-- MAIN THEOREM (Appendix G(i), finite form).  For every B ≥ 1, N ≥ 1 (written835    N + 1), every readout F, every vector w (the head's linear functional836    ell(sigma) = <w, sigma>), and every η, the parity-correlation premise implies837      Pr[legal winning move | sigma ≠ 0] ≤ 2/(q-1) + (q-1) η,   q = 2^B. -/838theorem success_bound {B N : Nat} (hB : 1 ≤ B) (F : Readout) (w : Nat) {η : Rat}839    (hyp : CorrHyp B (N + 1) F η) :840    succCount B (N + 1) F w / nonzeroCount B (N + 1) ≤841      2 / (((2 ^ B : Nat) : Rat) - 1) + (((2 ^ B : Nat) : Rat) - 1) * η := by842  have hqge : 2 ≤ 2 ^ B := by843    have := Nat.pow_le_pow_right (show 0 < 2 by decide) hB; simpa using this844  have hq2 : (2 : Rat) ≤ ((2 ^ B : Nat) : Rat) := by845    have := Rat.natCast_le_natCast.mpr hqge; simpa using this846  have hjoint := succCount_bound F w hyp847  rw [natCast_pred] at hjoint848  have ht : (0 : Rat) < ((2 ^ B : Nat) : Rat) ^ N := by849    rw [← Rat.natCast_pow]; exact Rat.natCast_pos.mpr (Nat.pow_pos (Nat.two_pow_pos B))850  have hT : T B (N + 1) = ((2 ^ B : Nat) : Rat) * ((2 ^ B : Nat) : Rat) ^ N := by851    unfold T; rw [Rat.pow_succ]; grind852  have hZ : nonzeroCount B (N + 1) =853      (((2 ^ B : Nat) : Rat) - 1) * ((2 ^ B : Nat) : Rat) ^ N := by854    rw [nonzeroCount_eq, hT]; grind855  rw [hT] at hjoint856  rw [hZ]857  generalize succCount B (N + 1) F w = S at *858  generalize ((2 ^ B : Nat) : Rat) ^ N = t at *859  generalize ((2 ^ B : Nat) : Rat) = q at *860  have h1 : (0 : Rat) < q - 1 := by grind861  have hZpos : 0 < (q - 1) * t := Rat.mul_pos h1 ht862  apply le_div_of_mul_le hZpos863  have hqpos : (0 : Rat) < q := by grind864  have hS : S ≤ 2 * t + (q - 1) * ((q - 1) * (η * t)) := by865    apply Rat.le_of_mul_le_mul_left _ hqpos866    grind867  have hq1 : q - 1 ≠ 0 := Rat.ne_of_gt h1868  have eR : (2 / (q - 1) + (q - 1) * η) * ((q - 1) * t) =869      2 * t + (q - 1) * ((q - 1) * (η * t)) := by grind870  rw [eR]871  exact hS

Project declarations in the statement: Prob.CorrHyp, Prob.Readout, Prob.nonzeroCount, Prob.succCount

Project declarations used by the proof or definition body

Prob.CorrHyp, Prob.Readout, Prob.T, Prob.le_div_of_mul_le, Prob.natCast_pred, Prob.nonzeroCount, Prob.nonzeroCount_eq, Prob.succCount, Prob.succCount_bound

theorem `CorrBridge.circuit_readout_bound`

Module NimCorrBridge (lean/phase3/NimCorrBridge.lean, lines 873–882) · file SHA-256 d3fb2e4a64db3e92… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

Combined with phase 2: under the same premise, the circuit readout fed the executed outcome of head pi_j succeeds with conditional probability at most 2/(2^B-1) + (2^B-1) ε.

Statement as elaborated and printed by Lean 4.26.0

∀ {B N j d s : ℕ},
  j < B →
    ∀ (R : Bool → NimAudit.CorrBridge.RCirc),
      (∀ (b : Bool), NimAudit.CorrBridge.RBound (R b) (N + 1) B d s) →
        ∀ {ε : ℚ},
          (∀ (m : ℕ),
              N + 1 ≤ m →
                m ≤ B * (N + 1) →
                  NimAudit.Bridge.ParityCorrPremise (d + 11)
                    (12 * NimAudit.CorrBridge.Upar (N + 1) B s ^ 10) m ε) →
            NimAudit.Prob.succCountRO B (N + 1) (NimAudit.CorrBridge.readoutOf B R) j /
                NimAudit.Prob.nonzeroCount B (N + 1) ≤
              2 / (↑(2 ^ B) - 1) + (↑(2 ^ B) - 1) * ε

Exact source text, lines 873–882

873/-- Combined with phase 2: under the same premise, the circuit readout fed the874    executed outcome of head pi_j succeeds with conditional probability at most875    2/(2^B-1) + (2^B-1) ε. -/876theorem circuit_readout_bound {B N j d s : Nat} (hj : j < B) (R : Bool → RCirc)877    (hb : ∀ b, RBound (R b) (N + 1) B d s) {ε : Rat}878    (hprem : ∀ m, N + 1 ≤ m → m ≤ B * (N + 1) →879      ParityCorrPremise (d + 11) (12 * Upar (N + 1) B s ^ 10) m ε) :880    succCountRO B (N + 1) (readoutOf B R) j / nonzeroCount B (N + 1) ≤881      2 / (((2 ^ B : Nat) : Rat) - 1) + (((2 ^ B : Nat) : Rat) - 1) * ε :=882  structured_head_bound hj _ (corrHyp_of_premise R hb hprem)

Project declarations in the statement: Bridge.ParityCorrPremise, CorrBridge.RBound, CorrBridge.RCirc, CorrBridge.Upar, CorrBridge.readoutOf, Prob.nonzeroCount, Prob.succCountRO

Project declarations used by the proof or definition body

Bridge.ParityCorrPremise, CorrBridge.RBound, CorrBridge.RCirc, CorrBridge.Upar, CorrBridge.corrHyp_of_premise, CorrBridge.readoutOf, Prob.structured_head_bound

theorem `ClassicalBoundary.search_gap_asymptotic`

Module Classical (lean/phase6/Classical.lean, lines 472–510) · file SHA-256 ee9d365e1611d40c… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

ASYMPTOTIC SINGLE-CHANNEL THEOREM (thm:search-gap (i), asymptotic form), conditional only on the external classical input. Fix B ≥ 2 and j < B. Let R N b be binary readout formulas for N+1 heaps with BBound of FIXED depth d and size s N, index width r N, where s and r are polynomially bounded in N+1. Then there is a negligible η with success_N ≤ 2/(2^B − 1) + η N for every N.

Statement as elaborated and printed by Lean 4.26.0

NimAudit.ClassicalBoundary.HastadNegl →
  ∀ {B j : ℕ},
    j < B →
      ∀ (R : ℕ → Bool → NimAudit.BinReadout.BCirc) (r s : ℕ → ℕ) (d : ℕ),
        (∀ (N : ℕ) (b : Bool), NimAudit.BinReadout.BBound (R N b) (N + 1) B (r N) d (s N)) →
          (∃ c k, ∀ (N : ℕ), s N ≤ c * (N + 1) ^ k ∧ r N ≤ c * (N + 1) ^ k) →
            ∃ η,
              NimAudit.ClassicalBoundary.Negligible η ∧
                ∀ (N : ℕ),
                  NimAudit.Prob.succCountRO B (N + 1)
                        (NimAudit.BinReadout.binReadoutOf B (N + 1) (R N)) j /
                      NimAudit.Prob.nonzeroCount B (N + 1) ≤
                    2 / (↑(2 ^ B) - 1) + η N

Exact source text, lines 472–510

472/-- ASYMPTOTIC SINGLE-CHANNEL THEOREM (thm:search-gap (i), asymptotic form), conditional473    only on the external classical input.  Fix B ≥ 2 and j < B.  Let R N b be binary474    readout formulas for N+1 heaps with BBound of FIXED depth d and size s N, index width475    r N, where s and r are polynomially bounded in N+1.  Then there is a negligible η with476      success_N ≤ 2/(2^B − 1) + η N   for every N. -/477theorem search_gap_asymptotic (hH : HastadNegl) {B j : Nat} (hj : j < B)478    (R : Nat → Bool → BCirc) (r s : Nat → Nat) (d : Nat)479    (hb : ∀ N b, BBound (R N b) (N + 1) B (r N) d (s N))480    (hpoly : ∃ c k, ∀ N, s N ≤ c * (N + 1) ^ k ∧ r N ≤ c * (N + 1) ^ k) :481    ∃ η : Nat → Rat, Negligible η ∧ ∀ N,482      succCountRO B (N + 1) (binReadoutOf B (N + 1) (R N)) j / nonzeroCount B (N + 1) ≤483        2 / (((2 ^ B : Nat) : Rat) - 1) + η N := by484  obtain ⟨c, k, hck⟩ := hpoly485  -- the premise size: 12 Upar(N+1) B ((r+1)(s+1))^10 is polynomial in N+1, hence in m ≥ N+1486  let S' : Nat → Nat := fun N => 12 * Upar (N + 1) B ((r N + 1) * (s N + 1)) ^ 10487  obtain ⟨C, K, hCK⟩ := upar_poly B c k488  have hS'le : ∀ N, S' N ≤ C * (N + 1) ^ K := by489    intro N490    refine Nat.le_trans ?_ (hCK N trivial)491    show 12 * Upar (N + 1) B ((r N + 1) * (s N + 1)) ^ 10 ≤ _492    unfold Upar493    apply Nat.mul_le_mul_left494    apply Nat.pow_le_pow_left495    apply Nat.mul_le_mul_left496    have h1 := (hck N).1; have h2 := (hck N).2497    have := Nat.mul_le_mul (show r N + 1 ≤ c * (N + 1) ^ k + 1 by omega) (show s N + 1 ≤ c * (N + 1) ^ k + 1 by omega)498    omega499  obtain ⟨δ, hδ, hcorr⟩ := hH (d + 2 + 11) C K500  refine ⟨fun N => (((2 ^ B - 1 : Nat) : Rat)) * etaSum δ B N, ?_, fun N => ?_⟩501  · exact etaSum_negligible hδ B (2 ^ B - 1)502  · have hbound := binary_readout_bound hj (R N) (hb N) (ε := etaSum δ B N) (fun m hm1 hm2 => by503      have hcl := classicalCorr_mono (hcorr m (by omega)) (show S' N ≤ C * m ^ K from504        Nat.le_trans (hS'le N) (Nat.mul_le_mul_left C (Nat.pow_le_pow_left hm1 K)))505      refine premise_mono (premise_of_classical (by omega) hcl) (Rat.le_trans (half_le_self (hδ.1 m)) ?_)506      apply term_le_rsum (fun x _ => hδ.1 x)507      simp only [List.mem_filter, List.mem_range, decide_eq_true_eq]; omega)508    have e : (((2 ^ B : Nat) : Rat) - 1) = (((2 ^ B - 1 : Nat) : Rat)) := (natCast_pred B).symm509    rw [e] at hbound ⊢510    exact hbound

Project declarations in the statement: BinReadout.BBound, BinReadout.BCirc, BinReadout.binReadoutOf, ClassicalBoundary.HastadNegl, ClassicalBoundary.Negligible, Prob.nonzeroCount, Prob.succCountRO

Project declarations used by the proof or definition body

theorem `Attain.attain_exact`

Module NimAttain (lean/phase3/NimAttain.lean, lines 563–576) · file SHA-256 dd978aa0cd3d6fe5… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

EXACT ATTAINABILITY: for B ≥ 2, any nonzero B-bit functional w, every N ≥ 1, the least-representative readout succeeds with conditional probability exactly 2/(2^B - 1).

Statement as elaborated and printed by Lean 4.26.0

∀ {B N w : ℕ},
  2 ≤ B →
    w ≠ 0 →
      w < 2 ^ B →
        NimAudit.Prob.succCount B (N + 1)
              (NimAudit.Attain.attainF (NimAudit.Attain.fibreRep B w false)
                (NimAudit.Attain.fibreRep B w true))
              w /
            NimAudit.Prob.nonzeroCount B (N + 1) =
          2 / (↑(2 ^ B) - 1)

Exact source text, lines 563–576

563/-- EXACT ATTAINABILITY: for B ≥ 2, any nonzero B-bit functional w, every N ≥ 1,564    the least-representative readout succeeds with conditional probability exactly565    2/(2^B - 1). -/566theorem attain_exact {B N w : Nat} (hB : 2 ≤ B) (hw0 : w ≠ 0) (hw : w < 2 ^ B) :567    succCount B (N + 1) (attainF (fibreRep B w false) (fibreRep B w true)) w /568        nonzeroCount B (N + 1) = 2 / (((2 ^ B : Nat) : Rat) - 1) := by569  rw [attain_count_exact hB hw0 hw, nonzeroCount_eq']570  have ht := qpow_pos B N571  have hq2 := q_ge_two (B := B) (by omega)572  generalize ((2 ^ B : Nat) : Rat) ^ N = t at *573  generalize ((2 ^ B : Nat) : Rat) = q at *574  have h1 : q - 1 ≠ 0 := by grind575  have h2 : t ≠ 0 := Rat.ne_of_gt ht576  grind

Project declarations in the statement: Attain.attainF, Attain.fibreRep, Prob.nonzeroCount, Prob.succCount

Project declarations used by the proof or definition body

Attain.attainF, Attain.attain_count_exact, Attain.fibreRep, Attain.nonzeroCount_eq', Attain.q_ge_two, Attain.qpow_pos, Prob.nonzeroCount, Prob.succCount

theorem `Attain.paper_example_two_thirds`

Module NimAttain (lean/phase3/NimAttain.lean, lines 600–609) · file SHA-256 dd978aa0cd3d6fe5… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

THE PAPER'S EXAMPLE: B = 2, head pi_0, guesses a_0 = 2, a_1 = 1, fallback "subtract 1": conditional success exactly 2/3 for every N ≥ 1.

Statement as elaborated and printed by Lean 4.26.0

∀ (N : ℕ),
  NimAudit.Prob.succCountRO 2 (N + 1) (NimAudit.Attain.attainF 2 1) 0 /
      NimAudit.Prob.nonzeroCount 2 (N + 1) =
    2 / 3

Exact source text, lines 600–609

600/-- THE PAPER'S EXAMPLE: B = 2, head pi_0, guesses a_0 = 2, a_1 = 1, fallback601    "subtract 1": conditional success exactly 2/3 for every N ≥ 1. -/602theorem paper_example_two_thirds (N : Nat) :603    succCountRO 2 (N + 1) (attainF 2 1) 0 / nonzeroCount 2 (N + 1) = 2 / 3 := by604  have := attain_exact_head (B := 2) (N := N) (j := 0) (by decide) (by decide)605  rw [rep_B2_false, rep_B2_true] at this606  rw [this]607  have e : (((2 ^ 2 : Nat) : Rat) - 1) = 3 := by608    rw [show (2 ^ 2 : Nat) = 4 from rfl]; simp; grind609  rw [e]

Project declarations in the statement: Attain.attainF, Prob.nonzeroCount, Prob.succCountRO

Project declarations used by the proof or definition body

Attain.attainF, Attain.attain_exact_head, Attain.fibreRep, Attain.rep_B2_false, Attain.rep_B2_true, Prob.headVec, Prob.nonzeroCount, Prob.succCountRO

Definitions these statements use

def `Prob.CorrHyp`

Module NimProbability (lean/phase2/NimProbability.lean, lines 541–546) · file SHA-256 1d5d7977a43e854d…

THE IMPORTED PARITY-CORRELATION PREMISE, as a predicate used only as a theorem hypothesis: |E[H_{b,a} chi_u]| ≤ η for every b, every a < q and every nonzero u < q. (Not an axiom; not proved here.)

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → NimAudit.Prob.Readout → ℚ → Prop

Exact source text, lines 541–546

541/-- THE IMPORTED PARITY-CORRELATION PREMISE, as a predicate used only as a theorem542    hypothesis: |E[H_{b,a} chi_u]| ≤ η for every b, every a < q and every nonzero543    u < q.  (Not an axiom; not proved here.) -/544def CorrHyp (B N : Nat) (F : Readout) (η : Rat) : Prop :=545  ∀ (b : Bool) (a u : Nat), a < 2 ^ B → 0 < u → u < 2 ^ B →546    -η ≤ corr B N F b a u ∧ corr B N F b a u ≤ η

Project declarations in the statement: Prob.Readout

Project declarations used by the proof or definition body

Prob.Readout, Prob.corr

def `Prob.Readout`

Module NimProbability (lean/phase2/NimProbability.lean, lines 399–402) · file SHA-256 1d5d7977a43e854d…

A readout: from board P and observed bit b, a proposed move (heap index i, new value v), or `none` (invalid output). No circuit restriction is imposed here; the only property ever used is the correlation premise `CorrHyp`.

Statement as elaborated and printed by Lean 4.26.0

Type

Exact source text, lines 399–402

399/-- A readout: from board P and observed bit b, a proposed move (heap index i, new400    value v), or `none` (invalid output).  No circuit restriction is imposed here;401    the only property ever used is the correlation premise `CorrHyp`. -/402abbrev Readout := List Nat → Bool → Option (Nat × Nat)

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `Prob.nonzeroCount`

Module NimProbability (lean/phase2/NimProbability.lean, lines 691–693) · file SHA-256 1d5d7977a43e854d…

Number of boards with sigma ≠ 0.

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → ℚ

Exact source text, lines 691–693

691/-- Number of boards with sigma ≠ 0. -/692def nonzeroCount (B N : Nat) : Rat :=693  rsum (boards (2 ^ B) N) (fun P => if nimSum P ≠ 0 then 1 else 0)

Project declarations in the statement: none

Project declarations used by the proof or definition body

Prob.boards, Prob.rsum, nimSum

def `Prob.succCount`

Module NimProbability (lean/phase2/NimProbability.lean, lines 685–689) · file SHA-256 1d5d7977a43e854d…

Number of boards with sigma ≠ 0 on which the readout, fed b = ell_w(sigma), makes a legal move to nim-sum zero.

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → NimAudit.Prob.Readout → ℕ → ℚ

Exact source text, lines 685–689

685/-- Number of boards with sigma ≠ 0 on which the readout, fed b = ell_w(sigma),686    makes a legal move to nim-sum zero. -/687def succCount (B N : Nat) (F : Readout) (w : Nat) : Rat :=688  rsum (boards (2 ^ B) N)689    (fun P => if nimSum P ≠ 0 ∧ successB F (dotB B w (nimSum P)) P = true then 1 else 0)

Project declarations in the statement: Prob.Readout

Project declarations used by the proof or definition body

Prob.Readout, Prob.boards, Prob.dotB, Prob.rsum, Prob.successB, nimSum

def `Bridge.ParityCorrPremise`

Module BitBridge (lean/phase3/BitBridge.lean, lines 449–455) · file SHA-256 000644dc271d27f9…

THE CLASSICAL PARITY-CORRELATION PREMISE (explicit hypothesis, not proved): every formula of depth ≤ d and size ≤ s reading only m inputs has correlation at most ε with parity of those m bits under the uniform distribution.

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → ℕ → ℚ → Prop

Exact source text, lines 449–455

449/-- THE CLASSICAL PARITY-CORRELATION PREMISE (explicit hypothesis, not proved):450    every formula of depth ≤ d and size ≤ s reading only m inputs has correlation451    at most ε with parity of those m bits under the uniform distribution. -/452def ParityCorrPremise (d s m : Nat) (ε : Rat) : Prop :=453  ∀ C : Circ, depth C ≤ d → size C ≤ s → maxInput C ≤ m →454    -ε ≤ rsum (bitvecs m) (fun y => ind (eval (vfun y) C) * sgn (par y)) / (2 : Rat) ^ m ∧455    rsum (bitvecs m) (fun y => ind (eval (vfun y) C) * sgn (par y)) / (2 : Rat) ^ m ≤ ε

Project declarations in the statement: none

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.depth, AC0.Circ.eval, AC0.Circ.maxInput, AC0.Circ.size, Bridge.bitvecs, Bridge.ind, Bridge.par, Bridge.sgn, Bridge.vfun, Prob.rsum

inductive `CorrBridge.RBound`

Module NimCorrBridge (lean/phase3/NimCorrBridge.lean, lines 505–517) · file SHA-256 d3fb2e4a64db3e92…

Resource hypotheses on the readout formulas.

Statement as elaborated and printed by Lean 4.26.0

NimAudit.CorrBridge.RCirc → ℕ → ℕ → ℕ → ℕ → Prop

Exact source text, lines 505–517

505/-- Resource hypotheses on the readout formulas. -/506structure RBound (R : RCirc) (N B d s : Nat) : Prop where507  sel_len : R.sel.length = N508  val_len : R.val.length = B509  depth_valid : depth R.valid ≤ d510  depth_sel : ∀ c ∈ R.sel, depth c ≤ d511  depth_val : ∀ c ∈ R.val, depth c ≤ d512  size_valid : size R.valid ≤ s513  size_sel : ∀ c ∈ R.sel, size c ≤ s514  size_val : ∀ c ∈ R.val, size c ≤ s515  max_valid : maxInput R.valid ≤ B * N516  max_sel : ∀ c ∈ R.sel, maxInput c ≤ B * N517  max_val : ∀ c ∈ R.val, maxInput c ≤ B * N

Project declarations in the statement: CorrBridge.RCirc

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.depth, AC0.Circ.maxInput, AC0.Circ.size, CorrBridge.RCirc, CorrBridge.RCirc.sel, CorrBridge.RCirc.val, CorrBridge.RCirc.valid

inductive `CorrBridge.RCirc`

Module NimCorrBridge (lean/phase3/NimCorrBridge.lean, lines 34–37) · file SHA-256 d3fb2e4a64db3e92…

Statement as elaborated and printed by Lean 4.26.0

Type

Exact source text, lines 34–37

34structure RCirc where35  valid : Circ36  sel : List Circ37  val : List Circ

Project declarations in the statement: none

Project declarations used by the proof or definition body

AC0.Circ

def `CorrBridge.Upar`

Module NimCorrBridge (lean/phase3/NimCorrBridge.lean, lines 519–520) · file SHA-256 d3fb2e4a64db3e92…

The polynomial size parameter U = (N+2)(B+2)(s+2).

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → ℕ → ℕ

Exact source text, lines 519–520

519/-- The polynomial size parameter U = (N+2)(B+2)(s+2). -/520def Upar (N B s : Nat) : Nat := (N + 2) * (B + 2) * (s + 2)

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `CorrBridge.readoutOf`

Module NimCorrBridge (lean/phase3/NimCorrBridge.lean, lines 48–54) · file SHA-256 d3fb2e4a64db3e92…

The readout computed by the circuit families R false, R true.

Statement as elaborated and printed by Lean 4.26.0

ℕ → (Bool → NimAudit.CorrBridge.RCirc) → NimAudit.Prob.Readout

Exact source text, lines 48–54

48/-- The readout computed by the circuit families R false, R true. -/49def readoutOf (B : Nat) (R : Bool → RCirc) : Readout := fun P b =>50  if eval (boardBits B P) (R b).valid then51    match firstTrue ((R b).sel.map (eval (boardBits B P))) with52    | some i => some (i, toNatBE ((R b).val.map (eval (boardBits B P))))53    | none => none54  else none

Project declarations in the statement: CorrBridge.RCirc, Prob.Readout

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.eval, Bridge.toNatBE, CorrBridge.RCirc, CorrBridge.RCirc.sel, CorrBridge.RCirc.val, CorrBridge.RCirc.valid, CorrBridge.boardBits, CorrBridge.firstTrue

def `Prob.succCountRO`

Module NimProbability (lean/phase2/NimProbability.lean, lines 933–936) · file SHA-256 1d5d7977a43e854d…

Success count when the readout is fed the ACTUAL rollout outcome RO_{pi_j}(P).

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → NimAudit.Prob.Readout → ℕ → ℚ

Exact source text, lines 933–936

933/-- Success count when the readout is fed the ACTUAL rollout outcome RO_{pi_j}(P). -/934def succCountRO (B N : Nat) (F : Readout) (j : Nat) : Rat :=935  rsum (boards (2 ^ B) N)936    (fun P => if nimSum P ≠ 0 ∧ successB F (rolloutWinner j P) P = true then 1 else 0)

Project declarations in the statement: Prob.Readout

Project declarations used by the proof or definition body

Game.rolloutWinner, Prob.Readout, Prob.boards, Prob.rsum, Prob.successB, nimSum

inductive `BinReadout.BBound`

Module BinaryReadout (lean/phase4/BinaryReadout.lean, lines 131–144) · file SHA-256 17ef1a62ba9edafb…

Resource bounds for binary readout formulas.

Statement as elaborated and printed by Lean 4.26.0

NimAudit.BinReadout.BCirc → ℕ → ℕ → ℕ → ℕ → ℕ → Prop

Exact source text, lines 131–144

131/-- Resource bounds for binary readout formulas. -/132structure BBound (R : BCirc) (N B r d s : Nat) : Prop where133  idx_len : R.idx.length = r134  val_len : R.val.length = B135  width : N ≤ 2 ^ r136  depth_valid : depth R.valid ≤ d137  depth_idx : ∀ c ∈ R.idx, depth c ≤ d138  depth_val : ∀ c ∈ R.val, depth c ≤ d139  size_valid : size R.valid ≤ s140  size_idx : ∀ c ∈ R.idx, size c ≤ s141  size_val : ∀ c ∈ R.val, size c ≤ s142  max_valid : maxInput R.valid ≤ B * N143  max_idx : ∀ c ∈ R.idx, maxInput c ≤ B * N144  max_val : ∀ c ∈ R.val, maxInput c ≤ B * N

Project declarations in the statement: BinReadout.BCirc

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.depth, AC0.Circ.maxInput, AC0.Circ.size, BinReadout.BCirc, BinReadout.BCirc.idx, BinReadout.BCirc.val, BinReadout.BCirc.valid

inductive `BinReadout.BCirc`

Module BinaryReadout (lean/phase4/BinaryReadout.lean, lines 24–28) · file SHA-256 17ef1a62ba9edafb…

Binary readout formulas for one observed bit.

Statement as elaborated and printed by Lean 4.26.0

Type

Exact source text, lines 24–28

24/-- Binary readout formulas for one observed bit. -/25structure BCirc where26  valid : Circ27  idx : List Circ28  val : List Circ

Project declarations in the statement: none

Project declarations used by the proof or definition body

AC0.Circ

def `BinReadout.binReadoutOf`

Module BinaryReadout (lean/phase4/BinaryReadout.lean, lines 30–37) · file SHA-256 17ef1a62ba9edafb…

The readout defined by binary readout formulas (index ≥ N is invalid).

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → (Bool → NimAudit.BinReadout.BCirc) → NimAudit.Prob.Readout

Exact source text, lines 30–37

30/-- The readout defined by binary readout formulas (index ≥ N is invalid). -/31def binReadoutOf (B N : Nat) (R : Bool → BCirc) : Readout := fun P b =>32  if eval (boardBits B P) (R b).valid then33    if toNatBE ((R b).idx.map (eval (boardBits B P))) < N then34      some (toNatBE ((R b).idx.map (eval (boardBits B P))),35        toNatBE ((R b).val.map (eval (boardBits B P))))36    else none37  else none

Project declarations in the statement: BinReadout.BCirc, Prob.Readout

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.eval, BinReadout.BCirc, BinReadout.BCirc.idx, BinReadout.BCirc.val, BinReadout.BCirc.valid, Bridge.toNatBE, CorrBridge.boardBits

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 `ClassicalBoundary.Negligible`

Module Classical (lean/phase6/Classical.lean, lines 271–273) · file SHA-256 ee9d365e1611d40c…

Negligible nonnegative rational sequence: below every inverse polynomial eventually.

Statement as elaborated and printed by Lean 4.26.0

(ℕ → ℚ) → Prop

Exact source text, lines 271–273

271/-- Negligible nonnegative rational sequence: below every inverse polynomial eventually. -/272def Negligible (f : Nat → Rat) : Prop :=273  (∀ n, 0 ≤ f n) ∧ ∀ k : Nat, ∃ n0 : Nat, ∀ n, n0 ≤ n → f n * ((n : Rat) + 1) ^ k ≤ 1

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `Attain.attainF`

Module NimAttain (lean/phase3/NimAttain.lean, lines 38–42) · file SHA-256 dd978aa0cd3d6fe5…

Attainability readout with guesses a_0 (observed bit false) and a_1 (true).

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → NimAudit.Prob.Readout

Exact source text, lines 38–42

38/-- Attainability readout with guesses a_0 (observed bit false) and a_1 (true). -/39def attainF (a0 a1 : Nat) : Readout := fun P b =>40  match cancelIdx (if b then a1 else a0) P with41  | some m => some m42  | none => decIdx P

Project declarations in the statement: Prob.Readout

Project declarations used by the proof or definition body

Attain.cancelIdx, Attain.decIdx

def `Attain.fibreRep`

Module NimAttain (lean/phase3/NimAttain.lean, lines 327–328) · file SHA-256 dd978aa0cd3d6fe5…

Least nonzero B-bit value in the fibre ell = b (0 if none).

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → Bool → ℕ

Exact source text, lines 327–328

327/-- Least nonzero B-bit value in the fibre ell = b (0 if none). -/328def fibreRep (B w : Nat) (b : Bool) : Nat := (findLeast (inFibre B w b) (2 ^ B)).getD 0

Project declarations in the statement: none

Project declarations used by the proof or definition body

Attain.findLeast, Attain.inFibre

Full modules

Module	File	Lines	Imports
BinaryReadout	`lean/phase4/BinaryReadout.lean`	333	FiniteNet, NimCorrBridge
BitBridge	`lean/phase3/BitBridge.lean`	560	Circuit
Classical	`lean/phase6/Classical.lean`	587	Bypass
NimAttain	`lean/phase3/NimAttain.lean`	673	NimProbability
NimCorrBridge	`lean/phase3/NimCorrBridge.lean`	922	BitBridge
NimProbability	`lean/phase2/NimProbability.lean`	1074	NimGame

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).

Appendix HFull proof of Theorem 5.12: uniform σ, character expansion, finite bound, Håstad input, attainability

1 Paper text

Appendix H. Proof of Theorem 5.12

2 Explain this

3 How this is formalised

4 Lean statement and source

Principal declarations

theorem Prob.success_bound

theorem CorrBridge.circuit_readout_bound

theorem ClassicalBoundary.search_gap_asymptotic

theorem Attain.attain_exact

theorem Attain.paper_example_two_thirds

Definitions these statements use

def Prob.CorrHyp

def Prob.Readout

def Prob.nonzeroCount

def Prob.succCount

def Bridge.ParityCorrPremise

inductive CorrBridge.RBound

inductive CorrBridge.RCirc

def CorrBridge.Upar

def CorrBridge.readoutOf

def Prob.succCountRO

inductive BinReadout.BBound

inductive BinReadout.BCirc

def BinReadout.binReadoutOf

def ClassicalBoundary.HastadNegl

def ClassicalBoundary.Negligible

def Attain.attainF

def Attain.fibreRep

Full modules

theorem `Prob.success_bound`

theorem `CorrBridge.circuit_readout_bound`

theorem `ClassicalBoundary.search_gap_asymptotic`

theorem `Attain.attain_exact`

theorem `Attain.paper_example_two_thirds`

def `Prob.CorrHyp`

def `Prob.Readout`

def `Prob.nonzeroCount`

def `Prob.succCount`

def `Bridge.ParityCorrPremise`

inductive `CorrBridge.RBound`

inductive `CorrBridge.RCirc`

def `CorrBridge.Upar`

def `CorrBridge.readoutOf`

def `Prob.succCountRO`

inductive `BinReadout.BBound`

inductive `BinReadout.BCirc`

def `BinReadout.binReadoutOf`

def `ClassicalBoundary.HastadNegl`

def `ClassicalBoundary.Negligible`

def `Attain.attainF`

def `Attain.fibreRep`