Section 5.4, “Depth amplification”Iterating an AC⁰ policy for L game steps gives a depth-Θ(L) computation

Informal interpretation Motivation, interpretation or scope; not a formal claim.

1 Paper text

Depth amplification. Although a single $\AC^0$ circuit cannot compute parity, iterating an $\AC^0$ policy for $L$ game steps yields an effective depth $\Theta(L)$ computation, which can reveal parity information. The next proposition makes this explicit by exhibiting $B$ simple $\AC^0$ rollout heads whose outcomes recover all $B$ bits of the nim-sum.

Generated from paper_jmlr.tex, lines 727–729.

2 Explain this

A single shallow circuit cannot compute parity, but running a shallow policy for $L$ game steps is a computation of depth proportional to $L$ . That is how rollouts can reveal parity information: the depth comes from time.

Caveat: depth by itself does not prove anything. That the complete rollout procedure is not an AC⁰ family is a separate, conditional result (Section 5.6, paragraph 1), even though each step is shallow.

Multi-head rollouts and the outer controller, tick by tick

Exact construction trace Every value is computed from the construction’s definitions for the example shown.

Policy $\pi_j$ subtracts $2^j$ from the first heap of size at least $2^j$ , and otherwise subtracts 1 from the first nonzero heap. A rollout lets both simulated players follow $\pi_j$ until no move is left; its outcome bit is the parity of the number of moves. Step through the outer controller one tick at a time: it resets, runs head 0's rollout move by move on a working copy of the board, records the outcome when the rollout ends, reloads the original board for the next head, and, in the all-head schedule, finally reads out a move. Every outcome bit here is produced by actually running the rollout; nothing is supplied from outside. The early-exit schedule (Figure 3) stops at the first outcome 1 and only classifies the position.

35 component evaluations (34 controller ticks and one readout). Colours: reset move terminal test store and reload store and stop readout.

tick 1: reset
tick 2: move, head 0
tick 3: move, head 0
tick 4: move, head 0
tick 5: move, head 0
tick 6: move, head 0
tick 7: move, head 0
tick 8: move, head 0
tick 9: move, head 0
tick 10: move, head 0
tick 11: move, head 0
tick 12: move, head 0
tick 13: move, head 0
tick 14: move, head 0
tick 15: terminal test, head 0
tick 16: store outcome and reload, head 0
tick 17: move, head 1
tick 18: move, head 1
tick 19: move, head 1
tick 20: move, head 1
tick 21: move, head 1
tick 22: move, head 1
tick 23: move, head 1
tick 24: terminal test, head 1
tick 25: store outcome and reload, head 1
tick 26: move, head 2
tick 27: move, head 2
tick 28: move, head 2
tick 29: move, head 2
tick 30: move, head 2
tick 31: move, head 2
tick 32: move, head 2
tick 33: terminal test, head 2
tick 34: store outcome and stop, head 2
readout

35 / 35 Readout: one evaluation of the readout circuit on the original board and the 3 stored outcome bits.

Working board (0, 0, 0)

Original board (read-only input) (3, 4, 6)

head j: 2
parity of moves: 1
rollout finished: 1
running: 0
some outcome 1: 1
stored outcomes: o₀ = 1 o₁ = 1 o₂ = 1

Readout

σ₀ = o₀ = 1; σ₁ = o₁ ⊕ o₀ = 0; σ₂ = o₂ ⊕ o₀ = 0, so σ = 1. The readout tests every heap in parallel and takes the first that decreases:

heap 0: 3 ⊕ 1 = 2 smaller
heap 1: 4 ⊕ 1 = 5 not smaller
heap 2: 6 ⊕ 1 = 7 not smaller

Move: set heap 0 to 2 → (2, 4, 6), nim-sum 0.

Counting the work

Simulated moves M = 13 + 7 + 7 = 27 (3 heads run).
Evaluations M + 2B + 2 = 27 + 6 + 2 = 35: 27 move updates, 3 terminal tests, 3 outcome updates, 1 reset, 1 readout.
Bound on M: BN(2^B − 1) = 63.
Each single evaluation is a shallow circuit: one policy step has Boolean depth ≤ 17 (≤ 36 threshold layers), the readout ≤ 19 (≤ 40), one controller tick ≤ 34 (≤ 70). Those bounds are per evaluation; the number of evaluations grows with the board. That no shallow family computes the complete board-to-move map is a separate statement, conditional on the named classical input that parity is not in AC⁰.

All 34 controller ticks as a table

Tick	Kind	Working board	j	parity	o₀…	What happens
1	reset	(3, 4, 6)	0	0	000	Reset: load the board, select head 0, clear the outcomes.
2	move	(2, 4, 6)	0	1	000	Head 0 moves: heap 0 from 3 to 2 (subtract 1 from the first heap of size at least 1).
3	move	(1, 4, 6)	0	0	000	Head 0 moves: heap 0 from 2 to 1 (subtract 1 from the first heap of size at least 1).
4	move	(0, 4, 6)	0	1	000	Head 0 moves: heap 0 from 1 to 0 (subtract 1 from the first heap of size at least 1).
5	move	(0, 3, 6)	0	0	000	Head 0 moves: heap 1 from 4 to 3 (subtract 1 from the first heap of size at least 1).
6	move	(0, 2, 6)	0	1	000	Head 0 moves: heap 1 from 3 to 2 (subtract 1 from the first heap of size at least 1).
7	move	(0, 1, 6)	0	0	000	Head 0 moves: heap 1 from 2 to 1 (subtract 1 from the first heap of size at least 1).
8	move	(0, 0, 6)	0	1	000	Head 0 moves: heap 1 from 1 to 0 (subtract 1 from the first heap of size at least 1).
9	move	(0, 0, 5)	0	0	000	Head 0 moves: heap 2 from 6 to 5 (subtract 1 from the first heap of size at least 1).
10	move	(0, 0, 4)	0	1	000	Head 0 moves: heap 2 from 5 to 4 (subtract 1 from the first heap of size at least 1).
11	move	(0, 0, 3)	0	0	000	Head 0 moves: heap 2 from 4 to 3 (subtract 1 from the first heap of size at least 1).
12	move	(0, 0, 2)	0	1	000	Head 0 moves: heap 2 from 3 to 2 (subtract 1 from the first heap of size at least 1).
13	move	(0, 0, 1)	0	0	000	Head 0 moves: heap 2 from 2 to 1 (subtract 1 from the first heap of size at least 1).
14	move	(0, 0, 0)	0	1	000	Head 0 moves: heap 2 from 1 to 0 (subtract 1 from the first heap of size at least 1).
15	terminal test	(0, 0, 0)	0	1	000	Head 0: no legal move, so the rollout has ended after an odd number of moves; the outcome bit is 1.
16	store outcome and reload	(3, 4, 6)	1	0	100	Store outcome o0 = 1, reload the original board and select head 1.
17	move	(1, 4, 6)	1	1	100	Head 1 moves: heap 0 from 3 to 1 (subtract 2 from the first heap of size at least 2).
18	move	(1, 2, 6)	1	0	100	Head 1 moves: heap 1 from 4 to 2 (subtract 2 from the first heap of size at least 2).
19	move	(1, 0, 6)	1	1	100	Head 1 moves: heap 1 from 2 to 0 (subtract 2 from the first heap of size at least 2).
20	move	(1, 0, 4)	1	0	100	Head 1 moves: heap 2 from 6 to 4 (subtract 2 from the first heap of size at least 2).
21	move	(1, 0, 2)	1	1	100	Head 1 moves: heap 2 from 4 to 2 (subtract 2 from the first heap of size at least 2).
22	move	(1, 0, 0)	1	0	100	Head 1 moves: heap 2 from 2 to 0 (subtract 2 from the first heap of size at least 2).
23	move	(0, 0, 0)	1	1	100	Head 1 moves: heap 0 from 1 to 0 (no heap has 2 or more: subtract 1 from the first nonzero heap).
24	terminal test	(0, 0, 0)	1	1	100	Head 1: no legal move, so the rollout has ended after an odd number of moves; the outcome bit is 1.
25	store outcome and reload	(3, 4, 6)	2	0	110	Store outcome o1 = 1, reload the original board and select head 2.
26	move	(3, 0, 6)	2	1	110	Head 2 moves: heap 1 from 4 to 0 (subtract 4 from the first heap of size at least 4).
27	move	(3, 0, 2)	2	0	110	Head 2 moves: heap 2 from 6 to 2 (subtract 4 from the first heap of size at least 4).
28	move	(2, 0, 2)	2	1	110	Head 2 moves: heap 0 from 3 to 2 (no heap has 4 or more: subtract 1 from the first nonzero heap).
29	move	(1, 0, 2)	2	0	110	Head 2 moves: heap 0 from 2 to 1 (no heap has 4 or more: subtract 1 from the first nonzero heap).
30	move	(0, 0, 2)	2	1	110	Head 2 moves: heap 0 from 1 to 0 (no heap has 4 or more: subtract 1 from the first nonzero heap).
31	move	(0, 0, 1)	2	0	110	Head 2 moves: heap 2 from 2 to 1 (no heap has 4 or more: subtract 1 from the first nonzero heap).
32	move	(0, 0, 0)	2	1	110	Head 2 moves: heap 2 from 1 to 0 (no heap has 4 or more: subtract 1 from the first nonzero heap).
33	terminal test	(0, 0, 0)	2	1	110	Head 2: no legal move, so the rollout has ended after an odd number of moves; the outcome bit is 1.
34	store outcome and stop	(0, 0, 0)	2	1	111	Store outcome o2 = 1 and stop (last head).

How this relates to the Lean proof. Each tick is one step of Shootout.ostep, with the policy step SelectCircuit.policyIdx inside the rollout registers RolloutExec.rsStep. Rollout.run_parity identifies the outcome bits with $\sigma_0$ and $\sigma_j\oplus\sigma_0$ , and Shootout.ah_counts proves that the all-head schedule takes $M+2B+1$ controller ticks, the reset included; with the single readout this gives $M+2B+2$ evaluations. The browser re-implements these steps; the agreement is checked against Lean's own evaluation of them.

What this does not show. Simulated moves and circuit evaluations are different counts: the $M$ moves are part of the $M+2B+2$ evaluations. The depth bounds (17 per policy step, 19 for the readout, 34 per controller tick) apply to one evaluation each. The complete board-to-move computation repeats them a number of times that grows with the board. That no shallow family computes the complete map is a separate statement (Proposition 5.14 and the text after it), conditional on the named classical input that parity is not in $\mathrm{AC}^0$ .

Depicted in Lean: SelectCircuit.policyIdx, RolloutExec.rsStep, Shootout.ostep, Shootout.initOS, Shootout.query_step, Rollout.run_parity, Game.recoverBit, Game.reconstruct_eq, Shootout.ahMove_eq, Shootout.ah_counts, Shootout.ahL_counts, Shootout.ee_spec, Shootout.ee_counts. Explains the paper’s Figure 3.

Computed in your browser by a short re-implementation of the definitions above (tools/visuals/nimvis-core.js). It is not itself checked by Lean. At build time it agreed with Lean's own evaluation of those definitions on all 313 reference cases.

3 How this is formalised

An interpretive remark. The checked counterparts are Proposition 5.9 (rollouts reveal all bits) and Section 5.6, paragraph 1 (conditional on the classical parity bound, the complete multi-head decision map is not an AC⁰ family).

Coverage record
Paper anchor	`par-depth-amplification-p1` (website anchor; the manuscript has no label here)
Displayed as	Section 5.4, “Depth amplification”
Claim	Iterating an AC⁰ policy for L game steps gives a depth-Θ(L) computation
Coverage category	Informal interpretation
Statement source	paper_jmlr.tex lines 727–729; SHA-256 of the normalised block source `fd2ef06aa48f3554…`
Depends on	Proposition 5.9, Section 5.6, paragraph 1
Explanations	`explain/c-depth-amplification`, `formal/c-depth-amplification`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

No Lean statement corresponds to this claim. This is interpretation or motivation, not a formal mathematical claim.

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

Section 5.4, “Depth amplification”Iterating an AC0 policy for L game steps gives a depth-Θ(L) computation