Reflection positivity does not imply a positive normalizer
ProvedFiniteSplitGibbsMethodsII.zeroWeightNoGoFor any finite , take one constant split feature with coefficient zero. Its coefficient and raw weight are nonnegative, with the raw weight identically zero, so
For every finite observable family, the raw reflected kernel is positive semidefinite, but the expression called the normalized split weight is not a probability weight on . Hence coefficient and raw-weight nonnegativity together with raw reflection positivity do not imply a positive partition function or successful normalization; a separate nonzero or strict-positivity hypothesis is required.
import Definitions.Def_FiniteSplitGibbsMethodsII import Theorems.Thm_FiniteReflectionPositivityMethodsI_splitWeightReflectionPositivity open FiniteSplitGibbsMethodsII
theorem FiniteSplitGibbsMethodsII.zeroWeightNoGo :
ZeroWeightNoGoGate := by sorryRead-back
What the Lean code literally says, in plain math · gpt-5
For every type (with no finiteness assumption in the first two clauses), form the split datum indexed by the one-element type whose sole coefficient is and whose feature has value at every point. The theorem asserts the conjunction of the following: for every type and every , the coefficient is nonnegative; for every type and every , the associated weight is nonnegative; for every finite type , the partition sum equals ; for every finite types and and every observable family , the reflected matrix with entries is positive semidefinite; and for every finite type , the normalized pair-weight is not a probability weight (that is, it does not simultaneously have nonnegative values and total sum ). In fact the datum's associated weight and every displayed reflected matrix are identically zero; real division is total, so , and the normalized weight therefore has total sum , including when is empty. Empty makes the second universal clause vacuous and empty makes the reflected-matrix assertion zero-dimensional, but the final non-probability assertion still applies to every finite , empty or not.
Confirmed by the mission captain (proposal self-audit).