OAI/Combinatorics/StripMass/ProjectionInjection.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. lemma OAI.CriticalStrip.Diagram.twoVacancyInsertion_transpose_deletion line 16
  2. lemma OAI.CriticalStrip.Diagram.deletionMap_injective line 51
  3. def OAI.CriticalStrip.Diagram.extendSource line 59
  4. lemma OAI.CriticalStrip.Diagram.extendSource_apply line 62
  5. lemma OAI.CriticalStrip.Diagram.LastMatrix.mulVec_extendSource line 66
  6. lemma OAI.CriticalStrip.Diagram.LastMatrix.source_injective line 83
  7. lemma OAI.CriticalStrip.Diagram.sourceBlock_merge_injective line 93
  8. lemma OAI.CriticalStrip.Diagram.sourceBlock_deletion_injective line 97
  9. lemma OAI.CriticalStrip.Diagram.twoVacancyInsertion_last line 101
  10. lemma OAI.CriticalStrip.Diagram.mergeProjection_last line 107
  11. lemma OAI.CriticalStrip.Diagram.deletionProjection_last line 113
  12. lemma OAI.CriticalStrip.Diagram.sourceBlock_merge_factor line 118
  13. lemma OAI.CriticalStrip.Diagram.sourceBlock_deletion_factor line 124
  14. def OAI.CriticalStrip.Diagram.twistedReflectionMonomial line 135
  15. def OAI.CriticalStrip.Diagram.twistedReflectLaurent line 144
  16. lemma OAI.CriticalStrip.Diagram.twistedReflectLaurent_monomial line 147
  17. lemma OAI.CriticalStrip.Diagram.twistedReflectLaurent_involutive line 156
  18. def OAI.CriticalStrip.Diagram.twistedReflectSpectral line 166
  19. lemma OAI.CriticalStrip.Diagram.twistedReflectSpectral_evalLaurent line 172
  20. lemma OAI.CriticalStrip.Diagram.twistedReflectSpectral_const line 176
  21. lemma OAI.CriticalStrip.Diagram.twistedReflectSpectral_variable line 184
  22. lemma OAI.CriticalStrip.Diagram.torusEvaluation_twistedReflect line 193
  23. lemma OAI.CriticalStrip.Diagram.sum_zpow_eq_prod line 210
  24. lemma OAI.CriticalStrip.Diagram.reflectLaurent_eq_twisted line 217
  25. lemma OAI.CriticalStrip.Diagram.torusEvaluation_reflect line 223
  26. def OAI.CriticalStrip.Diagram.pairReflection line 233
  27. lemma OAI.CriticalStrip.Diagram.pairReflection_const line 236
  28. lemma OAI.CriticalStrip.Diagram.pairReflection_variable_zero line 239
  29. lemma OAI.CriticalStrip.Diagram.pairReflection_variable_succ line 243
  30. lemma OAI.CriticalStrip.Diagram.pairReflection_torusCos line 247
  31. lemma OAI.CriticalStrip.Diagram.pairReflection_pairPoint line 256
  32. lemma OAI.CriticalStrip.Diagram.pairEvaluation_swap_reflect line 284
  33. lemma OAI.CriticalStrip.Diagram.pairReflection_mergePoint line 294
  34. lemma OAI.CriticalStrip.Diagram.pairReflection_mergeEvaluation line 303
  35. lemma OAI.CriticalStrip.Diagram.pairReflection_deleteEvaluation line 312
  36. lemma OAI.CriticalStrip.Diagram.twistedReflectSpectral_torusCos line 323
  37. lemma OAI.CriticalStrip.Diagram.twistedReflectSpectral_fcos line 327
  38. lemma OAI.CriticalStrip.Diagram.pairReflection_fcos_zero line 349
  39. lemma OAI.CriticalStrip.Diagram.pairReflection_fcos_succ line 353
  40. lemma OAI.CriticalStrip.Diagram.pairReflection_mergeScalar line 357
  41. lemma OAI.CriticalStrip.Diagram.pairReflection_deleteScalar line 365
  42. lemma OAI.CriticalStrip.Diagram.constF_C_ne_zero line 384
  43. lemma OAI.CriticalStrip.Diagram.torusL_split_nonzero line 387
  44. lemma OAI.CriticalStrip.Diagram.polynomialNorthSource_reflected_pair line 396
  45. lemma OAI.CriticalStrip.Diagram.pairReflection_mergeMap line 436
  46. theorem OAI.CriticalStrip.Diagram.polynomialNorthSource_reflected_merge line 454
  47. theorem OAI.CriticalStrip.Diagram.polynomialNorthSource_reflected_delete line 480