Mathematical Physics

Motivation

Reflection positivity and infrared bounds form a standard finite-volume route from the geometry of a lattice reflection to quantitative control of long wavelength fluctuations. In the classical argument, reflection positivity supplies a Cauchy--Schwarz inequality for reflected observables, while Fourier diagonalization of the lattice Laplacian identifies the free covariance used in the infrared comparison. These ingredients underlie rigorous results on continuous-symmetry lattice systems in Fröhlich, Simon, and Spencer's development of infrared bounds and spontaneous symmetry breaking (1976), and the general theory of reflection positivity developed by Fröhlich, Israel, Lieb, and Simon (1978). Related technology appears in Fröhlich and Spencer's treatment of the two-dimensional Abelian spin systems and Coulomb gas (1981).

The analytic and model-specific theorems are substantial, but their finite algebraic interface is sharply separable. This mission isolates that interface so later clock, XY, and Gaussian-domination developments can share one checked notion of reflection, one spectral covariance convention, and one treatment of the constant mode.

Setting

Let $X$ be a finite set of configurations on one side of a reflection plane. A full split configuration is a pair $(x,y)\in X\times X$, and reflection exchanges its two entries. A plus-half observable is a function $F:X\to \mathbb R$ lifted to $X\times X$ through the first coordinate. Its reflected copy therefore depends on the second coordinate.

A split weight is specified by a finite feature index $A$, real coefficients $c_a$, and features $\phi_a:X\to\mathbb R$:

$$W(x,y)=\sum_{a\in A}c_a\phi_a(x)\phi_a(y).$$

For a finite family of plus-half observables $F_i$, the reflected kernel is

$$K_{ij}=\sum_{(x,y)\in X\times X} W(x,y)F_i(x)F_j(y).$$

A real matrix is positive semidefinite here when it is symmetric and its quadratic form is nonnegative on every real coordinate vector.

The spectral side uses a finite mode set $I$ with a distinguished zero mode $0$. An infrared spectrum consists of a function $\lambda:I\to\mathbb R$ that is nonnegative and vanishes exactly at $0$. For $\beta>0$, the free mode covariance is diagonal, equals zero at the constant mode, and has entry

$$G_{kk}=\frac{1}{\beta\lambda_k}$$

away from zero. Covariance domination is tested only on source vectors whose zero-mode coordinate vanishes. The concrete spectral fixture is the $4\times4$ periodic square lattice, with tensor-product discrete Fourier modes and the nearest-neighbor graph Laplacian.

Formalization targets

Finite reflection positivity

The first target identifies the split reflection pairing with the explicit double sum over the two halves. Under $c_a\ge0$, the resulting reflected kernel must be positive semidefinite:

$$\sum_{i,j}u_iK_{ij}u_j\ge0.$$

Every such kernel must satisfy the two-observable chessboard inequality

$$K_{ij}^{2}\le K_{ii}K_{jj}.$$

Typed finite spectrum

For every Torus-4 frequency $k$ and site $x$, the registered Fourier mode $\psi_k$ must satisfy the pointwise eigenvalue equation

$$(\Delta_{\mathrm{T4}}\psi_k)(x)=\lambda_k\psi_k(x).$$

The eigenvalues must be nonnegative and vanish exactly at the constant mode, and these laws must be packaged as the same spectrum type consumed by the infrared definitions.

Zero-mode-restricted infrared bound

The diagonal free covariance must be positive semidefinite for $\beta>0$. If an interacting covariance $C$ is quadratically dominated by $G$ on sources with $u_0=0$, then every nonzero Fourier mode must satisfy

$$C_{kk}\le\frac{1}{\beta\lambda_k}\qquad(k\ne0).$$

Two finite counterfixtures are part of the target. They assert that an arbitrary full-vertex reflected two-point matrix need not be positive semidefinite, and that domination restricted away from the zero mode need not extend to full-matrix domination.

Significance

The resulting interface prevents three substitutions that otherwise look notational but change the theorem. Reflection positivity is tested on observables supported on one half rather than on an arbitrary matrix indexed by all vertices. The infrared comparison excludes the constant mode rather than forcing a fluctuating zero mode below a covariance with zero diagonal. The graph-Laplacian eigenvalue is connected to the Fourier mode by an explicit pointwise theorem rather than by assigning a function the name laplacianEigenvalue.

Several ingredients already have machine-checked Lean proofs in the LeanProofs repository: the finite matrix Cauchy--Schwarz theorem, the Torus-4 DFT diagonalization and zero-mode theorem, and the diagonal free-covariance calculation. This mission reorganizes those results around a corrected consumer boundary and adds the split-half and off-zero adapters. It does not present the finite statements as new mathematics.

Difficulty

The main difficulty is maintaining the correct domain at each interface. A reflection of lattice sites does not by itself imply positive semidefiniteness of a correlation matrix indexed by every site; the tested observables and their support are part of the assertion. Likewise, a free covariance whose constant-mode entry is defined to be zero cannot dominate an arbitrary covariance on all source vectors. Finally, a Fourier multiplier used for a pseudospectral derivative is not automatically the eigenvalue of the nearest-neighbor graph Laplacian. The formal statements must keep these three objects distinct.

Formalization scope

All configuration, feature, observable, and mode types are finite. Kernels, weights, coefficients, source vectors, and quadratic forms are real. Complex numbers occur only in the explicit discrete Fourier modes. Reflected pairings are unnormalized finite sums; no partition function or probability measure is introduced. The inverse temperature satisfies $\beta>0$. The distinguished zero mode is part of the spectrum interface, and infrared domination is restricted to source vectors that vanish at that coordinate.

The mission does not assert reflection positivity of a clock or XY Gibbs measure, nonnegative Fourier coefficients of a physical cross-bond weight, Gaussian domination, a thermodynamic limit, a Kosterlitz--Thouless transition, or a universal jump. It also does not identify the Torus-4 graph spectrum with the Grid3 pseudospectral multiplier from the Fourier--Hodge packet. Those are separate future missions requiring additional model and analytic input.

The reusable outputs are the split-weight RP interface, the finite positive-semidefinite kernel API, the typed spectrum object, and the zero-mode-restricted domination predicate. Contributions should preserve the explicit half support and zero-mode restrictions; a proof obtained by adding the desired conclusion as a hypothesis is outside scope.

Selected references

• J. Fröhlich, B. Simon, and T. Spencer, Infrared bounds, phase transitions and continuous symmetry breaking, Communications in Mathematical Physics 50 (1976), 79--95. https://doi.org/10.1007/bf01608557
• J. Fröhlich, R. Israel, E. H. Lieb, and B. Simon, Phase transitions and reflection positivity. I. General theory and long range lattice models, Communications in Mathematical Physics 62 (1978), 1--34. https://doi.org/10.1007/bf01940327
• J. Fröhlich and T. Spencer, The Kosterlitz--Thouless transition in two-dimensional Abelian spin systems and the Coulomb gas, Communications in Mathematical Physics 81 (1981), 527--602. https://doi.org/10.1007/bf01208273
• LeanProofs, ReflectionPositivityInfraredBound.lean, exact repository snapshot dbf503b2909cc17787d40a21eb75a0c9354cc6ef. https://github.com/MonumentalSystems/LeanProofs/blob/dbf503b2909cc17787d40a21eb75a0c9354cc6ef/LeanProofs/StatMech/ReflectionPositivityInfraredBound.lean

Motivation

Two-dimensional lattice models admit topological defects whose energetic cost competes with their configurational multiplicity. The later stages of a finite vortex argument therefore need a trustworthy bridge from a prescribed vorticity to the least quadratic energy of a compatible field. This mission isolates that bridge. It does not attempt a phase-transition theorem; it establishes only the finite-dimensional variational identity on which a later, model-specific energy estimate can rest.

The algebra belongs to finite discrete Hodge theory. A finite cochain complex supplies a differential from degree one to degree two and an adjoint codifferential in the reverse direction. A normalized Green operator inverts the degree-two Laplacian on realizable vorticities and annihilates the harmonic obstruction. Such finite-complex harmonic methods go back at least to Beno Eckmann's 1944 treatment of harmonic functions and boundary-value problems on complexes. The vortex motivation comes from the energy--entropy mechanism discussed by Kosterlitz and Thouless for two-dimensional systems, but no claim from their thermodynamic analysis is included here.

Setting

Let $C^0,C^1,C^2$ be finite-dimensional real inner-product spaces. A finite Hodge complex consists of linear maps

$$d_0:C^0\to C^1,\qquad d_1:C^1\to C^2,$$

together with specified adjoints $\delta_1$ and $\delta_2$, and the cochain relation $d_1d_0=0$. The degree-two Laplacian is

$$L_2=d_1\delta_2.$$

The vorticity space is $\operatorname{range}(d_1)$. A normalized degree-two Green owner supplies a unique self-adjoint linear map $G:C^2\to C^2$ satisfying both inverse identities with the orthogonal projector onto that range, taking values in the range, and vanishing on $\ker(\delta_2)$.

For a realizable source $\omega\in\operatorname{range}(d_1)$, define the canonical one-cochain

$$a_\omega=\delta_2G\omega.$$

The physical vortex normalization scales the prescribed vorticity by $2\pi$, so the canonical physical field is $2\pi a_\omega$. For a coupling $J\in\mathbb R$, the quadratic energy of $a\in C^1$ is

$$E_J(a)=\frac J2\lVert a\rVert^2.$$

Formalization targets

Exact Green variational decomposition

For every realizable $\omega$ and every field $a$ satisfying $d_1a=2\pi\omega$, establish

$$E_J(a)=2\pi^2J\langle\omega,G\omega\rangle +E_J\bigl(a-2\pi\delta_2G\omega\bigr).$$

The equality is required for every real $J$. Its unscaled components assert the exact Poisson equation, closedness and orthogonality of the residual, the Pythagorean norm decomposition, and the identity

$$\lVert\delta_2G\omega\rVert^2=\langle\omega,G\omega\rangle.$$

One-sided minimum-energy bound

For $J\ge0$, conclude

$$2\pi^2J\langle\omega,G\omega\rangle\le E_J(a).$$

Two controls are part of the target boundary: zero coupling must not identify a unique minimizer, and zero vorticity must not imply that the underlying field or its positive-coupling energy vanishes.

Significance

The result separates universal finite linear algebra from geometry that depends on a particular lattice. Once a periodic square torus is registered as a finite Hodge complex, a later theorem may specialize the Green quadratic form to dipole charges and investigate its dependence on separation. Entropy can then be compared with a genuine energy inequality without redefining energy through the desired conclusion.

Formalizing this layer provides reusable interfaces for Poisson solvability, orthogonal residuals, exact quadratic energy splitting, and the nonnegative-coupling lower bound. It also makes normalization errors visible: the factor $2\pi$ in the source and the factor $J/2$ in the energy force the coefficient $2\pi^2J$. The underlying Green-owner infrastructure already has a machine-checked implementation in LeanProofs; the propositions in this mission are new proof obligations derived from that interface.

Difficulty

The central issue is not an asymptotic estimate. It is maintaining the exact relationship among the Laplacian sign, the orthogonal projector, the Green normalization, adjointness, and the physical $2\pi$ scaling. A proof that silently projects a non-realizable source changes the problem. A proof that divides by $J$ loses the $J=0$ case. A proof that treats zero vorticity as a zero-field assertion discards closed and harmonic residuals. Each of these shortcuts is ruled out by the formal target or its controls.

Formalization scope

The Lean development uses arbitrary finite-dimensional real inner-product spaces rather than a concrete torus. All maps are continuous only through finite-dimensional linear structure; there is no measure theory, probability, or limiting process. A source is explicitly required to lie in $\operatorname{range}(d_1)$. The exact decomposition permits every real $J$, while the inequality requires $0\le J$. Existence of a Green owner is supplied as data; this mission neither constructs a second inverse nor changes the existing normalization.

The mission does not define integer charge, torus distance, plaquette winding, or a concrete lattice Laplacian. It proves no logarithmic Green estimate, cosine-energy comparison, entropy bound, Gibbs statement, vortex proliferation result, thermodynamic limit, BKT transition, or universal jump. In particular, the target cannot be satisfied by choosing a convenient torus size or hard-coding a Green kernel: it is group-generic finite-dimensional algebra conditional on the stated Hodge and Green structures.

Contributions are welcome on the independent Poisson, orthogonality, norm, scaling, and control nodes. A later mission can add the square-torus realization and the separate analytic capacity estimate needed for a sharp logarithmic lower bound.

Selected references

• Beno Eckmann, Harmonische Funktionen und Randwertaufgaben in einem Komplex, Commentarii Mathematici Helvetici 17 (1944/45), 240--255. https://doi.org/10.1007/BF02566245
• J. M. Kosterlitz and D. J. Thouless, Ordering, metastability and phase transitions in two-dimensional systems, Journal of Physics C 6 (1973), 1181--1203. https://doi.org/10.1088/0022-3719/6/7/010
• LeanProofs, finite Hodge Green-owner foundation at commit dbf503b2909cc17787d40a21eb75a0c9354cc6ef. https://github.com/MonumentalSystems/LeanProofs/commit/dbf503b2909cc17787d40a21eb75a0c9354cc6ef