OAI/Combinatorics/StripMass/ResidualParityCoefficients.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. lemma OAI.CriticalStrip.Diagram.signLaurent_coeff line 14
  2. lemma OAI.CriticalStrip.Diagram.signLaurent_odd_even_coeff_zero line 27
  3. lemma OAI.CriticalStrip.Diagram.laurentResidual_odd line 34
  4. lemma OAI.CriticalStrip.Diagram.laurentResidual_peel_top_zero line 47
  5. lemma OAI.CriticalStrip.Diagram.phase_primitive line 65
  6. def OAI.CriticalStrip.Diagram.residualRootPhase line 75
  7. def OAI.CriticalStrip.Diagram.residualRootExponent line 85
  8. def OAI.CriticalStrip.Diagram.residualRoot line 88
  9. lemma OAI.CriticalStrip.Diagram.residualRootPhase_lt line 91
  10. lemma OAI.CriticalStrip.Diagram.residualRootPhase_injective line 95
  11. lemma OAI.CriticalStrip.Diagram.residualRootExponent_support line 107
  12. lemma OAI.CriticalStrip.Diagram.residualRootExponent_index line 112
  13. lemma OAI.CriticalStrip.Diagram.residualRoot_ne_zero line 124
  14. lemma OAI.CriticalStrip.Diagram.residualRoot_injective line 131
  15. def OAI.CriticalStrip.Diagram.residualRootSet line 144
  16. lemma OAI.CriticalStrip.Diagram.residualRootSet_card line 147
  17. theorem OAI.CriticalStrip.Diagram.residual_zero_of_root_grid line 154
  18. lemma OAI.CriticalStrip.Diagram.torusSin_monomial_ne_zero line 190
  19. lemma OAI.CriticalStrip.Diagram.constF_mul_monomial line 206
  20. lemma OAI.CriticalStrip.Diagram.torusL_monomial_ne_zero line 214
  21. lemma OAI.CriticalStrip.Diagram.monomial_ratio_regular line 224
  22. lemma OAI.CriticalStrip.Diagram.variableExponent_injective line 233
  23. lemma OAI.CriticalStrip.Diagram.flat_update_regular line 239
  24. lemma OAI.CriticalStrip.Diagram.pair_update_regular line 249
  25. lemma OAI.CriticalStrip.Diagram.torusEvaluation_signLaurent line 280
  26. lemma OAI.CriticalStrip.Diagram.torusEvaluation_neg_zero line 297
  27. lemma OAI.CriticalStrip.Diagram.lastEvaluation_residual_zero line 310
  28. lemma OAI.CriticalStrip.Diagram.residual_last_delete_universal line 353
  29. lemma OAI.CriticalStrip.Diagram.residual_last_inverse_universal line 369
  30. def OAI.CriticalStrip.Diagram.positiveResidualRoot line 397
  31. lemma OAI.CriticalStrip.Diagram.phase_more_powers line 403
  32. lemma OAI.CriticalStrip.Diagram.residualRoot_values line 425
  33. lemma OAI.CriticalStrip.Diagram.positiveResidualRoot_ne_zero line 446
  34. lemma OAI.CriticalStrip.Diagram.positiveRoot_negative_zero line 452
  35. lemma OAI.CriticalStrip.Diagram.residualRoot_signed line 466
  36. lemma OAI.CriticalStrip.Diagram.residual_root_grid_of_positive line 476
  37. lemma OAI.CriticalStrip.Diagram.PairExchangeRegular.symm line 497
  38. theorem OAI.CriticalStrip.Diagram.residual_positive_roots line 504