OAI/Combinatorics/StripMass/ScalarFlat.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. theorem OAI.CriticalStrip.Diagram.plainKernel_cons_flat line 16
  2. theorem OAI.CriticalStrip.Diagram.pfaffian_augmented_cons_flat line 43
  3. theorem OAI.CriticalStrip.Diagram.scalarNormalization_cons_flat line 67
  4. lemma OAI.CriticalStrip.Diagram.cosineVar_ne_const line 103
  5. lemma OAI.CriticalStrip.Diagram.cosineVar_injective line 110
  6. lemma OAI.CriticalStrip.Diagram.flat_discriminant_map line 113
  7. theorem OAI.CriticalStrip.Diagram.scalarPolynomial_cons_flat_identity line 124
  8. theorem OAI.CriticalStrip.Diagram.scalarPolynomial_eval_cons_flat line 195
  9. lemma OAI.CriticalStrip.Diagram.cos_five_lambda_eq line 222
  10. lemma OAI.CriticalStrip.Diagram.c_add_rho_eq_C line 226
  11. lemma OAI.CriticalStrip.Diagram.discriminant_flat_complex line 236
  12. lemma OAI.CriticalStrip.Diagram.flat_scalar_linear line 243
  13. lemma OAI.CriticalStrip.Diagram.flat_scalar_constant line 249
  14. lemma OAI.CriticalStrip.Diagram.source_scalarPolynomial_flat line 252
  15. lemma OAI.CriticalStrip.Diagram.torusSin_phase_pow line 261
  16. lemma OAI.CriticalStrip.Diagram.torusSin_one line 266
  17. lemma OAI.CriticalStrip.Diagram.sin_two_lambda_eq_d line 269
  18. lemma OAI.CriticalStrip.Diagram.sin_five_lambda_eq line 273
  19. lemma OAI.CriticalStrip.Diagram.torusL_one line 276
  20. lemma OAI.CriticalStrip.Diagram.torusL_phase_three line 281
  21. lemma OAI.CriticalStrip.Diagram.sin_three_lambda_pos line 289
  22. lemma OAI.CriticalStrip.Diagram.torusL_one_ne_zero line 296
  23. lemma OAI.CriticalStrip.Diagram.torusWeights_one line 303
  24. lemma OAI.CriticalStrip.Diagram.torusWeights_phase_three line 314
  25. def OAI.CriticalStrip.Diagram.vacantBottomExtension line 336
  26. theorem OAI.CriticalStrip.Diagram.vacantBottomExtension_padBottom line 340
  27. theorem OAI.CriticalStrip.Diagram.Pairing.padBottom_injective line 345
  28. theorem OAI.CriticalStrip.Diagram.Pairing.padBottom_padTop line 351
  29. theorem OAI.CriticalStrip.Diagram.rawColumn_padBottom line 358
  30. def OAI.CriticalStrip.Diagram.firstZeroRaw line 381
  31. theorem OAI.CriticalStrip.Diagram.mulVec_vacantBottomExtension line 386
  32. theorem OAI.CriticalStrip.Diagram.firstZeroRaw_vacant line 402
  33. theorem OAI.CriticalStrip.Diagram.deletion_column_mulVec line 409
  34. theorem OAI.CriticalStrip.Diagram.normalizedVacuum_firstZero line 433
  35. theorem OAI.CriticalStrip.Diagram.lastValue_vacantBottomExtension line 455
  36. theorem OAI.CriticalStrip.Diagram.LastDegree.vacantBottomExtension line 468
  37. theorem OAI.CriticalStrip.Diagram.vacantBottomExtension_leading line 481
  38. def OAI.CriticalStrip.Diagram.firstZeroPolynomial line 494
  39. theorem OAI.CriticalStrip.Diagram.firstZeroPolynomial_degree line 500
  40. theorem OAI.CriticalStrip.Diagram.firstZeroPolynomial_leading line 506
  41. theorem OAI.CriticalStrip.Diagram.map_deletion_tile line 515
  42. theorem OAI.CriticalStrip.Diagram.firstZeroPolynomial_evaluation line 522
  43. theorem OAI.CriticalStrip.Diagram.firstZeroRaw_rowScale line 552
  44. theorem OAI.CriticalStrip.Diagram.firstZeroPolynomial_spectral line 568