OAI/Probability/InvariantIsing/Cavity/CavityBaseWardLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Both Ward identities for the physical base array. The SO law is derived from its actual Haar eigenbasis, and its Gaussian realization is identified by the full array-law equality.

  1. theorem OAI.InvariantIsing.cavity_rotation_ward_limits line 16