Historical checkpoint scope
Block 27 formal-verification status. Seventeen source proof claims are checked at their declared conditional scope and three remain partial. Block 27 proves actual prime and Frobenius restriction to arbitrary finite normal number fields, derives unramifiedness outside the discriminant, and proves independence from Frobenius choices. Its general arithmetic coverage equivalence retains the prime-existence assertion as a premise. Block 25 proves the system-to-member isomorphism bridge under the required overlap density and proves actual arithmetic Frobenius separation for representations of a fixed cyclotomic Galois group over \({\mathbf Q}\). General arithmetic Frobenius coverage remains unproved here, so Claim 9.1 remains partial. Claim 11.2 is checked as the full-spine existence boundary with a nonzero joint eigenvector in every supplied required packet. The residual, higher-depth, and positive-trace requirements are retained; universal arithmetic occupancy is not proved. Claim 8.2 is checked as a universally quantified conditional completion theorem, retaining its explicit local-closure and finite-level-existence hypotheses. Earlier accounting included verification of particular arithmetic application premises in this claim; those applications remain separate and unfinished. For the fixed quadratic packet of actual \(G_{{\mathbf Q}}\) characters, local triviality after the field-induced map from \(G_{{\mathbf Q}_p}\) is proved equivalent to \(p\equiv1\pmod4\) or global triviality. Its preservation under coefficient completion and simultaneous finite-level existence criterion are proved. The packet characters are trivial on actual valuation inertia at every odd prime, with a locally dominating valuation constructed. The equality of the valuation decomposition group with the entire local Galois group is not established, and ramification at two is not claimed. The full packet identifications, Galois-to-Weil–Deligne attachment, and coefficient and Hodge–Tate/period comparisons remain unfinished.
Cumulative formalization status after Block 27.
On this page · Permalink · Source line 9
The cumulative formal ledger records 17 source proof claims checked at their stated conditional scope, 3 partially formalized, and no untouched proof claims. Claims 8.2 and 11.2 are checked with their stated hypotheses retained. Claims 9.1, 9.2, and 11.1 remain partial. The finite cyclotomic case of Claim 9.1 is now checked with arithmetic coverage proved. Arithmetic applications of the conditional completion and occupancy criterion still require verification of their premises. This status does not prove any universal existence conjecture. No PDF has been typeset or visually certified for this code-focused checkpoint.