Uniform control through the physical scale
The construction must carry one Wilson-law family through the multiscale flow without replacing the difficult infrared regime by a different model.
Proof overview
One construction, carried from the lattice to the quantum spectrum.
The argument is constructive: the continuum theory and its positive gap are produced from a concrete regulated family rather than postulated separately.
Unconditional proof claimed in Volumes I–III. Independent expert review ongoing.
- 1
Regulator
Start with the Wilson theory
For a fixed compact simple global form, the construction begins with gauge-invariant Wilson measures on finite four-dimensional lattices.
- 2
Renormalisation
Control every physical scale
A multiscale analysis follows the same finite-law family from the ultraviolet regime through dimensional transmutation and into the infrared.
- 3
Compactness
Take the continuum limit
Cofinal lattice rows converge to reflection-positive Euclidean correlation functions on ℝ⁴ while retaining nontrivial observables.
- 4
OS → Wightman
Reconstruct the quantum theory
Osterwalder–Schrader reconstruction turns the Euclidean data into a relativistic Hilbert-space theory with fields, vacuum, translations, and Hamiltonian.
- 5
Spectrum
Extract the mass gap
Quantitative decay and transfer contraction exclude Hamiltonian spectrum in an interval above the vacuum, producing Δ > 0.
The decisive bridge
Decay in Euclidean time becomes a gap in quantum energy.
Reflection positivity supplies a positive time-translation semigroup. Once the centred observables contract uniformly, spectral calculus shows that no non-vacuum state can carry arbitrarily small positive energy.
∥e−tH│Ω⊥∥ ≤ e−tΔ
Where to slow down
The difficult steps are marked, not polished flat.
The proof guide distinguishes routine infrastructure from the places where the argument carries its real mathematical load.
A nontrivial continuum theory on ℝ⁴
Compactness alone is not enough: reflection positivity, Euclidean covariance, local observables, and marked nontriviality must survive both limits.
Decay promoted to a Hamiltonian gap
The spectral step must exclude every non-vacuum low-energy state—not merely show decay for one convenient correlator.
Supporting verification
Formalisation checks the load-bearing logical chain.
Selected spectral, continuum-extraction, and reconstruction arguments are mirrored in Lean. The formal development is used to expose hidden dependencies and verify the composition of the proof’s major components.
The mathematical manuscript remains the authoritative statement of the claimed proof; formalisation is an additional verification layer.
Lean verification programme