Reflection positivity after positive normalization

Proved

FiniteSplitGibbsMethodsII.normalizedReflectionPositivity

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

normalizationpositive-semidefinitereflection-positivitysplit-weights

Let $X$ , $A$ , and $I$ be finite, and let $W(x,y)=\sum_{a\in A}c_a\phi_a(x)\phi_a(y)$ have $c_a\ge0$ . If $Z=\sum_{x,y}W(x,y)>0$ , then for every family $F_i:X\to\mathbb R$ , the reflected kernel constructed from $W/Z$ is a symmetric positive-semidefinite real matrix. This theorem uses coefficient nonnegativity and positivity of the scalar normalizer; it neither assumes nor concludes pointwise nonnegativity or probability normalization.

Preamble

import Definitions.Def_FiniteSplitGibbsMethodsII
import Theorems.Thm_FiniteReflectionPositivityMethodsI_splitWeightReflectionPositivity

open FiniteSplitGibbsMethodsII

Formal statement

theorem FiniteSplitGibbsMethodsII.normalizedReflectionPositivity :
    NormalizedReflectionPositivityGate := by sorry

Source

Positive-scalar normalization corollary of the published Prove2Me theorem FiniteReflectionPositivityMethodsI.splitWeightReflectionPositivity, id 25912f71-137c-4b0d-b43b-3e25dcbd7163. Its source is LeanProofs commit dbf503b2909cc17787d40a21eb75a0c9354cc6ef, ReflectionPositivityInfraredBound.lean, lines 40--56: https://github.com/MonumentalSystems/LeanProofs/blob/dbf503b2909cc17787d40a21eb75a0c9354cc6ef/LeanProofs/StatMech/ReflectionPositivityInfraredBound.lean . Exact local gate: NormalizedReflectionPositivityGate.

Read-back

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

For every universe-level-0 triple of types $X,A,I$ , each equipped with a finite enumeration, and every split-weight datum $D$ on $X$ indexed by $A$ , if $D.coefficient(a)≥0$ for every $a∈A$ and the split partition function $Z_D$ , namely the finite sum of $D.weight(ω.1,ω.2)$ over all full configurations $ω$ of $X$ , is strictly positive, then for every observable family $O:I→X→ℝ$ , the $I$ -by- $I$ reflected kernel formed from the normalized weight $(l,r)↦D.weight(l,r)/Z_D$ and $O$ is positive semidefinite. The theorem assumes no pointwise nonnegativity of $D.weight$ . All three types are permitted to be empty; whenever the strict-positivity hypothesis on $Z_D$ is impossible the implication is vacuous, while an empty $I$ leaves the positive-semidefinite assertion with only its empty-index meaning.

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