OAI/Probability/InvariantIsing/Fields/SpinPriorContactContradiction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

At an actual positive-temperature contact minimum, the field directions and temperature direction contradict the identified limiting energy.

  1. theorem OAI.InvariantIsing.spinPriorContact_limit_contradiction line 18