NIM paper · interactive edition Interactive edition · paper, explanations and Lean proofs.

Theorem 5.12 (i)One structured head plus an AC0 readout wins with probability at most 2/(2^B−1)+negl(N)

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

1 Paper text

Theorem 5.12 (Restricted bound and bypasses) The following statements hold under Definition 5.7.

  1. (i) For each fixed B≥2B\ge2, let PP be uniform on {0,…,2B−1}N\{0,\ldots,2^B-1\}^N conditional on σ(P)≠0\sigma(P)\ne0. For one fixed structured head πj\pi_j and an AC0\AC^0 readout FN(P,ROπj(P))F_N(P,\mathrm{RO}_{\pi_j}(P)), winning-move success is at most 22B−1+negl⁡(N).\frac{2}{2^B-1}+\operatorname{negl}(N). Here N≥1N\ge1, and a negligible error is a nonnegative sequence smaller than every inverse polynomial for sufficiently large NN, with circuit depth, polynomial size exponent and BB fixed. More precisely, a uniform parity-correlation bound ηN\eta_N for the fixed-bit readout indicators gives the finite upper bound 2/(2B−1)+(2B−1)ηN2/(2^B-1)+(2^B-1)\eta_N; the indicators and correlation premise are specified in Appendix H. The leading constant is asymptotically attainable by guessing one nonzero nim-sum in each channel fibre.

  2. (ii) For any BB, the BB structured heads and an AC0\AC^0 readout select an optimal move using O(BN2B)O(BN2^B) rollout steps, as in Proposition 5.9.

  3. (iii) Given a legal transition from a known zero-nim-sum predecessor, a two-frame AC0\AC^0 selector restores zero. Once a player has established that invariant, it maintains it against every legal opponent response. This statement does not supply the initial winning move from an arbitrary position.

Generated from paper_jmlr.tex, lines 802–814.

2 Explain this

The setting. Boards are uniformly random NN-heap boards with BB-bit heaps, conditioned on being winning (σ≠0\sigma\ne0). The agent observes one structured channel β=ROπj(P)\beta=\mathrm{RO}_{\pi_j}(P) and must output a move with a shallow circuit FN(P,β)F_N(P,\beta).

The bound. Its chance of playing a winning move is at most 2/(2B−1)2/(2^B-1) plus a quantity that vanishes faster than any inverse polynomial in NN. For B=2B=2 that is about 2/32/3; for B=4B=4 about 0.130.13.

Intuition. Knowing one linear bit ℓ(σ)\ell(\sigma) narrows the 2B−12^B-1 possible nonzero nim-sums to a fibre of about half of them. A shallow readout has essentially no correlation with the remaining parity information, so the best it can do is guess one value per fibre: two lucky values out of 2B−12^B-1.

Attainability. Guessing one nonzero value in each fibre achieves 2/(2B−1)2/(2^B-1) exactly, so the constant is right.

Caveats. Fixed BB; this distribution; this interface. The negligible term rests on Håstad's parity-correlation bound, used as the named external input HastadNegl. It is not a bound on general single-policy search or on MCTS.

3 How this is formalised

Finite part, no classical input. Prob.success_bound: for every readout and every η\eta, the correlation premise Prob.CorrHyp (∣E[Hb,aχu]∣≤η|\mathbb E[H_{b,a}\chi_u]|\le\eta for all observed bits bb, values aa and nonzero uu) implies conditional success at most 2/(q−1)+(q−1)η2/(q-1)+(q-1)\eta, q=2Bq=2^B.

From circuits to the premise. CorrBridge.circuit_readout_bound: for readouts given by formulas of depth dd and size ss, the premise follows from the parity-correlation premise for formulas of depth d+11d+11 and polynomially larger size on every support size between N+1N+1 and B(N+1)B(N+1), where Lean indexes boards by N+1N+1 heaps (so this is NN to BNBN in the paper's notation); restriction and averaging are checked.

Asymptotic part, named classical input. ClassicalBoundary.search_gap_asymptotic: assuming ClassicalBoundary.HastadNegl, for fixed B≥2B\ge2, j<Bj<B and readout families of fixed depth and polynomial size there is a negligible η\eta (ClassicalBoundary.Negligible) with success at most 2/(2B−1)+η(N)2/(2^B-1)+\eta(N). ClassicalBoundary.search_gap_asymptotic_net is the same for fixed-scale network readouts.

Attainability. Attain.attain_exact: for B≥2B\ge2 and any nonzero functional, the least-representative readout succeeds with conditional probability exactly 2/(2B−1)2/(2^B-1), for every N≥1N\ge1.

Boundary. The analytic derivation of Håstad's correlation bound is external. Everything that applies it to this paper (indicators, restrictions, conditioning, the probability calculation) is checked.

Coverage record
Paper anchorthm:search-gap (manuscript label)
Displayed asTheorem 5.12 (i)
ClaimOne structured head plus an AC0 readout wins with probability at most 2/(2^B−1)+negl(N)
Coverage categoryChecked conditional theorem using named classical input
Statement sourcepaper_jmlr.tex lines 802–814; SHA-256 of the normalised block source 6a8c9a4107356a14…
Lean declarations
Named classical inputsHastadNegl
Assumptions and domain

Fixed B≥2B\ge2; boards uniform on {0,…,2B−1}N\{0,\dots,2^B-1\}^N conditioned on σ≠0\sigma\ne0; one fixed structured head; readout circuits of fixed depth and polynomial size (or fixed-scale networks of fixed depth).

Prose-to-formal notes

The finite bound holds under the explicit correlation premise CorrHyp (proved without any classical input). The asymptotic form uses the named input HastadNegl, from which the premise is derived for the readout indicators; the analytic derivation of Håstad's bound is external. Attainability of 2/(2B−1)2/(2^B-1) is proved exactly.

Depends onDefinition 5.7, Proposition 5.10, Equation (H.1)
Audited correspondence rowsthm:search-gap
Explanationsexplain/thm:search-gap.i, formal/thm:search-gap.i
Build evidencefresh 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

BinReadout.BBound, BinReadout.BCirc, BinReadout.binReadoutOf, BinReadout.binary_readout_bound, ClassicalBoundary.ClassicalCorr, ClassicalBoundary.HastadNegl, ClassicalBoundary.Negligible, ClassicalBoundary.classicalCorr_mono, ClassicalBoundary.etaSum, ClassicalBoundary.etaSum_negligible, ClassicalBoundary.half_le_self, ClassicalBoundary.premise_mono, ClassicalBoundary.premise_of_classical, ClassicalBoundary.term_le_rsum, ClassicalBoundary.upar_poly, CorrBridge.Upar, Family.PolyIn, Prob.natCast_pred, Prob.nonzeroCount, Prob.succCountRO

theorem ClassicalBoundary.search_gap_asymptotic_net

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

The same for readouts computed by fixed-scale threshold networks (W, L fixed, polynomial widths), compiled by the finite-input compiler.

Statement as elaborated and printed by Lean 4.26.0

NimAudit.ClassicalBoundary.HastadNegl →
  ∀ {B j W L : ℕ},
    j < B →
      ∀ (nets : ℕ → Bool → List NimAudit.AC0.Layer) (r : ℕ → ℕ),
        (∀ (N : ℕ) (b : Bool), (nets N b).length ≤ L) →
          (∀ (N : ℕ) (b : Bool), NimAudit.AC0.NetValid W (nets N b)) →
            (∀ (N : ℕ), N + 1 ≤ 2 ^ r N) →
              (∃ c k,
                  ∀ (N : ℕ) (b : Bool),
                    NimAudit.AC0.NetBounded (c * (N + 1) ^ k) (nets N b) ∧ r N ≤ c * (N + 1) ^ k) →
                ∃ η,
                  NimAudit.ClassicalBoundary.Negligible η ∧
                    ∀ (N : ℕ),
                      NimAudit.Prob.succCountRO B (N + 1)
                            (NimAudit.BinReadout.binReadoutOf B (N + 1) fun b =>
                              NimAudit.BinReadout.netBCirc W B (N + 1) (r N) (nets N b))
                            j /
                          NimAudit.Prob.nonzeroCount B (N + 1) ≤
                        2 / (↑(2 ^ B) - 1) + η N
Exact source text, lines 512–538
512/-- The same for readouts computed by fixed-scale threshold networks (W, L fixed,513    polynomial widths), compiled by the finite-input compiler. -/514theorem search_gap_asymptotic_net (hH : HastadNegl) {B j W L : Nat} (hj : j < B)515    (nets : Nat → Bool → List Layer) (r : Nat → Nat) (hlen : ∀ N b, (nets N b).length ≤ L)516    (hv : ∀ N b, NetValid W (nets N b)) (hr : ∀ N, N + 1 ≤ 2 ^ r N)517    (hpoly : ∃ c k, ∀ N b, NetBounded (c * (N + 1) ^ k) (nets N b) ∧ r N ≤ c * (N + 1) ^ k) :518    ∃ η : Nat → Rat, Negligible η ∧ ∀ N,519      succCountRO B (N + 1) (binReadoutOf B (N + 1) (fun b => netBCirc W B (N + 1) (r N) (nets N b))) j /520          nonzeroCount B (N + 1) ≤ 2 / (((2 ^ B : Nat) : Rat) - 1) + η N := by521  obtain ⟨c, k, hck⟩ := hpoly522  let s : Nat → Nat := fun N => 2 * ((2 * W + 3) ^ L * (c * (N + 1) ^ k + 1) ^ (W * L))523  apply search_gap_asymptotic hH hj (fun N b => netBCirc W B (N + 1) (r N) (nets N b)) r s (3 * L)524  · intro N b525    have hb := netBCirc_BBound (B := B) (N := N + 1) (r := r N) (nets N b) (hv N b) (hck N b).1 (hr N)526    have hl := hlen N b527    refine bbound_mono hb (Nat.mul_le_mul_left 3 hl) ?_528    have e1 : (2 * W + 3) ^ (nets N b).length ≤ (2 * W + 3) ^ L := Nat.pow_le_pow_right (by omega) hl529    have e2 : (c * (N + 1) ^ k + 1) ^ (W * (nets N b).length) ≤ (c * (N + 1) ^ k + 1) ^ (W * L) :=530      Nat.pow_le_pow_right (by omega) (Nat.mul_le_mul_left W hl)531    have := Nat.mul_le_mul e1 e2532    show 2 * ((2 * W + 3) ^ (nets N b).length * (c * (N + 1) ^ k + 1) ^ (W * (nets N b).length)) ≤ s N533    simp only [s]; omega534  · obtain ⟨C, K, hCK⟩ := netsize_poly W L c k535    refine ⟨C, K, fun N => ⟨?_, ?_⟩⟩536    · have h1 := hCK N trivial; dsimp only at h1537      show 2 * ((2 * W + 3) ^ L * (c * (N + 1) ^ k + 1) ^ (W * L)) ≤ C * (N + 1) ^ K; omega538    · have h1 := hCK N trivial; have h2 := (hck N false).2; dsimp only at h1; omega

Project declarations in the statement: AC0.Layer, AC0.NetBounded, AC0.NetValid, BinReadout.binReadoutOf, BinReadout.netBCirc, ClassicalBoundary.HastadNegl, ClassicalBoundary.Negligible, Prob.nonzeroCount, Prob.succCountRO

Project declarations used by the proof or definition body

AC0.Layer, AC0.NetBounded, AC0.NetValid, Barrier.bbound_mono, BinReadout.BBound, BinReadout.binReadoutOf, BinReadout.netBCirc, BinReadout.netBCirc_BBound, ClassicalBoundary.HastadNegl, ClassicalBoundary.Negligible, ClassicalBoundary.netsize_poly, ClassicalBoundary.search_gap_asymptotic, Family.PolyIn, Prob.nonzeroCount, Prob.succCountRO

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

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 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 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 AC0.Layer

Module Circuit (lean/phase3/Circuit.lean, lines 743–744) · file SHA-256 af97cc0eec7d8464…

A layer: a list of gates reading the previous layer's outputs (indexed by Nat).

Statement as elaborated and printed by Lean 4.26.0

Type
Exact source text, lines 743–744
743/-- A layer: a list of gates reading the previous layer's outputs (indexed by Nat). -/744abbrev Layer := List Gate

Project declarations in the statement: none

Project declarations used by the proof or definition body

AC0.Gate

def AC0.NetBounded

Module Circuit (lean/phase3/Circuit.lean, lines 768–769) · file SHA-256 af97cc0eec7d8464…

Fan-in and width bounded by M.

Statement as elaborated and printed by Lean 4.26.0

ℕ → List NimAudit.AC0.Layer → Prop
Exact source text, lines 768–769
768/-- Fan-in and width bounded by M. -/769def NetBounded (M : Nat) (ls : List Layer) : Prop := ∀ l ∈ ls, l.length ≤ M ∧ ∀ g ∈ l, g.fanin ≤ M

Project declarations in the statement: AC0.Layer

Project declarations used by the proof or definition body

AC0.Gate, AC0.Gate.fanin, AC0.Layer

def AC0.NetValid

Module Circuit (lean/phase3/Circuit.lean, lines 765–766) · file SHA-256 af97cc0eec7d8464…

All gates valid for W.

Statement as elaborated and printed by Lean 4.26.0

ℕ → List NimAudit.AC0.Layer → Prop
Exact source text, lines 765–766
765/-- All gates valid for W. -/766def NetValid (W : Nat) (ls : List Layer) : Prop := ∀ l ∈ ls, ∀ g ∈ l, Gate.Valid W g

Project declarations in the statement: AC0.Layer

Project declarations used by the proof or definition body

AC0.Gate, AC0.Gate.Valid, AC0.Layer

def BinReadout.netBCirc

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

Output layout of a readout network: output 0 = valid, outputs 1..r = index bits, outputs r+1..r+B = value bits; compiled with the finite-input compiler on the B·N board bits.

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → ℕ → ℕ → List NimAudit.AC0.Layer → NimAudit.BinReadout.BCirc
Exact source text, lines 228–233
228/-- Output layout of a readout network: output 0 = valid, outputs 1..r = index bits,229    outputs r+1..r+B = value bits; compiled with the finite-input compiler on the230    B·N board bits. -/231def netBCirc (W B N r : Nat) (ls : List Layer) : BCirc :=232  ⟨netFormula W (B * N) ls 0, (List.range r).map (fun q => netFormula W (B * N) ls (1 + q)),233   (List.range B).map (fun p => netFormula W (B * N) ls (1 + r + p))⟩

Project declarations in the statement: AC0.Layer, BinReadout.BCirc

Project declarations used by the proof or definition body

AC0.Circ, AC0.Layer, BinReadout.BCirc.mk, FiniteNet.netFormula

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

ModuleFileLinesImports
BinaryReadoutlean/phase4/BinaryReadout.lean333FiniteNet, NimCorrBridge
BitBridgelean/phase3/BitBridge.lean560Circuit
Circuitlean/phase3/Circuit.lean1151NimProbability
Classicallean/phase6/Classical.lean587Bypass
NimAttainlean/phase3/NimAttain.lean673NimProbability
NimCorrBridgelean/phase3/NimCorrBridge.lean922BitBridge
NimProbabilitylean/phase2/NimProbability.lean1074NimGame

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