Section 7.3, paragraph 2Multi-head FSM classifies all 2,000 test positions correctly, with imperfect per-head channel accuracy

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

1 Paper text

Multi-head FSM achieves perfect classification. The saved output reports correct $P/N$ classification on all 2,000 test positions, matching the teacher’s final decisions. However, the saved per-head channel accuracies are $2000/2000$ , $2000/2000$ , $1469/2000$ and $1480/2000$ , respectively: $1.0000$ , $1.0000$ , $0.7345$ and $0.7400$ . Consequently, this result does not establish exact channel recovery or recovery of the full invariant by the learned model. Early stopping leaves some channels unqueried, and even queried channel errors need not change the final OR decision. These are transcribed saved outputs, not a fresh checkpoint evaluation; reached-head error counts and a reproducible end-to-end rerun are needed for a stronger claim.

Generated from paper_jmlr.tex, lines 1177–1179.

2 Explain this

Result. The learned multi-head controller classifies all 2,000 test positions correctly, matching the teacher's decisions.

But. The saved per-head channel accuracies are 1.0000, 1.0000, 0.7345 and 0.7400. So the learned model does not recover every channel bit exactly. Early stopping leaves some channels unqueried, and queried errors need not change the OR. These are transcribed saved outputs; a fresh end-to-end rerun and reached-head error counts would be needed for a stronger claim.

3 How this is formalised

How this is covered. Empirical, transcribed from the saved notebook output. The audit's correspondence row for this section records it as empirical with partly checked arithmetic.

Coverage record
Paper anchor	`par-results-p2` (website anchor; the manuscript has no label here)
Displayed as	Section 7.3, paragraph 2
Claim	Multi-head FSM classifies all 2,000 test positions correctly, with imperfect per-head channel accuracy
Coverage category	Empirical result
Statement source	paper_jmlr.tex lines 1177–1179; SHA-256 of the normalised block source `157360d919881b5c…`
Audited correspondence rows	`sec:exp-fsm-shootout`
Explanations	`explain/c-fsm-results`, `formal/c-fsm-results`
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).