Lean verification and revision scope

The preserved Lean release 0.17.0, reverified in evidence release 0.17.1, reports 748 named theorem declarations written for Paper XII, including supporting lemmas and interface results. A further 81 theorem declarations are reused unchanged from Paper X and counted separately. The cumulative verification rebuilds all 96 registered project modules with Lean 4.34.0-rc2 and warnings treated as errors. The transitive axiom audit covers 1,229 named declarations and permits only propext, Classical.choice, and Quot.sound. Three deliberately invalid controls test rejection of a false proof, a placeholder, and an incorrect empty family normalization. The pinned Mathlib dependency cache is not itself rebuilt. Exact compiler results, source hashes, and the verification scope are recorded with the archive.

The preserved release records complete mapped Lean statements for all 49 internal numbered claims of its revised manuscript. The present traditional edition retains those proof bodies, exposes the local-map and coefficient-target hypotheses in Proposition 3.3, makes the \(r>n\) convention explicit in the proof of Theorem 6.4, states all the pointwise comparison inputs in Definition 12.1, and declares a finite ramification set and coherent geometric Frobenius normalization. These editorial clarifications are recorded separately from the inherited eight amendments; they are not counted as newly compiled Lean certificates. No new statement amendment was needed for the completion and tensor results. The eight inherited amendments remain explicitly separate from the original wording, and the cited arithmetic inputs remain outside the internal claim census. Formal proof coverage is recorded claim by claim in the roadmap. These checks certify the formal statements under their explicit hypotheses, not every prose claim, novelty assertion, or external arithmetic result.

The completion block proves Theorem 3.1 and Proposition 3.3 using actual algebraic tensor products, actual Hausdorff completions, and the actual closed generated ideals. Both inverse laws, continuity in both directions, and the canonical factor maps are checked. An independent comparison with the algebraic inverse limit completion identifies the topology and local ring structure. The global theorem retains continuous local algebra points and their naturality, rather than only an unstructured point existence statement. The empty family retains the scalar adic topology. The zero condition and unit ideal boundaries are checked separately.

The preceding Fitting block proves Theorem 6.3, Theorem 6.4, Proposition 6.5, and Theorem 7.1. Its intrinsic Fitting ideals are independent of the chosen finite presentation, including the number of generators and relations. Arbitrary base change, all higher fiber dimension strata, and the complete support and Fitting transport statement are checked. The Noetherian and finite module hypotheses of the manuscript provide the finite presentation needed by the general construction.

The new checks for Proposition 5.1, Theorem 5.4, and Corollary 11.2 include actual group algebra transfer and augmentation. Coinvariant recovery uses the quotient by all balancing relations, with its universal property proved. In the commutative case, this construction is identified with the ordinary tensor product. The augmentation relations generate exactly the augmentation ideal acting on the module. Applying augmentation to the coordinates of a supplied free basis gives a coefficient basis with the same index set. The right module argument applies to arbitrary groups, including nonabelian two groups, and includes rank zero.

The new checks for Theorem 5.2, Corollary 5.3, Corollary 8.4, and Proposition 11.1 construct the full multivariable truncated polynomial algebra isomorphism and identify its augmentation generators. The residual group algebra is local for abelian \(p\) groups in characteristic \(p\). For each supplied Hecke idempotent, the trace is the image dimension cast into the coefficient field; occupancy is equivalent to positive rank and, in characteristic zero, nonzero trace. The dyadic calculation gives the two rational sign projectors, proves that neither lies in the integral group algebra, and identifies the residual algebra with \({\mathbb F}_2[X]/(X^2)\).

Corollary Corollary 5.3 is now checked for every finite \(p\) group, including nonabelian groups, over every field of characteristic \(p\). The proof uses a finite prime field orbit span and a nonzero fixed vector. The original unrestricted statement is restored, and the earlier explicit abelian restriction is no longer needed.

The checks for Proposition 7.3, Theorem 8.2, and Corollary 8.3 now include the actual formal power series quotient and the canonical Hecke packet maps. In the node \(k[[x,y]]/(xy)\), quotienting by \((x)\) gives \(k[[y]]\), with support \(V(x)\); Lean verifies both irreducible components and the exclusion of the generic point \((y)\). The components can still meet, so this is not a claim that their supports are disjoint.

For the Hecke results, the canonical ring decomposition in Standard fact 8.1 remains a declared external input. Its coordinates are the actual localization maps. The module direct sum, the packet identification with the localized module, and the formula \(v\mapsto v/1\) are constructed in Lean. Nilpotence in the selected Artin local factor, together with invertibility of a generator on each other factor, gives a single positive exponent for the simultaneous generalized eigenspace. The result includes the explicit generators \(T_i-\lambda_i\), agrees with the packet used in the trace theorem, and does not assume semisimplicity.

The revised five gate statement in Theorem 12.6 is now checked for both ordinary and derived carriers and for a general support comparison. The comparison is an actual inclusion of subsets of prime spectra, and scalar extension is proved to satisfy it. The coefficient quotient and ordinary or derived control maps yield finite level support; that conclusion is not supplied as a separate patching assumption. The specialized tensor module or derived cohomology supplies an actual nonzero eigenvector. The declared realization theorem is applied to this particular eigensystem, and the resulting representation comparison is an actual invertible linear intertwiner. The system conclusion uses the family attached to the very same automorphic object, with distinguished member identities and a common algebraic polynomial spine.

The original comparison wording did not explicitly supply a compatible Hecke point over the fixed coefficient field. Support preservation alone is insufficient: extension from \(\mathbb Q\) to \(\mathbb Q(i)\) preserves full support, but there is no ring map \(\mathbb Q(i)\to\mathbb Q\) extending the identity. The revision therefore states \(y\circ f=x\) and exposes the arithmetic comparison and existing-family inputs. Residual occupancy, representability and the applicable patching theorem remain supplied arithmetic provenance. The original full statement remains partial. The completed tensor quotients and intrinsic Fitting ideals are now checked as described above, including the full Fitting transport clause.

The derived realization checks cover the revised Theorem 9.6 and Theorem 12.4. They prove vanishing outside the bounds of an actual finite projective model and construct a nonzero cohomology vector inside those bounds. The Hecke action is induced from multiplication on the original cochain model, carried through scalar extension and derived localization, and proved to act by the specialized character on actual cohomology. The conditional arithmetic step gives an actual invertible linear intertwiner from the declared realization input and common Frobenius polynomials.

The original formulation of Theorem 9.6 did not ensure that the surviving degree lies in the classicality range. A complex concentrated in degree one has full support over a field, while a classicality condition restricted to degree zero says nothing about its nonzero fiber. The revision requires the declared range to contain the model interval. The conditional conclusion of Theorem 12.4 retains applicability at the selected eigensystem itself. Both statements now expose the topology, continuity, semisimplification, and common polynomial inputs needed for the representation comparison. Their original unconditional cohomological conclusions are checked, but their original complete statements remain partial. The general support comparison and compatible-point formulation is now checked in the revised Theorem 12.6, as described above.

The derived support checks prove Theorem 6.16, Theorem 6.18, and Corollary 6.19 as originally stated. Perfect complexes are actual derived category objects equipped with bounded finite projective models and derived isomorphisms to those models. Scalar extension is constructed on cochain complexes. Its associativity, preservation of homotopy equivalences, and independence under actual derived isomorphisms are checked. The quotient support formula uses the actual map of spectra and its image \(V(I)\). Every field valued point factors through the residue field at its kernel, and faithful flatness of field extensions preserves and reflects acyclicity. The surviving integer degree is expressed using the actual derived cohomology functor, with a corresponding witness in the specialized cochain model. These proofs do not require the external cohomological support description in Standard fact 6.15. The external classicality theorems remain supplied arithmetic inputs; the conditional derived realization argument is checked as described above.

The adequacy checks prove Theorem 4.2 as originally stated. They construct the faithful standard representation from the actual permutation module, prove irreducibility after extension to the algebraic closure, and split every group element's characteristic polynomial over \({\mathbb F}_7\). The trace zero adjoint is the kernel of matrix trace with its conjugation action, and its sign plus standard decomposition is an actual equivariant linear isomorphism. The averaging proof is connected to Mathlib's actual first group cohomology, while the invariant calculation gives actual degree zero vanishing. Canonical projectors are identified with generalized eigenspace projectors for every positive exponent. Their trace pairings detect every nonzero endomorphism and hence every irreducible adjoint submodule. The two printed constituent witnesses and their traces are checked exactly. The adequacy definition remains a cited convention; no external adequacy theorem is assumed in this finite certificate.

The realization checks cover Theorem 9.4, Corollary 9.5, Theorem 10.7, Theorem 12.2, and Theorem 12.5. Characteristic polynomial coefficients are continuous by the principal minor formula. Equality on the declared Frobenius conjugacy classes therefore extends to the whole Galois group. The finite dimensional algebra input is explicit: a supplied semisimple representative preserves every characteristic polynomial, and a general Brauer Nesbitt theorem identifies semisimple representations with equal polynomials. Lean proves independence of this representative and the irreducible conclusion. Construction of semisimplification, the general Brauer Nesbitt theorem, and arithmetic Chebotarev density remain external inputs.

The ordinary completion argument derives finite generation, full finite level support, and an actual nonzero Hecke tensor fiber from the patched support and control isomorphisms. The declared classicality input then supplies the occurring automorphic object and its attached representation. Both existing compatible systems, with their common polynomial spine, are retained as hypotheses in the propagation results. These results do not construct missing companions or an attached compatible system.

The pointwise realization and ordinary completion statements now explicitly require Hausdorff coefficient topology and continuity of the compared representations, including the universal specialization. The corresponding locus statement is restricted to such points. These three revised claims are counted as complete; their original wording remains partial. This clarification also makes the coefficient topology in Standard fact 9.2 explicit without claiming a new proof of that external arithmetic fact.

The earlier revision made two further substantive corrections. In Corollary 6.12, every irreducible component is contained in the full support. The previous sentence reversed that containment. In Theorem 10.5, the coefficient, continuity, integrality, class finiteness, and quotient condition hypotheses are now explicit. Finite forests by themselves establish branches, not all arithmetic effectivity assertions. Corollary Corollary 3.2 now gives the closed kernel argument and the continuity and uniqueness of its factors.

The original manuscript and its literal claim records are preserved with the release. In that original census, 41 claims are fully checked, seven are partial, and one is not checked as written. The corrected Corollary 6.12 and restricted Theorem 10.5 are counted as proved only for their revised statements. The original unrestricted completion wording is not retrospectively marked proved. Source hashes, the exact amendments, compiler logs, and a mathematical self-review accompany the code.

Compiler and axiom checks are distinguished from semantic proof review and external arithmetic results.

Permalink · Source line 1804