OAI/Combinatorics/StripMass/BottomGauge.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. def OAI.CriticalStrip.Diagram.occupancyGauge line 14
  2. lemma OAI.CriticalStrip.Diagram.occupancyGauge_empty line 17
  3. lemma OAI.CriticalStrip.Diagram.rawColumn_bottom_gauge line 20
  4. lemma OAI.CriticalStrip.Diagram.lastCoefficient_bottom_gauge line 42
  5. lemma OAI.CriticalStrip.Diagram.Weights.vacantSouth_gauge line 68
  6. lemma OAI.CriticalStrip.Diagram.matrix_mulVec_gauge line 76
  7. lemma OAI.CriticalStrip.Diagram.normalizedVacuum_gauge_pair line 87
  8. lemma OAI.CriticalStrip.Diagram.spectralRow_den_ne_zero line 104
  9. lemma OAI.CriticalStrip.Diagram.rowReflectSpectral_weightsA line 108
  10. lemma OAI.CriticalStrip.Diagram.rowReflectSpectral_weightsU line 116
  11. lemma OAI.CriticalStrip.Diagram.rowReflectSpectral_weightsB line 120
  12. lemma OAI.CriticalStrip.Diagram.spectralWeights_A_ne_zero line 128
  13. lemma OAI.CriticalStrip.Diagram.spectralWeights_U_ne_zero line 140
  14. lemma OAI.CriticalStrip.Diagram.rowReflectSpectral_weights_other line 144
  15. def OAI.CriticalStrip.Diagram.rowGauge line 149
  16. lemma OAI.CriticalStrip.Diagram.rowGauge_ne_zero line 152
  17. lemma OAI.CriticalStrip.Diagram.reflectSpectral_rowGauge line 155
  18. lemma OAI.CriticalStrip.Diagram.rowReflectSpectral_bottom_tile line 168
  19. lemma OAI.CriticalStrip.Diagram.rowReflectSpectral_bottom_column line 178
  20. lemma OAI.CriticalStrip.Diagram.rowReflectSpectral_bottom_lastCoefficient line 194
  21. lemma OAI.CriticalStrip.Diagram.rowReflectSpectral_bottom_vacuum line 207
  22. lemma OAI.CriticalStrip.Diagram.rowReflectSpectral_bottom_rationalVacuum line 223
  23. lemma OAI.CriticalStrip.Diagram.matrix_one_sub_gauge line 234
  24. lemma OAI.CriticalStrip.Diagram.rowReflectSpectral_bottom_sourceTransfer line 246
  25. lemma OAI.CriticalStrip.Diagram.rowReflectSpectral_bottom_northSource line 255
  26. lemma OAI.CriticalStrip.Diagram.rowReflectSpectral_bottom_northNumerator line 272
  27. lemma OAI.CriticalStrip.Diagram.polynomialNorthSource_bottom_reflection line 326
  28. lemma OAI.CriticalStrip.Diagram.map_occupancyGauge line 335
  29. lemma OAI.CriticalStrip.Diagram.sourceGlue_gauge line 342
  30. theorem OAI.CriticalStrip.Diagram.polynomialNorthGluing_bottom_reflection line 362
  31. theorem OAI.CriticalStrip.Diagram.polynomialNorthGluing_row_reflection line 377
  32. lemma OAI.CriticalStrip.Diagram.permLaurent_one line 406
  33. lemma OAI.CriticalStrip.Diagram.permLaurent_mul line 414
  34. lemma OAI.CriticalStrip.Diagram.permLaurent_invariant_of_adjacent line 424
  35. lemma OAI.CriticalStrip.Diagram.polynomialNorthGluing_permute line 446
  36. lemma OAI.CriticalStrip.Diagram.laurent_eq_zero_of_many_roots line 452
  37. lemma OAI.CriticalStrip.Diagram.torusEvaluation_rowReflect line 479