Pointwise nonnegativity does not imply reflection positivity
ProvedFiniteSplitGibbsMethodsII.pointwisePositiveNoGoOn the two-element set, define the symmetric weight
Every entry is nonnegative. As a weight on the four pairs, it has a positive partition function and normalizes to a probability weight. Nevertheless, 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.
import Definitions.Def_FiniteSplitGibbsMethodsII open FiniteSplitGibbsMethodsII
theorem FiniteSplitGibbsMethodsII.pointwisePositiveNoGo :
PointwisePositiveNoGoGate := by sorryRead-back
What the Lean code literally says, in plain math · gpt-5
On the fixed two-element type , define when and otherwise, regard also as a weight on the four ordered pairs, and let be when and otherwise. The theorem asserts the conjunction that every is nonnegative; for every ; its partition sum is strictly positive; the normalized pair-weight is everywhere nonnegative and sums to exactly ; the matrix is not positive semidefinite; the reflected matrix with entries (which is again ) is not positive semidefinite; and the reflected matrix with entries (which is ) 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.
Confirmed by the mission captain (proposal self-audit).