anderson4d

Lean 4 + mathlib

The four-dimensional Anderson model

A conditional formalization of Deng–Shen Theorem 1.1, with the mathematical argument linked directly to its blueprint and checked Lean source.

Conditional scope complete 53 blueprint nodes 167 checked declarations 0 project sorrys

Start here

The proof at a glance

Read left to right. Every stage opens its exact blueprint node; the full graph records all 53 nodes and 103 dependency edges.

P-5.6 / P-5.7 / P-5.9Count & organizeHepp trees and permutation sums P-4.1Estimate kernelsPrimitive continuum bound R-322 / R-324Control momentsDeterministic parametrix bounds P-3.5b / P-redPass to probabilityWick reduction and good event P-mom / T-1.1Converge in lawGaussian moments to the main theorem

External input P-3.6: the uniform Gabriel–Rosati estimate enters only at the final probabilistic assembly, as an explicit theorem hypothesis rather than a Lean axiom.

Lean declaration
Open the full 53-node DAG Read the mathematical blueprint

Conditional Theorem 1.1

The public capstone

Prop36Family M rho → MainLawStatement M rho

For each fixed noise model and cutoff satisfying the external hypothesis, there is a positive coupling threshold below which every finite family of Fourier modes converges in distribution to the stated centered Gaussian limit. Lean records joint convergence through characteristic functions and derives the finite-vector form.

Paper statementTheorem 1.1 Blueprint nodeT-1.1 Lean declarationmain_conditional_law Checked sourceFinal.lean

Paper ↔ Lean

Load-bearing results

Each row links the paper result to its blueprint node and checked Lean declaration.

Theorem 1.1

Conditional convergence in law

Finite Fourier-mode families converge to the explicit Gaussian limit.

BlueprintLean
Proposition 3.6

Explicit external hypothesis

The uniform family estimate quoted from Gabriel–Rosati.

BlueprintLean
Proposition 4.1

Primitive continuum estimate

The analytic engine for singular kernel bounds.

BlueprintLean
Proposition 5.6

Hepp-tree volume bound

Controls the combinatorial volume assigned to each tree.

BlueprintLean
Proposition 5.7

Permutation-sum estimate

Bounds the structured sum over words and permutations.

BlueprintLean
Proposition 5.9

Inductive estimate

Closes the discrete multiscale induction.

BlueprintLean
Open the complete paper-to-Lean index

Provenance

Built to be inspected.

Formalization authors: Yu Deng, Hao Shen, and sairmath.

Based on Deng–Shen, “The four-dimensional Anderson model: a case study for critical SPDEs”.

See citation metadata and the Apache License 2.0.