8.1. Summary🔗

Manuscript main.tex, version 2026-09-13 revision (numbers synced 2026-09-13). Verified declarations in theorem_names: 369.

Conventions. Bias sign: the 2026-09-13 revision writes neurons as sigma(<a,x> - b), where b = -c is the negative of the bias c of the previous revision and of the Lean definitions (OperatorRidgelet.ridgelet, integralNetwork, ... still use <a,x> + c). The two coordinates are related by the measure-preserving involution tau(a,c) = (a,-c); no Lean statement is invalidated by the change, but the manuscript-to-Lean reading of every bias-dependent statement goes through tau. Also renamed in the manuscript without mathematical effect: H -> \mathcal H, Y -> \mathcal Y (outY), \mathcal G_Q -> F_Q, scalar activation beta -> sigma, operator activation sigma -> Sigma, spectral density G -> g, target g_G -> f_g, coefficient gamma_G -> gamma_g, \mathcal N(0,Q) -> mu_Q, Gaussian activation Phi -> sigma_Gauss, operator layer \mathcal F -> F, Dirichlet Green operator \mathsf G -> L_D^{-1}, the Gaussian-parameter ReLU target F_Q -> f_{ReLU,Q}.

The status of an item is that of STATUS.md: verified when every Lean theorem of the item is in theorem_names; partial k/n when k of its n Lean theorems are; stated when all of its Lean names exist (theorems in Challenge, definitions in the library) but none is verified; defined when its Lean names are all definitions in the library, so that there is nothing for comparator to check; and — when some Lean name is not yet stated. The full table, with the consistency warnings of the generator, is STATUS.md in the repository.