Explain verified algorithms with shared visuals and static PDF dossiers

[xtraid]

Pipeline illustrations need to explain how algorithmic decisions follow from recorded evidence, and remain readable in a printed report. This change makes MRV selection, propagation, DFS, conflict and rollback visible through the existing renderer, and adds a static PDF report for captured v2 runs.

• Expand the shared visual assets for native traces, Yang–Zhang routing, six optimized mechanisms, Boolean/Wang encoding order, checker receipts and verified witness presentations. Deterministic HiDPI figures, captions, alt text and reduced-motion fallbacks share the existing validated artifact/replay/compositor chain.
• Add the separate v2 formatter/template and opt-in --pdf, using the captured facts and static assets. Ordinary v2 capture needs no LaTeX. PDF formatting performs no solve, oracle invocation, replay or semantic reconstruction; UNSAT sections mark witness content not applicable and make no certificate claim. The isolated compiler is shared with v1.
• Regenerate the canonical Pages assets and refine component copy and the worked example. The README becomes an entry point for status and quickstart, routing the long explanation to Pages and preserving existing Pages routes.

Core behavior, ABI, independent oracles, versioned schemas and dependency locks remain unchanged. V1 keeps its formatter/template and compatible cases; the frozen v1 TeX, PDF and complete output tree are byte-identical.

Local validation for the frozen branch passed:

• 17 C binaries, 199 Python tests including all 33 v1/v2 dossier tests, and 324 renderer tests.
• Strict GCC/Clang, sanitizer, analyzer, complete Memcheck, Cachegrind, 2,000 parser fuzz runs, informational coverage and v1/v2 smoke. Sanitizer and fuzz passed outside the ptrace sandbox with leak detection retained.
• Pages checks cover 40 routes; the accepted Jekyll build covers 40 pages, 799 internal references and 48 browser cases, with build-input identity verified through the final changes.
• All 23 SAT and 26 search-UNSAT PDF pages were reviewed. Fresh smoke preserved 162 narrative images and 43 page rasters exactly; all six timing/environment pages were rechecked.

No Critical or Important review finding remains. Four non-blocking limitations are recorded in the freeze checklist, §13: overlap in redundant MRV legend lines, narrower raster coverage of candidate colors/counts, crowded redundant-signal labels in search-UNSAT figures, and slight readable caller owns label overhang.