Section 8.4, paragraph 1Theorem 5.12(i) bounds one restricted interface, not general single-policy search
Informal interpretation Motivation, interpretation or scope; not a formal claim.
1 Paper text
Theorem 5.12(i) bounds winning-move selection for fixed bit-width, a specified family of root/one-heap measurements and a polynomial-size, constant-depth readout. It does not bound general single-policy search. Within that interface, the structured channels reconstruct the invariant and permit direct move selection. The extra computational resource is the sequential rollout, not the number of neural output coordinates alone. Repeated deterministic measurements of the same affine channel cannot create additional channel bits, but changing the permitted query transformations or controller computation changes the model and can remove that restriction.
Generated from paper_jmlr.tex, lines 1249–1252.
2 Explain this
Theorem 5.12(i) is narrow on purpose: fixed bit-width, a specified family of root and one-heap measurements, and a polynomial-size, constant-depth readout. It does not bound general single-policy search. Within that interface, channels reconstruct the invariant. The extra resource is the sequential rollout, not the number of output neurons. Changing the allowed queries or controller computation changes the model and can remove the restriction.
3 How this is formalised
An interpretation of Theorem 5.12 (i) and Section 5.4, paragraph 3 (which shows how arbitrary queries would remove the restriction).
| Paper anchor | sec:multipolicy-discussion-p1 (website anchor; the manuscript has no label here) |
|---|---|
| Displayed as | Section 8.4, paragraph 1 |
| Claim | Theorem 5.12(i) bounds one restricted interface, not general single-policy search |
| Coverage category | Informal interpretation |
| Statement source | paper_jmlr.tex lines 1249–1252; SHA-256 of the normalised block source 1d5275c69af4bff5… |
| Depends on | Theorem 5.12 (i) |
| Explanations | explain/c-rollout-separation, formal/c-rollout-separation |
| 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).