OAI/Combinatorics/StripMass/NodalScalarDeletion.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. lemma OAI.CriticalStrip.Diagram.spectralA_injective line 15
  2. lemma OAI.CriticalStrip.Diagram.spectralA_ne_beta line 21
  3. def OAI.CriticalStrip.Diagram.deletionScalarTuple line 27
  4. lemma OAI.CriticalStrip.Diagram.deletionScalarTuple_injective line 30
  5. lemma OAI.CriticalStrip.Diagram.spectralA_discriminant_ne line 45
  6. lemma OAI.CriticalStrip.Diagram.beta_spectralA_discriminant_ne line 50
  7. lemma OAI.CriticalStrip.Diagram.deletionScalarTuple_discriminant line 55
  8. theorem OAI.CriticalStrip.Diagram.nodalScalar_deletion line 93
  9. def OAI.CriticalStrip.Diagram.deletionDataFactor line 111
  10. lemma OAI.CriticalStrip.Diagram.nodalScalar_factor_smaller line 116
  11. lemma OAI.CriticalStrip.Diagram.insertSpectral_rationalVacuum line 125
  12. theorem OAI.CriticalStrip.Diagram.nodalVacuum_interpolation_data line 134
  13. def OAI.CriticalStrip.Diagram.rawLocal line 153
  14. lemma OAI.CriticalStrip.Diagram.rawLocal_weights line 157
  15. lemma OAI.CriticalStrip.Diagram.rawLocal_smul line 160
  16. def OAI.CriticalStrip.Diagram.torusNumerator line 165
  17. lemma OAI.CriticalStrip.Diagram.torusNumerator_eq line 173
  18. theorem OAI.CriticalStrip.Diagram.movingBox_cleared line 180
  19. def OAI.CriticalStrip.Diagram.matrixPrefix line 205
  20. lemma OAI.CriticalStrip.Diagram.matrixPrefix_smul_partial line 209
  21. lemma OAI.CriticalStrip.Diagram.matrixPrefix_smul line 223
  22. lemma OAI.CriticalStrip.Diagram.matrixPrefix_map line 227
  23. lemma OAI.CriticalStrip.Diagram.rho_eq_two_c_d line 245
  24. theorem OAI.CriticalStrip.Diagram.deletion_occupied_sine_cancellation line 261
  25. def OAI.CriticalStrip.Diagram.movingStep line 300
  26. lemma OAI.CriticalStrip.Diagram.movingBoxes_prefix line 304
  27. def OAI.CriticalStrip.Diagram.reflectionFactor line 318
  28. def OAI.CriticalStrip.Diagram.scalarPairFactor line 321
  29. def OAI.CriticalStrip.Diagram.reducedMovingStep line 327
  30. lemma OAI.CriticalStrip.Diagram.reducedMovingStep_eq line 335
  31. lemma OAI.CriticalStrip.Diagram.reducedMoving_product line 349
  32. lemma OAI.CriticalStrip.Diagram.scalarPairFactor_product line 357
  33. theorem OAI.CriticalStrip.Diagram.nodalVacuum_reduced_data line 366
  34. theorem OAI.CriticalStrip.Diagram.rationalNodalPolynomial_at_node line 386
  35. theorem OAI.CriticalStrip.Diagram.rationalNodalPolynomial_degree line 399
  36. theorem OAI.CriticalStrip.Diagram.rationalNodalPolynomial_leading line 417
  37. lemma OAI.CriticalStrip.Diagram.deletionBeta_eq line 439
  38. lemma OAI.CriticalStrip.Diagram.deletionBeta_difference line 445
  39. def OAI.CriticalStrip.Diagram.ordinaryFactor line 462
  40. lemma OAI.CriticalStrip.Diagram.deletionBeta_product line 465
  41. lemma OAI.CriticalStrip.Diagram.reflectionOrdinary_product_ne_zero line 478
  42. def OAI.CriticalStrip.Diagram.reducedNodalHead line 486
  43. def OAI.CriticalStrip.Diagram.reducedNodalDatum line 491
  44. lemma OAI.CriticalStrip.Diagram.reducedNodalDatum_eq line 497
  45. lemma OAI.CriticalStrip.Diagram.nodalWeight_reduced line 510
  46. theorem OAI.CriticalStrip.Diagram.nodal_interpolate_reduced line 520