The appendix uses small objects to make the paper's constructions inspectable. Every matrix and finite example is supplied in editable source, with a separate check record. The plates make those calculations visible. Their appearance helps explain the result, while the equations and check records supply its evidence.
| Evidence | What it supports | What it does not supply |
|---|---|---|
| Exact matrices | The displayed finite identities, witnesses, and counterexamples. | A classification of arbitrary systems. |
| Symbolic derivatives | The explicit rotating and Bloch examples. | A proof inferred from numerical differentiation. |
| Rational enclosures | The three displayed dispersion intervals and ratio inequalities. | A continuum theorem from three sample points. |
| Saved Lean release | Its 19 registered finite items under their recorded hypotheses. | A fresh kernel run for this appendix. |
| Numerical record | The original finite software examples in the tested environment. | Physical experiments or unrestricted convergence. |
Which source is authoritative?
The saved formal checkpoint is v0.6.0: 323 recorded theorem declarations in 25 current modules, including supporting lemmas. These counts describe the inherited checkpoint. This prose revision includes no new Lean kernel execution. The final traditional edition supplies the current reading references. The original proof sources and the separate v0.5.1 editorial sibling retain their own identities.
The five research boundaries remain separate: an anomaly-free coherent refinement, uniform control of effective operators, Lorentzian reconstruction, an Einstein infrared limit, and a positive physical massless spin-two sector. A finite projector bundle, positive transfer matrix, or spectral diagnostic does not settle them.
A practical way to use the appendix
Choose one page, reproduce its matrix calculation, and then read the cited theorem with its hypotheses. The retained execution records give the exact assertions, tested ranges, and rejected controls for the finite and symbolic suites. The additional examples and their recorded bounds are described on Visual 40. In particular, retain the two resolvent assumptions on Visual 21, the distinction between a known error and an error family on Visual 20, and the limitation of testing only the common kernel on Visual 26.
Read this as
Exact finite structure is valuable because its boundary is explicit. The appendix adds understanding and reproducibility, not unproved continuum claims or a new theorem count.