OAI/Probability/InvariantIsing/Magnetic/MagneticHeightConcavity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Constrained finite-field concavity on the strict height cone, derived from the actual magnetic supporting planes.

  1. theorem OAI.InvariantIsing.concaveOn_constrainedHeightFieldValue line 14