This guide preserves the 24 worked pages and 22 exact figures from the finite visual appendix. It updates their references to the final traditional paper and explains the relation to that paper's broader nonlinear and analytic material.
Read each evidence record in its scope
| Evidence | What it supports |
|---|---|
| Finite Lean release | The finite declarations and the released Section 16 and 17 additions were compiled in the pinned environment. The Lean guide records the current source scope, axiom audit, and kernel replay. |
| Ordinary mathematics | The traditional paper's expanded proofs, including nonlinear, obstruction, lifting, and smooth transport results. Inclusion in that paper does not add these results to the finite Lean contract. |
| Exact model checks | Replay on 20 October 2026 passed all 124 exact checks and rejected all four deliberately false controls. The scope is the displayed finite matrices, paths, polynomials, candidate tables, and trees. |
| Figure regeneration | All 22 editable TikZ figures are supplied with their exact model data and generators. The original figure sources and their earlier regeneration record remain preserved. |
The release also records 18,630 exact assertions for the Section 16 and 17 examples. These finite calculations support the displayed mechanisms. General claims rest on their mathematical proofs and, where mapped, their Lean declarations.
Boundaries that remain in force
The formal edge system uses a single scalar coefficient semiring. The heterogeneous path theorem for arbitrary lengths uses a common packet index, with forms allowing changing types for two and three factors. General dependent tree expansion and analytic convergence lie outside this finite formal contract. The traditional paper states and proves its broader results with their own hypotheses.
The generic obstruction theorem rejects its named candidate. A nonzero holonomy block rejects flatness for its named loop data. Neither conclusion supplies a universal classification, a new arithmetic realization, or an algorithmic search guarantee.
Replay the worked layer
From the editable visual guide directory, compile the PDF with python build.py. Check the exact examples with python checks/verify_examples.py. Regenerate the figures with python source/generate_graphics.py. Use a temporary copy to retain the delivered evidence unchanged. The full package preserves the finite release and its original formal sources separately.
Read this as
Use the figures to understand the mechanisms, the traditional paper to read the mathematical proofs, and the Lean guide to identify the exact formal contract. These are related records with distinct scopes.