docs: qualify proof and execution guarantees

[oxura]

Closes #1317.

Scope

Qualify the law guarantee at its first README appearance: --verdict checks translated terms with the proven kernel, while the source checker and translation are unproved. Execution can differ from proved results on a backend with documented limits.

• Link the README limitations, existing WONTFIX and the paper's actual proof-scope paragraph.
• Give the guide introduction the same qualification, linking directly to the paper's mechanization section on PDF page 8; remove the contradictory later bug-free-code guarantee too.
• Give the existing introductory film two paced scope slides next to its first proof claim. Replace its unconditional all-bugs/no-mistakes claims with declared-law wording.
• Regenerate both media/intro.mp4 and media/intro.gif with the existing native-canvas capture command, so the shipped film is not stale.

No checker, translator, kernel or backend semantics change. Detailed limitation lists stay in WONTFIX and the paper.

Verification

• Real cached Lean kernel: the issue's exact NaN round-trip law prints ALL PROOFS CHECK under --verdict.
• Actual source interpreter and native binary print 2139095041; emitted JavaScript prints 2143289344. The documented backend decision is unchanged.
• Actual Chromium preview: both scope slides are readable at their computed 9.7s and 8.7s beats; no recorded browser errors.
• Complete native-canvas movie capture: 15,600 frames; decoded the new scope slides from the generated MP4 and visually inspected the actual movie frame.
• MP4: H.264, 1920×1080, 60fps, 260s. Generated GIF: 640×360, 259.97s.
• bun gates/repo.ts: PASS 50 / 50, including the unchanged 8,000-token guide cap.

No timing assertion or wording-only permanent test is added. The unavailable mini-cluster gates were not run.

[Lorenzobattistela]

Thanks @oxura. We're closing this one. The README, the guides and the intro film are written by hand and are part of how we present Bend, so we don't take outside rewrites of them, and we're keeping the pitch as it is. Inside Bend's semantics the laws do hold. The real gaps #1317 points at are the backends and the translation into the kernel, and those belong in the Limitations list next to the ones already there. #1423 tracks that and #1424 adds the two lines.

[oxura]

Understood, thanks for clarifying the boundary. I won’t reopen this PR or submit further outside rewrites of the README, guides or intro film. I’ll keep the distinction between source semantics, backend limits and translation into the kernel in mind, and leave the Limitations update to #1423/#1424.