OAI/Combinatorics/StripMass/ScalarDegree.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. theorem OAI.CriticalStrip.Diagram.cosine_difference_degree_self line 14
  2. theorem OAI.CriticalStrip.Diagram.cosine_difference_degree line 22
  3. theorem OAI.CriticalStrip.Diagram.sourceVandermonde_degree line 39
  4. theorem OAI.CriticalStrip.Diagram.scalarPolynomial_degree line 53
  5. def OAI.CriticalStrip.Diagram.firstScalarHom line 75
  6. lemma OAI.CriticalStrip.Diagram.firstScalarHom_degree line 79
  7. lemma OAI.CriticalStrip.Diagram.scalarPolynomial_first_degree line 102
  8. lemma OAI.CriticalStrip.Diagram.polynomial_top_numerator line 107
  9. lemma OAI.CriticalStrip.Diagram.polynomial_top_discriminant line 114
  10. def OAI.CriticalStrip.Diagram.infinityNumerator line 126
  11. def OAI.CriticalStrip.Diagram.infinityDenominator line 130
  12. lemma OAI.CriticalStrip.Diagram.augmentedNumerator_first_degree line 135
  13. lemma OAI.CriticalStrip.Diagram.augmentedDenominator_first_degree line 147
  14. lemma OAI.CriticalStrip.Diagram.firstScalarHom_C line 159
  15. lemma OAI.CriticalStrip.Diagram.firstScalarHom_X line 162
  16. lemma OAI.CriticalStrip.Diagram.scalarNumerator_first_map line 167
  17. lemma OAI.CriticalStrip.Diagram.scalarNumerator_first_top line 177
  18. def OAI.CriticalStrip.Diagram.infinityKernel line 197
  19. lemma OAI.CriticalStrip.Diagram.infinityNumerator_skew line 208
  20. lemma OAI.CriticalStrip.Diagram.infinityDenominator_symm line 217
  21. lemma OAI.CriticalStrip.Diagram.infinityDenominator_zero_real line 223
  22. lemma OAI.CriticalStrip.Diagram.infinityNumerator_zero_real line 231
  23. lemma OAI.CriticalStrip.Diagram.infinityDenominator_pos_real line 239
  24. lemma OAI.CriticalStrip.Diagram.infinityNumerator_pos_real line 253
  25. lemma OAI.CriticalStrip.Diagram.infinityDenominator_fake line 264
  26. lemma OAI.CriticalStrip.Diagram.infinityKernel_eq line 270
  27. lemma OAI.CriticalStrip.Diagram.infinityKernel_real line 299
  28. lemma OAI.CriticalStrip.Diagram.pfaffian_infinityKernel line 314
  29. def OAI.CriticalStrip.Diagram.infinityPairEmbed line 351
  30. lemma OAI.CriticalStrip.Diagram.infinityPairEmbed_injective line 354
  31. lemma OAI.CriticalStrip.Diagram.infinityDenominator_product line 363
  32. lemma OAI.CriticalStrip.Diagram.infinityDenominator_ne line 389
  33. lemma OAI.CriticalStrip.Diagram.scalarNumerator_first_top_eval line 415
  34. lemma OAI.CriticalStrip.Diagram.firstScalarHom_vandermonde line 427
  35. lemma OAI.CriticalStrip.Diagram.firstScalarHom_vandermonde_degree line 438
  36. lemma OAI.CriticalStrip.Diagram.firstScalarHom_vandermonde_top line 446
  37. theorem OAI.CriticalStrip.Diagram.scalarPolynomial_first_top line 460