The Four-Dimensional Anderson Model: Formalization Blueprint

1 Introduction

This blueprint organizes the Lean 4 formalization of the main theorem of Deng–Shen, The four-dimensional Anderson model: a case study for critical SPDEs (arXiv:2607.10105; all references use the v1 numbering). The accompanying documentation provides complementary views. The DESIGN.md describes architecture and scope; PAPER_MAP.md gives node IDs and paper-level dependencies (the uses-labels here reuse those IDs verbatim); PAPER_TO_LEAN.md gives exact paper-number-to-public-declaration links; and PAPER_INDEX.md is the generated module inventory. This chapter states the target and the global conventions; it contains no formalizable nodes.

1.1 The target

Let \(\xi \) be spatial white noise on \(\mathbb {T}^4 = [-\pi ,\pi ]^4\), let \(\rho \) be a smooth cutoff (Section 1.2), and \(\xi _\varepsilon = \rho _\varepsilon * \xi \). Consider

\[ \mathcal{L}_\varepsilon \; =\; 1 - \Delta - \lambda _\varepsilon \, \xi _\varepsilon + \mathcal{C}_\varepsilon , \qquad \lambda _\varepsilon = \frac{\lambda }{\sqrt{\lvert \log \varepsilon \rvert }}, \]

with the explicit renormalization constants \(\mathcal{C}_\varepsilon = \sum _{q \le A}\mathcal{C}_{2q}\), \(A = \lfloor \lvert \log \varepsilon \rvert \rfloor \), of Chapter 6. The paper’s Theorem 1.1 asserts that \(\mathcal{H}_\varepsilon = \lambda _\varepsilon ^{-1}(G_\varepsilon - G)\) converges in law, as \(\varepsilon \to 0^+\), to an explicit centered Gaussian field.

Formal main statement (design in DESIGN.md §2): for every cutoff \(\rho \) there is \(\lambda _0(\rho ) {\gt} 0\) such that for \(0 {\lt} \lambda {\lt} \lambda _0\) and every finite family of Fourier modes \((\alpha _j,\beta _j)_{j\le s}\), the random vectors \(\big(\widehat{\mathcal{H}_\varepsilon }(\alpha _j,\beta _j)\big)_{j\le s}\) converge in distribution to the corresponding Gaussian limit (Chapter 9). This finite-mode form is exactly what the paper’s proof establishes at (3.34); no distribution-space topology enters.

External input. The single statement quoted by the paper from Gabriel–Rosati (arXiv:2602.22509) — Proposition 3.6, our node 49 — is treated as an explicit hypothesis: it is stated in Lean in full, marked external here, never assumed as an axiom, and the main theorem main_conditional takes it as an argument. No unconditional main is declared; a proof of the cited Gabriel–Rosati result is outside the scope of this repository.

1.2 Conventions

The following conventions are fixed once and used silently everywhere; getting them wrong invalidates constants globally, so they form the fixed “normalization ledger”.

  1. Torus and measure. \(\mathbb {T}^4\) is the product of four copies of \(\mathbb {R}/2\pi \mathbb {Z}\); the reference measure is Lebesgue measure of total mass \((2\pi )^4\). mathlib’s AddCircle Fourier API is normalized against probability Haar measure; the translation dictionary (all \(2\pi \)-factors) is recorded with the Lean definitions.

  2. Characters and coefficients. \(e_k(x) = e^{i k\cdot x}\); for kernels, \(\widehat K(\alpha ,\beta ) = \iint e^{i(\alpha \cdot x + \beta \cdot y)}K(x,y)\, \mathrm{d}x\, \mathrm{d}y = \langle e_{-\alpha },\, K e_\beta \rangle \) with the inner product conjugate-linear in the first slot (paper (3.23); sign frozen by a rank-one roundtrip test).

  3. Cutoff. \(\rho \colon \mathbb {R}^4 \to \mathbb {R}\) smooth, nonnegative, supported in the ball of an explicit radius \(R\) (no unit-ball normalization), invariant under coordinate permutations and sign flips (the class \(\mathcal{E}\), node 21), with \(\int \rho = 1\). Torus objects arise by \(2\pi \mathbb {Z}^4\)-periodization; mollification is equivalently the Fourier multiplier \(\widehat{\rho }(\varepsilon k)\).

  4. White noise. Defined through Fourier coefficients: two independent standard real Gaussians per \(\{ \pm k\} \)-orbit and one for the zero mode, assembled so that \(\mathbb {E}[g_k g_l] = \mathbf{1}_{k=-l}\) and \(\mathbb {E}[g_k \overline{g_l}] = \mathbf{1}_{k=l}\). Since these characters are orthonormal for probability Haar while the paper uses Lebesgue measure of mass \((2\pi )^4\), the physical field is \(\xi _\varepsilon =(2\pi )^{-2}\sum _k \widehat\rho (\varepsilon k)g_ke_k\). This half-density is part of the normalization ledger.

  5. Junk values. Partial operations are totalized by junk values (\(G_\varepsilon := 0\) off the invertibility event, junk limit law for \(\lambda ^2 \ge 2\pi ^2\), etc.); every estimate carries the hypotheses that exclude the junk branch.

  6. Constants. No asymptotic notation in Lean statements. Constants referenced by several nodes are named definitions (\(C_0 {\gt} 1000\), \(D = e^{C_0^{10}}\), …); one-off line constants are existentially quantified. All constants may depend on \(\rho \) (including its support radius \(R\)).

  7. Word model. All permutation sums of the paper’s §5.4 are stated over words (maps with prescribed fiber sizes). The definitional ledger \(\mathrm{paperSum} = \big(\prod _{\mathfrak {l}} m_{\mathfrak {l}}!\big) \cdot \mathrm{wordSum}\) (node 13) aligns statements with the paper’s labeled normalization: paper-facing statements put \(\mathrm{paperSum}\) on the left with the paper’s right-hand sides verbatim.