Section 7.3, paragraph 5Average 2.87 shootouts because positions with σ₀=1 stop at head 0; scope of the result

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

1 Paper text

Early stopping. The average number of shootouts is 2.87 rather than the worst-case 4, because any N-position with $\sigma_0 = 1$ is caught at head 0 (one rollout); only those with $\sigma_0 = 0$ require further heads. Scope. We report the saved seed-7 configuration above. Perfect classification on this finite test set does not establish all-position correctness, robustness across seeds, or successful self-play discovery. We make no broader sweep claim without corresponding run records.

Generated from paper_jmlr.tex, lines 1192–1195.

2 Explain this

The controller used 2.87 rollouts on average instead of the worst case 4, because every $N$ -position with $\sigma_0=1$ is detected by head 0 after one rollout; only positions with $\sigma_0=0$ need further heads (and $P$ -positions always need all four). The result is for the saved seed-7 configuration and does not establish correctness on all positions, robustness across seeds, or self-play discovery.

3 How this is formalised

How this is covered. The 2.87 average is empirical. That the depicted controller stops after one query when head 0 reports 1, and uses at most $B$ queries, is checked (Figure 3).

Coverage record
Paper anchor	`par-results-p5` (website anchor; the manuscript has no label here)
Displayed as	Section 7.3, paragraph 5
Claim	Average 2.87 shootouts because positions with σ₀=1 stop at head 0; scope of the result
Coverage category	Empirical result
Statement source	paper_jmlr.tex lines 1192–1195; SHA-256 of the normalised block source `2f5c7c88e0e81519…`
Explanations	`explain/c-early-stopping`, `formal/c-early-stopping`
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).