Section 6.5, paragraph 1Global invariant hard from one frame; transition quantity local from two frames
Informal interpretation Motivation, interpretation or scope; not a formal claim.
1 Paper text
The core representational point is that the global invariant is hard to compute from a single frame, whereas the transition quantity is locally computable from two frames (Lemma 5.4). Section 7.2 isolates this effect by training one-frame and two-frame models on the same restoration targets.
Generated from paper_jmlr.tex, lines 987–989.
2 Explain this
The representational point in one sentence: the global invariant is hard to compute from one frame, while the transition quantity is local from two. The supervised experiment isolates exactly this contrast by training one-frame and two-frame models on the same targets.
3 How this is formalised
A summary of Theorem 5.2 (barrier) and Lemma 5.4; the experiment is Section 7.2.5, “One-frame does not learn restoration; two-frame eventually does”.
| Paper anchor | sec-from-global-invariants-to-local-checks-p1 (website anchor; the manuscript has no label here) |
|---|---|
| Displayed as | Section 6.5, paragraph 1 |
| Claim | Global invariant hard from one frame; transition quantity local from two frames |
| Coverage category | Informal interpretation |
| Statement source | paper_jmlr.tex lines 987–989; SHA-256 of the normalised block source 73cb6f5d6a547c77… |
| Depends on | Theorem 5.2 (barrier), Lemma 5.4 |
| Explanations | explain/c-local-checks, formal/c-local-checks |
| 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).