OAI/Combinatorics/StripMass/NodalEmpty.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.scalarValue_snoc line 14
  2. lemma OAI.CriticalStrip.Diagram.rationalVacuum_empty line 19
  3. lemma OAI.CriticalStrip.Diagram.rationalNodalPolynomial_empty line 22
  4. lemma OAI.CriticalStrip.Diagram.rationalInterpolant_empty line 51
  5. lemma OAI.CriticalStrip.Diagram.stationary_eq_empty_mul_normalized line 72
  6. lemma OAI.CriticalStrip.Diagram.interpolant_eq_vacuum_of_residual line 86
  7. lemma OAI.CriticalStrip.Diagram.rationalInterpolationResidual_empty line 99
  8. lemma OAI.CriticalStrip.Diagram.Pairing.exists_earlier_occupied line 102
  9. structure OAI.CriticalStrip.Diagram.VacuumPolynomialData line 121
  10. def OAI.CriticalStrip.Diagram.VacuumPolynomialData.W line 129
  11. lemma OAI.CriticalStrip.Diagram.VacuumPolynomialData.degree line 130
  12. lemma OAI.CriticalStrip.Diagram.VacuumPolynomialData.box line 133
  13. lemma OAI.CriticalStrip.Diagram.VacuumPolynomialData.interpolant line 136
  14. lemma OAI.CriticalStrip.Diagram.spectralNormalization_zero line 142
  15. lemma OAI.CriticalStrip.Diagram.rationalVacuum_zero line 145
  16. lemma OAI.CriticalStrip.Diagram.Pairing.one_eq_empty line 148
  17. lemma OAI.CriticalStrip.Diagram.rationalVacuum_one line 153
  18. lemma OAI.CriticalStrip.Diagram.rationalNodalPolynomial_zero line 161
  19. def OAI.CriticalStrip.Diagram.vacuumData_zero line 165
  20. theorem OAI.CriticalStrip.Diagram.residual_saturation line 182
  21. lemma OAI.CriticalStrip.Diagram.LastMatrix.lastValue_map line 214
  22. lemma OAI.CriticalStrip.Diagram.pairEvaluation_lastLaurent line 235
  23. lemma OAI.CriticalStrip.Diagram.freePoint_delete line 242
  24. lemma OAI.CriticalStrip.Diagram.freePoint_merge line 248
  25. lemma OAI.CriticalStrip.Diagram.deleteEvaluation_lastLaurent line 253
  26. lemma OAI.CriticalStrip.Diagram.mergeEvaluation_lastLaurent line 260
  27. lemma OAI.CriticalStrip.Diagram.functionMatrix_map_hom line 267
  28. lemma OAI.CriticalStrip.Diagram.deletionMap_map line 273
  29. lemma OAI.CriticalStrip.Diagram.mergeMap_lift line 290
  30. lemma OAI.CriticalStrip.Diagram.liftSpectral_fcos line 304
  31. lemma OAI.CriticalStrip.Diagram.deletePairPolynomial_free line 309
  32. lemma OAI.CriticalStrip.Diagram.mergePairPolynomial_free line 321
  33. lemma OAI.CriticalStrip.Diagram.pairPoint_weights line 339
  34. lemma OAI.CriticalStrip.Diagram.rationalAt_pair_vacuum line 343
  35. lemma OAI.CriticalStrip.Diagram.deleteEvaluation_vacuum line 353
  36. lemma OAI.CriticalStrip.Diagram.mergeEvaluation_vacuum line 362
  37. lemma OAI.CriticalStrip.Diagram.deletePairCandidate_value line 371
  38. lemma OAI.CriticalStrip.Diagram.mergePairCandidate_value line 400
  39. theorem OAI.CriticalStrip.Diagram.residual_pair_delete line 432
  40. theorem OAI.CriticalStrip.Diagram.residual_pair_merge line 446
  41. lemma OAI.CriticalStrip.Diagram.residual_flat_universal line 465
  42. lemma OAI.CriticalStrip.Diagram.vacuumData_one_exists line 477
  43. lemma OAI.CriticalStrip.Diagram.vacuumData_step_exists line 491
  44. theorem OAI.CriticalStrip.Diagram.vacuumData_exists line 513
  45. def OAI.CriticalStrip.Diagram.vacuumData line 523
  46. theorem OAI.CriticalStrip.Diagram.vacuum_interpolation_stationary line 527