Section 8.1, paragraph 1The experiments' networks differ from the theorem's gates; finite results do not settle asymptotic ones
Informal interpretation Motivation, interpretation or scope; not a formal claim.
1 Paper text
The simulation theorem concerns Boolean literal-threshold gates with nonnegative weights and bounded thresholds, including their permitted compositions. The experiments use floating-point signed linear layers and ReLU as well as LayerNorm and a Log-Softmax loss. Their difference from the theorem therefore extends beyond normalisation layers. A failure at one finite board size does not establish an asymptotic representational impossibility; success on a finite dataset does not establish strong mastery. The controlled comparison supports a narrower empirical conclusion: the reported transition representation is much easier to learn under this supervised protocol.
Generated from paper_jmlr.tex, lines 1225–1228.
2 Explain this
The theorem's gates (nonnegative weights on Boolean literals, bounded thresholds) and the experiments' networks (floating-point signed linear layers, ReLU, LayerNorm, Log-Softmax loss) differ in more than normalisation. Two consequences: a failure at one finite board size does not prove an asymptotic impossibility, and success on a finite dataset does not prove strong mastery. What the experiment supports is narrower: under this supervised protocol, the transition representation is much easier to learn.
3 How this is formalised
A scope statement relating Theorem 2.4 to the empirical records; nothing further is formalised.
| Paper anchor | sec:idealisation-p1 (website anchor; the manuscript has no label here) |
|---|---|
| Displayed as | Section 8.1, paragraph 1 |
| Claim | The experiments' networks differ from the theorem's gates; finite results do not settle asymptotic ones |
| Coverage category | Informal interpretation |
| Statement source | paper_jmlr.tex lines 1225–1228; SHA-256 of the normalised block source d46857718fdf6b1d… |
| Explanations | explain/c-idealisation, formal/c-idealisation |
| 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).