Section 2.1, paragraph 6A one-step recurrence h_{r+1}=h_r⊕x_r accumulates parity over an arbitrarily long stream

A recurrent update that looks only at its previous state is still very powerful if it is allowed to run for many steps. The update $h_{r+1}=h_r\oplus x_r$ consults one previous state, yet after $n$ steps $h_n$ is the parity of all inputs, which no AC⁰ circuit computes.

So the right restriction for the simulation theorem is on the total number of unrolled steps $T$, not on how far back each update looks. Section 5.5 uses exactly this loophole on purpose: it lets the number of updates grow with the number of heaps.

scan_invariant proves that folding XOR over a list of rows from an initial value gives that value XOR the nim-sum of the rows, for any length: a one-step dependency accumulates the global XOR. A single update is shallow: Recurrent.circuit_resources bounds one recurrent update by depth 4 and size $28B+8$. The bounded-unrolling restriction under which the simulation theorem does apply is Definition A.2.

Principal declarations

∀ (rows : List ℕ) (initial : ℕ), NimAudit.scan initial rows = initial ^^^ NimAudit.nimSum rows

26theorem scan_invariant (rows : List Nat) (initial : Nat) :27    scan initial rows = initial ^^^ nimSum rows := by28  induction rows generalizing initial with29  | nil => simp [scan, nimSum]30  | cons h t ih =>31    change scan (initial ^^^ h) t = initial ^^^ (h ^^^ nimSum t)32    rw [ih, Nat.xor_assoc]

∀ (B k : ℕ),
  (NimAudit.Recurrent.accC B k).depth ≤ 4 ∧
    (NimAudit.Recurrent.prevC B k).depth ≤ 4 ∧
      (NimAudit.Recurrent.validC B).depth ≤ 4 ∧
        (NimAudit.Recurrent.diffC B k).depth ≤ 4 ∧
          (NimAudit.Recurrent.diffValidC B).depth ≤ 4 ∧
            (NimAudit.Recurrent.accC B k).size + (NimAudit.Recurrent.prevC B k).size +
                  (NimAudit.Recurrent.diffC B k).size ≤
                28 ∧
              (NimAudit.Recurrent.validC B).size + (NimAudit.Recurrent.diffValidC B).size ≤ 8

491/-- Per-update circuit resources: depth ≤ 4, total size ≤ 28 B + 8 for all492    state and output bits (constant depth, O(B) size). -/493theorem circuit_resources (B k : Nat) :494    depth (accC B k) ≤ 4 ∧ depth (prevC B k) ≤ 4 ∧ depth (validC B) ≤ 4 ∧495    depth (diffC B k) ≤ 4 ∧ depth (diffValidC B) ≤ 4 ∧496    size (accC B k) + size (prevC B k) + size (diffC B k) ≤ 28 ∧497    size (validC B) + size (diffValidC B) ≤ 8 := by498  simp [accC, prevC, validC, diffC, diffValidC, xorC, listMax]

Definitions these statements use

ℕ → List ℕ → ℕ

11def scan (initial : Nat) (rows : List Nat) : Nat :=12  rows.foldl (fun acc row => acc ^^^ row) initial

List ℕ → ℕ

7def nimSum : List Nat → Nat8  | [] => 09  | h :: t => h ^^^ nimSum t

NimAudit.AC0.Circ → ℕ

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

NimAudit.AC0.Circ → ℕ

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

ℕ → ℕ → NimAudit.AC0.Circ

388def accC (B k : Nat) : Circ := and [input (2 * B + 1), xorC (input k) (input (2 * B + 2 + k))]

ℕ → ℕ → NimAudit.AC0.Circ

392def diffC (B k : Nat) : Circ := xorC (input (B + k)) (input k)

ℕ → NimAudit.AC0.Circ

393def diffValidC (B : Nat) : Circ := and [input (2 * B), not (input (2 * B + 1))]

ℕ → ℕ → NimAudit.AC0.Circ

389def prevC (B k : Nat) : Circ :=390  or [and [input (2 * B + 1), input (B + k)], and [not (input (2 * B + 1)), input k]]

ℕ → NimAudit.AC0.Circ

391def validC (B : Nat) : Circ := or [input (2 * B), not (input (2 * B + 1))]

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