CayleySpec + L-Function Zeros: Complete Formal and Empirical Analysis

This repository contains the complete source code, datasets, and papers for two complementary research projects: CayleySpec (formal verification of Cayley-Hecke dictionary in Lean 4) and L-Function Zero Statistics (empirical analysis of 63,844 modular forms). **CayleySpec**: First complete formalization of the dictionary between Cayley graph spectral theory and Hecke eigenvalue theory. Includes 5 core modules with 3,265 Lean jobs, 0 errors, 0 admitted theorems. All theorems proven including boundedness at cusps. **L-Function Zeros**: Discovery of two-population structure in zero spacing statistics - dim=1 forms exhibit GUE statistics (Brody β=1.88), dim≥2 forms exhibit near-Poisson statistics (β=0.24). 6% of dim≥2 forms retain GUE statistics as low-dimension, small-level outliers.