This guide explains the revised manuscript and retains its inherited verification boundaries. There are two censuses, with different statements as their subjects:
| Inherited contract | Complete | Partial | Unchecked |
|---|---|---|---|
| Revised 49 internal claims | 49 | 0 | 0 |
| Original wording of those claims | 41 | 7 | 1 |
The eight inherited amendments
| Claim | Scope that the revised statement makes explicit |
|---|---|
| 6.12 | Each irreducible component is contained in full support; the original containment was reversed. |
| 9.4 | Hausdorff coefficient topology and continuity for the compared representations. |
| 9.5 | The realized locus consists of points satisfying those topology and continuity hypotheses. |
| 9.6 | The surviving cohomological degree belongs to the declared classicality range; comparison inputs are explicit. |
| 10.5 | Complete separated coefficients, finite continuous admissible classes, integrality, and actual quotient equations in every admissible frame. |
| 12.2 | Continuous characteristic-zero pointwise comparison under the stated realization input. |
| 12.4 | Applicability of realization at the selected derived eigensystem, with the comparison inputs exposed. |
| 12.6 | A compatible Hecke point \(y\circ f=x\), actual ordinary or derived carriers, and both existing families for the same automorphic object. |
In the inherited record, original 6.12 is unchecked; original 10.5 and the other six amended claims are partial. Revised completeness does not certify the stronger original wording. Claims 3.1 and 3.3 required no additional amendment in the v0.17 completion record.
Final editorial clarifications
The final companions expose finite \(S\), a coherent Frobenius normalization, the local coefficient-test category in 3.3, the \(r>n\) Fitting boundary, and both compared Frobenius polynomial identities in ordinary completion. These clarifications are distinct from the eight inherited amendments; no new Lean replay certifies them.