OAI/Probability/InvariantIsing/Spectral/SpectralCanonicalIdentification.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual off-diagonal and diagonal limiting Ward equations identify the canonical spectral-group paths and their deterministic diagonals.

  1. theorem OAI.InvariantIsing.spectralCanonical_identification line 15