Lean verification and scope

Fifth checked block, 6 September 2026. The release contains 341 explicit Lean theorem declarations across 47 proof modules, including 31 additional declarations since the fourth checked block. The September 6 release records a successful full build and namespace audit with Lean 4.34.0-rc2 and pinned mathlib. The audit inspects 782 declarations, including definitions and generated auxiliaries; only propext, Classical.choice and Quot.sound are allowed. These are different counting units from the paper's 33 theorem-like results.

The ledger has 33 complete, zero partial, and zero pending results. The last two results, 13.2 and 15.1, are now complete. The three separately stated conjectures remain open and are excluded from this count.

“Complete” means the stated scope follows from the named checked targets and the ordinary specializations recorded in the ledger. Prose-to-Lean correspondence is manually reviewed. The fractional targets use complex Hilbert spaces; complexification for real operators is an ordinary mathematical specialization, not a separately checked Lean construction. Completion of the theorem ledger does not certify every prose sentence, numerical figure or open conjecture.

Permalink · Source line 1867

The actual damped exponential is decomposed into finitely many terms of the form \(t^k e^{(\mu-z)t}\). Integrability and convergence to zero follow from \(\operatorname{Re}\mu<\operatorname{Re}z\). The formal proof uses generalized eigenspaces of left multiplication on the matrix algebra, so nilpotent Jordan parts are included. Both inverse identities follow by integrating the two exponential derivative formulas. A continuous linear sandwich map gives the literal rectangular matrix memory integral and the actual inverse. No normality or externally supplied growth bound is required.

Permalink · Source line 1929

The standard finite Taylor-jet calculus defined before the theorem is constructed using the direct sum of generalized eigenspaces. Uniqueness, cutoff stability, and exact rectangular naturality are proved. Cauchy's formula identifies the local coefficients with actual circle integrals; admissible radii exist in every stated open holomorphic neighborhood, and changing them leaves the canonical operator unchanged. The argument permits disconnected neighborhoods and different matrix dimensions. It makes no assertion about general Banach-algebra contour deformation.

Permalink · Source line 1939

The inherited fourth block proves the scalar beta normalization, the Lebesgue integral representation of actual positive fractional powers, the literal resolvent-defect formula, both printed norm constants, and exact intertwining. The rectangular complex-Hilbert-space semigroup proof substitutes those constants into Duhamel's identity. The varying-space tower proof gives summability of fractional-defect norms and uniform convergence of time-defect norm series on bounded time intervals. Here “summable” means summable in norm. Operators with unrelated codomains are not added together; a separate fixed-space theorem proves operator-series convergence when such a sum is defined.

Permalink · Source line 1948

The September 6 release records that the full pinned build, project-wide axiom audit, all 54 companion tests and six verifier controls passed. No fresh Lean build is asserted for this October edition. The 54 tests comprise the original 37 and 17 added boundary and validation cases. The 19 numerical figure pairs are unchanged. The earlier 79-field numerical comparison remains historical evidence, not a rerun in that September 6 block. The September 12 visual release subsequently records a numerical replay; current October checks are reported separately in the final package. Machine-readable source contracts, exact theorem targets, full logs and previous checked ledgers accompany the source archive. Numerical tests are finite regressions and are not substitutes for the Lean proofs.

Permalink · Source line 1959