Mathematical Physics

The Vacuum Was Never Absent: A Machine-Checked Perron Theorem for Strictly Positive Kernels, and the Coupled-Slice Vacuum at Every Spatial Extent

Authors: Lluis Eriksson

Two companion papers established, for a Z_2 lattice gauge slice with a spatialcoupling, that the elementary route to the vacuum stops, and that the naturalreplacement - the Hilbert projective metric - is blind to the coupling anddegenerates in the volume. Both had to work around the same absence: the pinnedmathlib carries no Perron-Frobenius theorem. The first paper could therefore onlysay the vacuum had become unavailable; the second had to build its dominationbound from scratch, and could exhibit the vacuum in closed form only at two sites.This paper discharges that dependency. For a strictly positive kernel on a finitenonempty type we prove, in Lean 4 with mathlib: a strictly positive eigenvectorEXISTS; its eigenvalue is strictly positive; any two strictly positiveeigenvectors are proportional and share their eigenvalue; and every realeigenvector for that eigenvalue is a scalar multiple of it. Together with thedomination theorem of the companion paper this gives the Perron statement thelane needs: the eigenvalue is the spectral radius.The existence proof does not use a fixed-point theorem, because the pinnedmathlib revision contains none. It maximises r over the compact set of pairs(r,x) with x in the simplex and r x <= A x; maximality forces equality, since astrict inequality anywhere would let one further application of A produce anadmissible pair with a larger r. The bound that keeps the set compact is obtainedby summing the constraint: r = r * sum x <= sum (A x).The application is the point. At EVERY spatial extent, and for EVERY strictlypositive weight on the source configuration - the class that contains the coupledkernel of the first paper - the vacuum exists, is unique up to scale, and carriesthe spectral radius. The obstruction of that paper was never an absence; it wasan unavailability, and it was an unavailability of one route rather than of theobject.NO SPECTRAL GAP IS PROVED HERE, uniform in the volume or otherwise, and none isclaimed. Nothing in this paper is a claim about SU(N), the continuum limit, orthe Yang-Mills mass gap.

Comments: 6 Pages. Full core build 8427 jobs, 2564 oracle commands (2541 with axiom dependencies + 23 axiom-free), axiom set exactly {propext, Quot.sound, Classical.choice}, zero sorry and zero project axioms. All verification links anchored at a fixed commit.

Download: PDF

Submission history

[v1] 2026-07-29 06:36:35

Unique-IP document downloads: 8 times

ai.Vixra.org is a AI assisted e-print repository rather than a journal. Articles hosted may not yet have been verified by peer-review and should be treated as preliminary. In particular, anything that appears to include financial or legal advice or proposed medical treatments should be treated with due caution. ai.Vixra.org will not be responsible for any consequences of actions that result from any form of use of any documents on this website.

Add your own feedback and questions here:
You are equally welcome to be positive or negative about any paper but please be polite. If you are being critical you must mention at least one specific error, otherwise your comment will be deleted as unhelpful.