OAI/Probability/InvariantIsing/Cavity/CavityPhysicalEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The exact original-spin energy difference is the finite random-block cavity factor. All spectral-image and cavity-coordinate identities are proved for the actual orthogonal matrix.

  1. theorem OAI.InvariantIsing.cavity_physical_energy_difference line 16