OAI/Combinatorics/StripMass/ScalarDeleteContinuation.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. abbrev OAI.CriticalStrip.Diagram.PolynomialField line 16
  2. def OAI.CriticalStrip.Diagram.genericConst line 17
  3. def OAI.CriticalStrip.Diagram.genericVar line 19
  4. lemma OAI.CriticalStrip.Diagram.genericVar_ne_const line 22
  5. lemma OAI.CriticalStrip.Diagram.genericVar_inj line 28
  6. lemma OAI.CriticalStrip.Diagram.discriminant_genericVar_ne line 31
  7. lemma OAI.CriticalStrip.Diagram.discriminant_const_genericVar_ne line 43
  8. lemma OAI.CriticalStrip.Diagram.generic_twoCons_inj line 64
  9. lemma OAI.CriticalStrip.Diagram.generic_twoCons_discriminant line 93
  10. theorem OAI.CriticalStrip.Diagram.scalarPolynomial_delete_continuation line 127
  11. lemma OAI.CriticalStrip.Diagram.map_firstScalarHom line 188
  12. theorem OAI.CriticalStrip.Diagram.scalarPolynomial_first_top_continuation line 203
  13. def OAI.CriticalStrip.Diagram.scalarValue line 234
  14. lemma OAI.CriticalStrip.Diagram.scalarValue_permute line 237
  15. lemma OAI.CriticalStrip.Diagram.scalarValue_extract line 244
  16. lemma OAI.CriticalStrip.Diagram.scalarValue_swap_head line 253
  17. lemma OAI.CriticalStrip.Diagram.eval_firstScalarHom line 267
  18. lemma OAI.CriticalStrip.Diagram.scalarValue_zero line 277
  19. lemma OAI.CriticalStrip.Diagram.scalarValue_one line 285
  20. lemma OAI.CriticalStrip.Diagram.scalarValue_two line 303
  21. lemma OAI.CriticalStrip.Diagram.scalarValue_cons_extract line 339
  22. lemma OAI.CriticalStrip.Diagram.scalarValue_one_middle_extract line 351
  23. lemma OAI.CriticalStrip.Diagram.scalarValue_two_middle_extract line 362
  24. lemma OAI.CriticalStrip.Diagram.scalarValue_delete line 375
  25. lemma OAI.CriticalStrip.Diagram.scalarValue_flat line 383
  26. def OAI.CriticalStrip.Diagram.scalarMergeDiff line 394
  27. lemma OAI.CriticalStrip.Diagram.scalarMergeDiff_eval line 401
  28. lemma OAI.CriticalStrip.Diagram.scalarMergeDiff_degree line 410
  29. lemma OAI.CriticalStrip.Diagram.scalarMergeDiff_top line 423
  30. lemma OAI.CriticalStrip.Diagram.scalarMergeDiff_degree_reduced line 436