OAI/Combinatorics/StripMass/VacuumDegree.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. lemma OAI.CriticalStrip.Diagram.polynomial_eval₂_fin line 14
  2. def OAI.CriticalStrip.Diagram.polynomialVacuumVector line 27
  3. lemma OAI.CriticalStrip.Diagram.polynomialVacuumVector_eval line 31
  4. lemma OAI.CriticalStrip.Diagram.vacuumData_leading line 37
  5. theorem OAI.CriticalStrip.Diagram.vacuum_degree line 45
  6. theorem OAI.CriticalStrip.Diagram.vacuum_degree_remaining line 76
  7. theorem OAI.CriticalStrip.Diagram.vacuum_interpolation_stationary_remaining line 79
  8. abbrev OAI.CriticalStrip.Diagram.SourcePairing line 92
  9. lemma OAI.CriticalStrip.Diagram.SourcePairing.occupied line 94
  10. lemma OAI.CriticalStrip.Diagram.SourcePairing.ne_empty line 97
  11. def OAI.CriticalStrip.Diagram.sourceTopEquiv line 101
  12. def OAI.CriticalStrip.Diagram.sourceTopSplit line 107
  13. lemma OAI.CriticalStrip.Diagram.sourceTopSplit_inl line 110
  14. lemma OAI.CriticalStrip.Diagram.sourceTopSplit_inr_val line 113
  15. def OAI.CriticalStrip.Diagram.horizontalWeights line 118
  16. def OAI.CriticalStrip.Diagram.sourceTransfer line 120
  17. def OAI.CriticalStrip.Diagram.northSource line 124
  18. lemma OAI.CriticalStrip.Diagram.horizontal_column_blocks line 128
  19. lemma OAI.CriticalStrip.Diagram.det_horizontal_column line 153
  20. lemma OAI.CriticalStrip.Diagram.sourceTransfer_regular_of_horizontal line 165
  21. lemma OAI.CriticalStrip.Diagram.horizontal_spectral_regular line 172
  22. lemma OAI.CriticalStrip.Diagram.spectral_source_regular line 207
  23. lemma OAI.CriticalStrip.Diagram.rationalResidualCoefficient_zero line 211
  24. lemma OAI.CriticalStrip.Diagram.rationalResidualPolynomial_zero line 243
  25. def OAI.CriticalStrip.Diagram.vacantTopEquiv line 248
  26. def OAI.CriticalStrip.Diagram.pairingTopSplit line 255
  27. lemma OAI.CriticalStrip.Diagram.pairingTopSplit_inl line 260
  28. lemma OAI.CriticalStrip.Diagram.pairingTopSplit_inr line 263
  29. lemma OAI.CriticalStrip.Diagram.lastTransform_source_leading line 268
  30. def OAI.CriticalStrip.Diagram.northNumerator line 290
  31. lemma OAI.CriticalStrip.Diagram.northNumerator_equation line 293
  32. def OAI.CriticalStrip.Diagram.integratedNorthSource line 324
  33. lemma OAI.CriticalStrip.Diagram.northNumerator_eq_integrated line 329
  34. def OAI.CriticalStrip.Diagram.polynomialNorthSource line 345
  35. lemma OAI.CriticalStrip.Diagram.polynomialNorthSource_eval line 348
  36. theorem OAI.CriticalStrip.Diagram.polynomialNorthSource_box line 371
  37. def OAI.CriticalStrip.Diagram.Graph.DrainsAt line 387
  38. lemma OAI.CriticalStrip.Diagram.Graph.DrainsAt.mono_root line 390
  39. lemma OAI.CriticalStrip.Diagram.Graph.DrainsAt.map line 394
  40. def OAI.CriticalStrip.Diagram.Graph.boundaryClosure line 405
  41. lemma OAI.CriticalStrip.Diagram.Graph.closure_lift line 409