OAI/Combinatorics/StripMass/NodalRegularity.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. def OAI.CriticalStrip.Diagram.inverseRowDenominator line 14
  2. def OAI.CriticalStrip.Diagram.inverseRowNumerator line 18
  3. theorem OAI.CriticalStrip.Diagram.inverseRowDenominator_flat line 33
  4. theorem OAI.CriticalStrip.Diagram.inverseRowDenominator_flat_ne_zero line 38
  5. theorem OAI.CriticalStrip.Diagram.inverseRowDenominator_map line 43
  6. theorem OAI.CriticalStrip.Diagram.inverseRowDenominator_map_ne_zero line 48
  7. theorem OAI.CriticalStrip.Diagram.inverseRowNumerator_flat line 54
  8. theorem OAI.CriticalStrip.Diagram.inverseRowNumerator_map line 70
  9. theorem OAI.CriticalStrip.Diagram.nodalWeights_last line 92
  10. theorem OAI.CriticalStrip.Diagram.nodal_regular line 98
  11. theorem OAI.CriticalStrip.Diagram.nodalVacuum_stationary line 125
  12. lemma OAI.CriticalStrip.Diagram.spectral_regular_reindex line 141
  13. lemma OAI.CriticalStrip.Diagram.map_monomialL_sub_variable line 156
  14. lemma OAI.CriticalStrip.Diagram.torusL_ratio_ne_zero line 165
  15. theorem OAI.CriticalStrip.Diagram.spectral_vacuum_exchange line 192
  16. def OAI.CriticalStrip.Diagram.insertedNodeWeights line 220
  17. lemma OAI.CriticalStrip.Diagram.insertedNodeWeights_last line 224
  18. lemma OAI.CriticalStrip.Diagram.insertedNode_regular line 234
  19. lemma OAI.CriticalStrip.Diagram.insertedNode_deletion line 262
  20. lemma OAI.CriticalStrip.Diagram.Fin.insertNth_swap_adjacent line 302
  21. lemma OAI.CriticalStrip.Diagram.torusL_deletion_ratio_ne_zero line 313
  22. theorem OAI.CriticalStrip.Diagram.insertedNode_move line 336
  23. def OAI.CriticalStrip.Diagram.movingBoxes line 390
  24. lemma OAI.CriticalStrip.Diagram.movingBoxes_initial line 397
  25. lemma OAI.CriticalStrip.Diagram.insertedNode_moved line 403
  26. theorem OAI.CriticalStrip.Diagram.nodalVacuum_movingBoxes line 420
  27. def OAI.CriticalStrip.Diagram.topPerm line 436
  28. lemma OAI.CriticalStrip.Diagram.topPerm_cast line 439
  29. lemma OAI.CriticalStrip.Diagram.topPerm_last line 443
  30. lemma OAI.CriticalStrip.Diagram.permSpectral_deletionNode line 449
  31. lemma OAI.CriticalStrip.Diagram.permSpectral_deletionBeta line 452
  32. lemma OAI.CriticalStrip.Diagram.permSpectral_nodalWeights line 455
  33. lemma OAI.CriticalStrip.Diagram.scalarPolynomial_eval_reindex line 463
  34. lemma OAI.CriticalStrip.Diagram.permSpectral_nodalScalar line 469
  35. lemma OAI.CriticalStrip.Diagram.nodal_regular_reindex line 484
  36. lemma OAI.CriticalStrip.Diagram.permSpectral_nodalVacuum line 489
  37. def OAI.CriticalStrip.Diagram.deletionPerm line 508
  38. lemma OAI.CriticalStrip.Diagram.deletionPerm_tuple line 543
  39. lemma OAI.CriticalStrip.Diagram.scalarPolynomial_snoc_delete_reindex line 553