Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Pointwise nonnegativity does not imply reflection positivity

Proved
FiniteSplitGibbsMethodsII.pointwisePositiveNoGo

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

counterexamplenonnegativitypositive-semidefinitereflection-positivity

On the two-element set, define the symmetric weight

W(i,j)={1,i=j,2,i≠j.W(i,j)=\begin{cases}1,&i=j,\\2,&i\ne j.\end{cases}W(i,j)={1,2,​i=j,i=j.​

Every entry is nonnegative. As a weight on the four pairs, it has a positive partition function and normalizes to a probability weight. Nevertheless, WWW is not positive semidefinite, and the reflected delta-observable kernels generated by both the raw weight and its normalized probability weight are not positive semidefinite. Thus symmetry, pointwise nonnegativity, and successful probability normalization do not supply the coefficient-based split structure needed for reflection positivity.

Preamble
import Definitions.Def_FiniteSplitGibbsMethodsII

open FiniteSplitGibbsMethodsII
Formal statement
theorem FiniteSplitGibbsMethodsII.pointwisePositiveNoGo :
    PointwisePositiveNoGoGate := by sorry
Source
Finite counterfixture authored for this sequel to prevent replacing the coefficient-based split hypothesis in published theorem 25912f71-137c-4b0d-b43b-3e25dcbd7163 by pointwise nonnegativity. Inherited interface source: LeanProofs commit dbf503b2909cc17787d40a21eb75a0c9354cc6ef, ReflectionPositivityInfraredBound.lean, lines 40--56. Exact local gate: PointwisePositiveNoGoGate.
Read-back

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

On the fixed two-element type Fin⁡(2)={0,1}\operatorname{Fin}(2)=\{0,1\}Fin(2)={0,1}, define Wij=1W_{ij}=1Wij​=1 when i=ji=ji=j and Wij=2W_{ij}=2Wij​=2 otherwise, regard WWW also as a weight on the four ordered pairs, and let δi(x)\delta_i(x)δi​(x) be 111 when x=ix=ix=i and 000 otherwise. The theorem asserts the conjunction that every WijW_{ij}Wij​ is nonnegative; Wij=WjiW_{ij}=W_{ji}Wij​=Wji​ for every i,ji,ji,j; its partition sum Z=∑i,jWij=6Z=\sum_{i,j}W_{ij}=6Z=∑i,j​Wij​=6 is strictly positive; the normalized pair-weight Wij/6W_{ij}/6Wij​/6 is everywhere nonnegative and sums to exactly 111; the matrix W=(1221)W=\begin{pmatrix}1&2\\2&1\end{pmatrix}W=(12​21​) is not positive semidefinite; the reflected matrix with entries ∑x,yδi(x)Wxyδj(y)\sum_{x,y}\delta_i(x)W_{xy}\delta_j(y)∑x,y​δi​(x)Wxy​δj​(y) (which is again WWW) is not positive semidefinite; and the reflected matrix with entries ∑x,yδi(x)(Wxy/6)δj(y)\sum_{x,y}\delta_i(x)(W_{xy}/6)\delta_j(y)∑x,y​δi​(x)(Wxy​/6)δj​(y) (which is W/6W/6W/6) is not positive semidefinite. Here positive semidefinite means that every real quadratic form of the matrix is nonnegative. All indices range over exactly two elements, so none of these universal assertions is vacuous and no additional hypotheses are imposed.

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

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me