Section 7.3, paragraph 2Per-head accuracy compares channel bits with the exact teacher; the FSM uses the OR of queried outcomes

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

1 Paper text

The per-head accuracy metric is whether the model’s rollout outcome matches the teacher’s rollout outcome—the correct channel bit—not whether it matches the $P/N$ label directly. Each exact teacher head computes a specified linear functional ( $r_0=\sigma_0$ ; $r_j=\sigma_j\oplus\sigma_0$ for $j\ge1$ ). The learned heads can make channel errors. The FSM uses an OR of the queried outcomes for $P/N$ classification, which is a different task from reconstructing every nim-sum bit.

Generated from paper_jmlr.tex, lines 1164–1165.

2 Explain this

Two different things are measured. Per-head accuracy asks whether the learned head's rollout outcome equals the exact teacher's outcome (the correct channel bit). The controller's classification uses the OR of the queried outcomes. A head can be wrong on a channel without changing the final OR decision.

3 How this is formalised

How this is covered. Empirical definitions. The exact teacher heads' channel values are the checked identities of Proposition 5.9; the OR rule is Section 5.4, “Finite-state shootout controller (FSM over policy heads)”.

Coverage record
Paper anchor	`par-rollout-evaluation-p2` (website anchor; the manuscript has no label here)
Displayed as	Section 7.3, paragraph 2
Claim	Per-head accuracy compares channel bits with the exact teacher; the FSM uses the OR of queried outcomes
Coverage category	Empirical result
Statement source	paper_jmlr.tex lines 1164–1165; SHA-256 of the normalised block source `c3bf990959c12836…`
Depends on	Proposition 5.9, Section 5.4, “Finite-state shootout controller (FSM over policy heads)”
Explanations	`explain/c-fsm-metric`, `formal/c-fsm-metric`
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).