OAI/Probability/InvariantIsing/Fields/SpinPriorContactTailOrder.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual joint minima enforce upper-tail order at their synchronized GG limit. All finite field directions are taken at those same minima.

  1. theorem OAI.InvariantIsing.spinPriorContact_limit_tail_order line 16