OAI/Combinatorics/StripMass/FirstFlatSpecialization.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. def OAI.CriticalStrip.Diagram.firstFlatPoint line 14
  2. lemma OAI.CriticalStrip.Diagram.firstFlatPoint_ne_zero line 16
  3. def OAI.CriticalStrip.Diagram.firstFlatEvaluation line 21
  4. lemma OAI.CriticalStrip.Diagram.rationalAt_firstFlat_variable line 24
  5. lemma OAI.CriticalStrip.Diagram.rationalAt_firstFlat_spectralA line 28
  6. lemma OAI.CriticalStrip.Diagram.rationalAt_firstFlat_deletionNode line 42
  7. lemma OAI.CriticalStrip.Diagram.rationalAt_firstFlat_deletionBeta line 51
  8. def OAI.CriticalStrip.Diagram.firstFlatSmallerWeights line 70
  9. lemma OAI.CriticalStrip.Diagram.firstFlatSmaller_regular line 73
  10. lemma OAI.CriticalStrip.Diagram.rationalAt_firstFlat_nodalWeights line 83
  11. lemma OAI.CriticalStrip.Diagram.rationalAt_firstFlat_normalizedVacuum line 126
  12. lemma OAI.CriticalStrip.Diagram.scalarPolynomial_eval_snoc_flat line 144
  13. lemma OAI.CriticalStrip.Diagram.scalarPolynomial_eval_spectral line 154
  14. def OAI.CriticalStrip.Diagram.firstFlatSmallerScalar line 161
  15. lemma OAI.CriticalStrip.Diagram.firstFlatSmallerScalar_eq line 165
  16. lemma OAI.CriticalStrip.Diagram.rationalAt_firstFlat_nodalScalar line 176
  17. lemma OAI.CriticalStrip.Diagram.rationalAt_firstFlat_nodalVacuum line 198
  18. def OAI.CriticalStrip.Diagram.lastEvaluation line 213
  19. lemma OAI.CriticalStrip.Diagram.lastEvaluation_lift line 216
  20. lemma OAI.CriticalStrip.Diagram.rationalAt_last_lift line 227
  21. lemma OAI.CriticalStrip.Diagram.rationalAt_last_variable line 240
  22. lemma OAI.CriticalStrip.Diagram.rationalAt_last_spectralA line 245
  23. lemma OAI.CriticalStrip.Diagram.rationalAt_last_interpolant line 253
  24. lemma OAI.CriticalStrip.Diagram.rationalAt_last_weights line 264
  25. theorem OAI.CriticalStrip.Diagram.sum_selectedPairs line 286
  26. theorem OAI.CriticalStrip.Diagram.clearedPfaffianTerm_degree line 299
  27. theorem OAI.CriticalStrip.Diagram.clearedPfaffian_degree line 316
  28. theorem OAI.CriticalStrip.Diagram.numerator_degree_bound line 334
  29. theorem OAI.CriticalStrip.Diagram.discriminant_degree_bound line 346
  30. def OAI.CriticalStrip.Diagram.scalarEdgeDegree line 368
  31. theorem OAI.CriticalStrip.Diagram.scalarEdgeDegree_symm line 371
  32. theorem OAI.CriticalStrip.Diagram.augmentedNumerator_degree line 378
  33. theorem OAI.CriticalStrip.Diagram.augmentedDenominator_degree line 390
  34. def OAI.CriticalStrip.Diagram.incidentPair line 408
  35. theorem OAI.CriticalStrip.Diagram.incidentPair_injective line 411
  36. theorem OAI.CriticalStrip.Diagram.incidentPair_has_k line 417
  37. theorem OAI.CriticalStrip.Diagram.incidentPair_range line 422
  38. theorem OAI.CriticalStrip.Diagram.sum_incident_degree line 434
  39. theorem OAI.CriticalStrip.Diagram.sum_scalarEdgeDegree line 449
  40. theorem OAI.CriticalStrip.Diagram.scalarNumerator_degree line 469
  41. theorem OAI.CriticalStrip.Diagram.coeff_prod_budget line 483
  42. theorem OAI.CriticalStrip.Diagram.clearedPfaffianTerm_top line 499
  43. theorem OAI.CriticalStrip.Diagram.clearedPfaffian_top line 519