OAI/Combinatorics/StripMass/SplitGluing.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. lemma OAI.CriticalStrip.Diagram.functionMatrix_omit_glue_adjoint line 13
  2. lemma OAI.CriticalStrip.Diagram.position_padTop_root_ne line 22
  3. lemma OAI.CriticalStrip.Diagram.mergeMap_glue_adjoint line 36
  4. lemma OAI.CriticalStrip.Diagram.twoVacancyInsertion_glue_adjoint line 51
  5. lemma OAI.CriticalStrip.Diagram.deletionMap_glue_adjoint line 69
  6. theorem OAI.CriticalStrip.Diagram.sourceGlue_merge line 96
  7. theorem OAI.CriticalStrip.Diagram.sourceGlue_delete line 113
  8. lemma OAI.CriticalStrip.Diagram.sourceGlue_smul_right line 128
  9. lemma OAI.CriticalStrip.Diagram.sourceGlue_smul_left line 132
  10. lemma OAI.CriticalStrip.Diagram.sourceGlue_algMap line 136
  11. theorem OAI.CriticalStrip.Diagram.polynomialNorthGluing_merge line 144
  12. theorem OAI.CriticalStrip.Diagram.polynomialNorthGluing_delete line 164
  13. lemma OAI.CriticalStrip.Diagram.lastCoefficient_cons_padBottom line 187
  14. lemma OAI.CriticalStrip.Diagram.lastFactor_padBottom line 195
  15. lemma OAI.CriticalStrip.Diagram.firstZeroPolynomial_padBottom line 200
  16. lemma OAI.CriticalStrip.Diagram.rationalFirstZeroPolynomial_vacant line 216
  17. def OAI.CriticalStrip.Diagram.SourcePairing.padBottom line 224
  18. lemma OAI.CriticalStrip.Diagram.SourcePairing.padBottom_injective line 227
  19. lemma OAI.CriticalStrip.Diagram.SourcePairing.padBottom_range line 232
  20. def OAI.CriticalStrip.Diagram.vacantBottomSourceExtension line 245
  21. lemma OAI.CriticalStrip.Diagram.vacantBottomSourceExtension_padBottom line 249
  22. lemma OAI.CriticalStrip.Diagram.coefficient_X_add_source line 256
  23. theorem OAI.CriticalStrip.Diagram.polynomialNorthSource_firstFlat line 269
  24. theorem OAI.CriticalStrip.Diagram.polynomialNorthSource_firstThree line 290
  25. lemma OAI.CriticalStrip.Diagram.firstFlatEvaluation_reflect line 322
  26. lemma OAI.CriticalStrip.Diagram.firstThreeEvaluation_reflect line 334
  27. lemma OAI.CriticalStrip.Diagram.vacantBottomSourceExtension_map line 341
  28. lemma OAI.CriticalStrip.Diagram.sourceGlue_vacantBottom_right line 347
  29. lemma OAI.CriticalStrip.Diagram.sourceGlue_vacantBottom_left line 384
  30. theorem OAI.CriticalStrip.Diagram.polynomialNorthGluing_firstFlat line 392
  31. theorem OAI.CriticalStrip.Diagram.polynomialNorthGluing_firstThree line 422
  32. def OAI.CriticalStrip.Diagram.reflectExponentAt line 436
  33. lemma OAI.CriticalStrip.Diagram.reflectExponentAt_same line 439
  34. lemma OAI.CriticalStrip.Diagram.reflectExponentAt_other line 441
  35. lemma OAI.CriticalStrip.Diagram.reflectExponentAt_zero line 443
  36. lemma OAI.CriticalStrip.Diagram.reflectExponentAt_add line 445
  37. lemma OAI.CriticalStrip.Diagram.reflectExponentAt_neg line 449
  38. lemma OAI.CriticalStrip.Diagram.reflectExponentAt_involutive line 453
  39. def OAI.CriticalStrip.Diagram.rowReflectionMonomial line 458
  40. def OAI.CriticalStrip.Diagram.rowReflectLaurent line 468
  41. lemma OAI.CriticalStrip.Diagram.rowReflectLaurent_monomial line 471
  42. lemma OAI.CriticalStrip.Diagram.rowReflectLaurent_involutive line 480
  43. def OAI.CriticalStrip.Diagram.rowReflectSpectral line 490
  44. lemma OAI.CriticalStrip.Diagram.rowReflectSpectral_evalLaurent line 496
  45. lemma OAI.CriticalStrip.Diagram.rowReflectSpectral_involutive line 500
  46. lemma OAI.CriticalStrip.Diagram.rowReflectSpectral_const line 509
  47. lemma OAI.CriticalStrip.Diagram.rowReflectSpectral_variable line 517
  48. lemma OAI.CriticalStrip.Diagram.rowReflectSpectral_torusSin line 541
  49. lemma OAI.CriticalStrip.Diagram.rowReflectSpectral_torusCos line 544
  50. lemma OAI.CriticalStrip.Diagram.rowReflectSpectral_torusL line 547
  51. lemma OAI.CriticalStrip.Diagram.rowReflectSpectral_torusWeights line 549
  52. lemma OAI.CriticalStrip.Diagram.rowReflectSpectral_spectralA line 553
  53. lemma OAI.CriticalStrip.Diagram.rowReflectSpectral_normalization line 562
  54. lemma OAI.CriticalStrip.Diagram.reflectLaurent_rowReflect line 567
  55. lemma OAI.CriticalStrip.Diagram.reflectSpectral_rowReflect line 585
  56. lemma OAI.CriticalStrip.Diagram.rowReflectLaurent_perm line 596