Confinement and Clustering at Strong Coupling in Lean 4, without Cluster Expansions

Lean 4 proofs, with no cluster expansion, of Wilson's area law for rectangular loops for any gauge group whose character detects a central element, including SU(N), U(1) and Z2, in every dimension at strong coupling on finite tori; of decay of Polyakov loop correlators at every temporal extent; and of exponential clustering in Euclidean time for all bounded local observables and every gauge group, uniformly in the volume. An earlier Lean proof of the area law, for SU(N) and all closed loops by a formalised Kotecky-Preiss expansion, is due to L. Eriksson. At d = 4 the range here is |beta_W| < 1/12, about 1.5 million times beyond the largest coupling that the hypotheses of that volume-uniform theorem allow. The library depends only on propext, Classical.choice and Quot.sound, enforced in the build. All results hold at fixed lattice spacing. No theorem here concerns the continuum limit or the Clay Millennium problem. Code: github.com/bharathsrivats/fisher-lorentz-formalization, tag v2.1.0.