OAI/Probability/InvariantIsing/Cavity/ConsecutiveProductMinimumConsistency.lean
1 declarations, 0 contain sorry, 0 declared as axioms
Actual constrained minima supply all GG and Ward premises of block self-consistency.
- theorem
OAI.InvariantIsing.consecutive_product_minimizers_weak_consistencyline 13