OAI/Probability/InvariantIsing/Cavity/OffsetMinimumIncrement.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A minimum at the next repeated-block dimension controls the genuine base/cavity increment. Dimension casts do not impose a new model hypothesis.

  1. theorem OAI.InvariantIsing.offset_minimum_increment line 13