The first 28 pages retain the worked mathematical atlas from the September release. Traditional Part I carries the corresponding core manuscript, including its figures and formal-status appendix; its theorem numbers are the references beneath these titles. The standalone guide uses internal visual-page links. The added pages beginning at V–29 address the strengthened branch in Traditional Part II.
The chosen release records all 33 scoped results complete, with 341 supporting theorem declarations in 47 proof modules and a saved audit of 782 namespace declarations. Those are inherited verification records, not a new Lean run and not counts of historically novel results. The three original conjectures retain their stated status.
Read each kind of evidence at its actual strength
| Evidence | What is checked here | What it does not establish |
|---|---|---|
| Exact matrices | Stochasticity, intertwining, projector identities, inverse formulas, and specific defects. | The same properties for arbitrary partitions or unbounded operators. |
| Rational algebra | Posterior/evidence identities, polynomial integrals, nodal errors, and complete finite path sums. | An unstated observation model or a continuum convergence theorem. |
| Symbolic formulas | The displayed exponentials, Laplace transforms, derivatives, and finite spectral powers under stated conditions. | A general-purpose formal proof of every analytic identity. |
| Vector drawings | Reproducible geometry and sampled curves from the explicit models. | Numerical quadrature certificates or an exhaustive infinite-time experiment. |
| Saved Lean records | The original contract, source files, dependency pins, and earlier verification logs. | Fresh kernel verification of this editorial addition. |
Reproduce a calculation before adapting it
The visual-appendix tree contains the mathematical models, drawing generator, and exact-example verifier. Its README records their paths and execution commands. The inherited September verifier records 204 exact or symbolic assertions and 11 deliberately false controls rejected. The monograph reproduces that symbolic suite with the available SymPy and mpmath environment. Its current execution record is identified on V–42. Its JSON record names every check and its finite scope.
The finite families are explicit: three-step Feynman–Kac paths are fully enumerated, selected rational priors are checked exhaustively within their stated denominator bound, and Green inverses are checked on four named grids. No finite count is used as a substitute for a general theorem.
To change a model, specify the state convention, partition, likelihood meaning, topology, and domain first. Then rerun the calculations and inspect the regenerated drawings. A preserved formula with changed assumptions is not automatically a preserved result.
Read this as
Use the guide to see why a hypothesis matters and to compute a small case. Use the manuscript and its formal map for the scope of the general claim.