Section 7.3, “Setup”FSM experiment setup: N=20, k=4, balanced test set of 2000 positions

Empirical result Supported by saved experimental runs, not by a proof.

1 Paper text

Setup. We consider NIM with $N=20$ heaps and bit-width $k=4$ (so $B=k=4$ heads), matching the encoding of Section 7.1.1. We evaluate on a balanced test set of 2000 positions with $50\%$ $P$ -positions ( $\sigma=0$ ) and $50\%$ $N$ -positions ( $\sigma\neq 0$ ).

Generated from paper_jmlr.tex, lines 1145–1147.

2 Explain this

The second experiment tests the single-frame rollout bypass with learned approximations of the structured policies, controlled by the shootout automaton. Setting: $N=20$ heaps, $k=4$ bits, so $B=4$ heads; a balanced test set of 2,000 positions, half with $\sigma=0$ and half with $\sigma\ne0$ . The trained floating-point networks are not claimed to satisfy the formal gate restrictions.

3 How this is formalised

How this is covered. Empirical setup from the saved notebook; not formalised.

Coverage record
Paper anchor	`par-setup-p1` (website anchor; the manuscript has no label here)
Displayed as	Section 7.3, “Setup”
Claim	FSM experiment setup: N=20, k=4, balanced test set of 2000 positions
Coverage category	Empirical result
Statement source	paper_jmlr.tex lines 1145–1147; SHA-256 of the normalised block source `2a05cec9d17cbecb…`
Explanations	`explain/c-fsm-setup`, `formal/c-fsm-setup`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

No Lean statement corresponds to this claim. This is an empirical statement about saved experimental runs. Lean proofs do not certify training runs, curves or checkpoints.

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