OAI/Probability/InvariantIsing/Cavity/CavityRationalLabelIdentities.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Both sides of the physical rational-count coupling have exactly the labels of the single global spectral family.

  1. lemma OAI.InvariantIsing.cavityRationalFullGroup_eq line 13
  2. lemma OAI.InvariantIsing.cavityRationalBase_label line 22
  3. lemma OAI.InvariantIsing.cavityRationalBase_canonical_label line 32
  4. lemma OAI.InvariantIsing.cavityRationalBase_partition line 41