Remark 2.3 (local XOR)XOR of a constant number of bits or B-bit blocks is computable in AC⁰

Checked theorem Lean checks a formal statement corresponding to this claim.

1 Paper text

Remark 2.3 (Local vs. global parity) When we say “parity is hard” we mean global parity across the full Boolean input of length $n=NB$ . In contrast, parity on $O(1)$ bits is trivial in $\AC^0$ (hardwire the truth table), and more generally XOR of a constant number of $B$ -bit blocks is $\AC^0$ -computable. This local/global separation underlies both the two-frame bypass via the nimber difference $\Delta(P,P')$ and the recurrent bypass, which composes local XOR updates over a growing number of steps.

Generated from paper_jmlr.tex, lines 329–334.

2 Explain this

"Parity is hard" always means global parity of all $n=NB$ input bits. Parity of a constant number of bits is easy: a fixed truth table, or a short chain of two-input XORs. Bitwise XOR of a constant number $t$ of $B$ -bit blocks is equally easy, since each output bit is the XOR of $t$ bits.

This is what both bypasses exploit: the two-frame difference XORs two heaps, and the recurrent update XORs the accumulator with one row.

3 How this is formalised

Windows.xorChain_res: XOR of $t$ formulas of depth at most $d$ and size at most $s$ has depth at most $d+3t$ and size at most $6^t(s+1)$ . Windows.blockXor_res: bitwise XOR of $t$ blocks has depth at most $3t$ and size at most $2\cdot6^t$ . For fixed $t$ these are constants.

Coverage record
Paper anchor	`rem:local-vs-global-parity` (manuscript label)
Displayed as	Remark 2.3 (local XOR)
Claim	XOR of a constant number of bits or B-bit blocks is computable in AC⁰
Coverage category	Checked theorem
Statement source	paper_jmlr.tex lines 329–334; SHA-256 of the normalised block source `521cad39a13ca6cb…`
Lean declarations	`NimAudit.Windows.blockXor_res` (Windows, lines 233–236, file `ff59ec8bf0a0…`) `NimAudit.Windows.xorChain_res` (Windows, lines 213–228, file `ff59ec8bf0a0…`)
Audited correspondence rows	`rem:local-vs-global-parity`
Explanations	`explain/rem:local-vs-global-parity.local`, `formal/rem:local-vs-global-parity.local`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

Principal declarations

theorem `Windows.blockXor_res`

Module Windows (lean/phase6/Windows.lean, lines 233–236) · file SHA-256 ff59ec8bf0a0de70… Axioms reported by the fresh build: propext, Quot.sound

Statement as elaborated and printed by Lean 4.26.0

∀ (B t q : ℕ),
  (NimAudit.Windows.blockXor B t q).depth ≤ 3 * t ∧
    (NimAudit.Windows.blockXor B t q).size ≤ 6 ^ t * 2

Exact source text, lines 233–236

233theorem blockXor_res (B t q : Nat) : depth (blockXor B t q) ≤ 3 * t ∧ size (blockXor B t q) ≤ 6 ^ t * 2 := by234  have := xorChain_res (d := 0) (s := 1) (by decide) ((List.range t).map (fun k => input (B * k + q)))235    (fun c hc => by obtain ⟨k, _, rfl⟩ := List.mem_map.mp hc; simp)236  simpa [blockXor] using this

Project declarations in the statement: AC0.Circ.depth, AC0.Circ.size, Windows.blockXor

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.depth, AC0.Circ.depth_input, AC0.Circ.input, AC0.Circ.size, AC0.Circ.size_input, Windows.blockXor, Windows.xorChain, Windows.xorChain_res

theorem `Windows.xorChain_res`

Module Windows (lean/phase6/Windows.lean, lines 213–228) · file SHA-256 ff59ec8bf0a0de70… Axioms reported by the fresh build: propext, Quot.sound

XOR of t formulas of depth ≤ d and size ≤ s (s ≥ 1): depth ≤ d + 3t, size ≤ 6^t (s + 1).

Statement as elaborated and printed by Lean 4.26.0

∀ {d s : ℕ},
  1 ≤ s →
    ∀ (cs : List NimAudit.AC0.Circ),
      (∀ c ∈ cs, c.depth ≤ d ∧ c.size ≤ s) →
        (NimAudit.Windows.xorChain cs).depth ≤ d + 3 * cs.length ∧
          (NimAudit.Windows.xorChain cs).size ≤ 6 ^ cs.length * (s + 1)

Exact source text, lines 213–228

213/-- XOR of t formulas of depth ≤ d and size ≤ s (s ≥ 1): depth ≤ d + 3t, size ≤ 6^t (s + 1). -/214theorem xorChain_res {d s : Nat} (hs : 1 ≤ s) : ∀ cs : List Circ, (∀ c ∈ cs, depth c ≤ d ∧ size c ≤ s) →215    depth (xorChain cs) ≤ d + 3 * cs.length ∧ size (xorChain cs) ≤ 6 ^ cs.length * (s + 1)216  | [], _ => by simp [xorChain]217  | c :: cs, h => by218    obtain ⟨ih1, ih2⟩ := xorChain_res hs cs (fun c' hc' => h c' (by simp [hc']))219    obtain ⟨hd, hsz⟩ := h c (by simp)220    obtain ⟨x1, x2, _⟩ := RolloutExec.xor2_res c (xorChain cs)221    simp only [xorChain, List.length_cons]222    refine ⟨by omega, ?_⟩223    rw [x2, Nat.pow_succ]224    have hp : 1 ≤ 6 ^ cs.length := Nat.one_le_pow _ _ (by decide)225    have : s + 1 ≤ 6 ^ cs.length * (s + 1) := Nat.le_mul_of_pos_left _ (by omega)226    have e : 6 ^ cs.length * 6 * (s + 1) = 6 * (6 ^ cs.length * (s + 1)) := by227      rw [Nat.mul_comm (6 ^ cs.length) 6, Nat.mul_assoc]228    rw [e]; omega

Project declarations in the statement: AC0.Circ, AC0.Circ.depth, AC0.Circ.size, Windows.xorChain

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.const, AC0.Circ.depth, AC0.Circ.depth_const, AC0.Circ.maxInput, AC0.Circ.size, AC0.Circ.size_const, CorrBridge.xor2, RolloutExec.xor2_res, Windows.xorChain

Definitions these statements use

def `Windows.blockXor`

Module Windows (lean/phase6/Windows.lean, lines 230–231) · file SHA-256 ff59ec8bf0a0de70…

Bitwise XOR of t blocks of B bits (block k occupies inputs B·k .. B·k + B − 1).

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → ℕ → NimAudit.AC0.Circ

Exact source text, lines 230–231

230/-- Bitwise XOR of t blocks of B bits (block k occupies inputs B·k .. B·k + B − 1). -/231def blockXor (B t q : Nat) : Circ := xorChain ((List.range t).map (fun k => input (B * k + q)))

Project declarations in the statement: AC0.Circ

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.input, Windows.xorChain

def `Windows.xorChain`

Module Windows (lean/phase6/Windows.lean, lines 204–207) · file SHA-256 ff59ec8bf0a0de70…

XOR of a list of formulas (by repeated two-input XOR).

Statement as elaborated and printed by Lean 4.26.0

List NimAudit.AC0.Circ → NimAudit.AC0.Circ

Exact source text, lines 204–207

204/-- XOR of a list of formulas (by repeated two-input XOR). -/205def xorChain : List Circ → Circ206  | [] => const false207  | c :: cs => CorrBridge.xor2 c (xorChain cs)

Project declarations in the statement: AC0.Circ

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.const, CorrBridge.xor2

def `AC0.Circ.depth`

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

Statement as elaborated and printed by Lean 4.26.0

NimAudit.AC0.Circ → ℕ

Exact source text, lines 61–66

61def depth : Circ → Nat62  | input _ => 063  | const _ => 064  | not c => depth c + 165  | and cs => listMax (cs.attach.map (fun ⟨c, _⟩ => depth c)) + 166  | or cs => listMax (cs.attach.map (fun ⟨c, _⟩ => depth c)) + 1

Project declarations in the statement: AC0.Circ

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.and, AC0.Circ.casesOn, AC0.Circ.const, AC0.Circ.input, AC0.Circ.listMax, AC0.Circ.not, AC0.Circ.or, AC0.Circ.rec, AC0.Circ.rec_1

def `AC0.Circ.size`

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

Statement as elaborated and printed by Lean 4.26.0

NimAudit.AC0.Circ → ℕ

Exact source text, lines 51–56

51def size : Circ → Nat52  | input _ => 153  | const _ => 154  | not c => size c + 155  | and cs => (cs.attach.map (fun ⟨c, _⟩ => size c)).sum + 156  | or cs => (cs.attach.map (fun ⟨c, _⟩ => size c)).sum + 1

Project declarations in the statement: AC0.Circ

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.and, AC0.Circ.casesOn, AC0.Circ.const, AC0.Circ.input, AC0.Circ.not, AC0.Circ.or, AC0.Circ.rec, AC0.Circ.rec_1

inductive `AC0.Circ`

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

Statement as elaborated and printed by Lean 4.26.0

Type

Exact source text, lines 35–40

35inductive Circ where36  | input (i : Nat)37  | const (b : Bool)38  | not (c : Circ)39  | and (cs : List Circ)40  | or (cs : List Circ)

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

Full modules

Module	File	Lines	Imports
Circuit	`lean/phase3/Circuit.lean`	1151	NimProbability
Windows	`lean/phase6/Windows.lean`	261	Bypass

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

Remark 2.3 (local XOR)XOR of a constant number of bits or B-bit blocks is computable in AC0

1 Paper text

2 Explain this

3 How this is formalised

4 Lean statement and source

Principal declarations

theorem Windows.blockXor_res

theorem Windows.xorChain_res

Definitions these statements use

def Windows.blockXor

def Windows.xorChain

def AC0.Circ.depth

def AC0.Circ.size

inductive AC0.Circ

Full modules

Remark 2.3 (local XOR)XOR of a constant number of bits or B-bit blocks is computable in AC⁰

theorem `Windows.blockXor_res`

theorem `Windows.xorChain_res`

def `Windows.blockXor`

def `Windows.xorChain`

def `AC0.Circ.depth`

def `AC0.Circ.size`

inductive `AC0.Circ`