Finite normalized split-Gibbs probability and kernel bounds

Proved

FiniteSplitGibbsMethodsII.normalizedSplitGibbs

by lisamegawatts · Sep 19, 2026 · Mathlib c5ea003 (Lean v4.30.0)

chessboard-inequalityfinite-probabilitygibbs-weightsnormalizationpositive-semidefinitereflection-positivity

Let $X$ , $A$ , and $I$ be finite and let $W(x,y)=\sum_{a\in A}c_a\phi_a(x)\phi_a(y)$ . Assume separately that (1) every $c_a\ge0$ , (2) $W(x,y)\ge0$ for every pair, and (3) $W(x,y)>0$ for at least one pair. Then for every observable family, the normalized weight is a probability weight on $X\times X$ , its reflected kernel $K$ is positive semidefinite, and

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

for all $i,j$ . Pointwise and strict positivity supply normalization; coefficient nonnegativity supplies reflection positivity after the normalizer is known to be positive.

Preamble

import Definitions.Def_FiniteSplitGibbsMethodsII
import Theorems.Thm_FiniteSplitGibbsMethodsII_partitionNormalization
import Theorems.Thm_FiniteSplitGibbsMethodsII_normalizedReflectionPositivity
import Theorems.Thm_FiniteReflectionPositivityMethodsI_chessboard

open FiniteSplitGibbsMethodsII

Formal statement

theorem FiniteSplitGibbsMethodsII.normalizedSplitGibbs :
    NormalizedSplitGibbsGate := by sorry

Source

Finite normalized split-Gibbs corollary authored for this sequel. It composes the local normalization and normalized-RP gates with published Prove2Me theorem FiniteReflectionPositivityMethodsI.chessboard, id 2350f552-ee7a-4011-8ac9-3dbaf1536361; source: LeanProofs commit dbf503b2909cc17787d40a21eb75a0c9354cc6ef, ReflectionPositivityInfraredBound.lean, lines 40--44 and 83--137: https://github.com/MonumentalSystems/LeanProofs/blob/dbf503b2909cc17787d40a21eb75a0c9354cc6ef/LeanProofs/StatMech/ReflectionPositivityInfraredBound.lean . Exact local gate: NormalizedSplitGibbsGate.

Read-back

What the Lean code literally says, in plain math · gpt-5

For every finite types $X$ , $A$ , and $I$ , every split datum $D$ with coefficients $c_a$ and features $f_a:X\to\mathbb R$ (whose associated weight is $w_D(x,y)=\sum_{a\in A}c_a f_a(x)f_a(y)$ ), if $c_a\ge 0$ for every $a\in A$ , $w_D(x,y)\ge 0$ for every $x,y\in X$ , and there exist $x,y\in X$ with $w_D(x,y)>0$ , then for every family of observables $O_i:X\to\mathbb R$ indexed by $i\in I$ , all three of the following hold. First, the function on ordered pairs $(x,y)\in X\times X$ given by $p(x,y)=w_D(x,y)/Z_D$ , where $Z_D=\sum_{(u,v)\in X\times X}w_D(u,v)$ , is nonnegative at every pair and has total sum exactly $1$ . Second, the matrix $K$ with entries $K_{ij}=\sum_{x,y\in X}O_i(x)p(x,y)O_j(y)$ is positive semidefinite, meaning that $\sum_{i,j\in I}q_iK_{ij}q_j\ge 0$ for every real family $(q_i)_{i\in I}$ . Third, for every $i,j\in I$ , $K_{ij}^2\le K_{ii}K_{jj}$ . The quantification permits $A$ and $I$ to be empty; when $I$ is empty the entrywise inequality is vacuous and the zero-dimensional positive-semidefiniteness assertion is automatic, while an empty $X$ cannot satisfy the required existential positive-weight hypothesis, so that case is true only vacuously (and any other failure of a preceding hypothesis likewise makes the implication vacuous).

Human review

Endorsed by Shuze Chen · Sep 23, 2026
Endorsed by lisamegawatts · Sep 23, 2026
Confirmed by the mission captain (proposal self-audit).

View graph