OAI/Combinatorics/StripMass/ArchTrig.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. lemma OAI.CriticalStrip.Diagram.arch_flat_constants line 13
  2. lemma OAI.CriticalStrip.Diagram.fcos_arch_merge line 19
  3. lemma OAI.CriticalStrip.Diagram.fcos_arch_delete line 25
  4. lemma OAI.CriticalStrip.Diagram.pairEvaluation_rowCosine line 41
  5. lemma OAI.CriticalStrip.Diagram.mergeEvaluation_rowCosine line 45
  6. lemma OAI.CriticalStrip.Diagram.deleteEvaluation_rowCosine line 51
  7. lemma OAI.CriticalStrip.Diagram.nextScalar_flat_previous line 58
  8. theorem OAI.CriticalStrip.Diagram.archCandidate_firstFlat line 70
  9. lemma OAI.CriticalStrip.Diagram.nextScalar_merge_previous line 89
  10. theorem OAI.CriticalStrip.Diagram.archCandidate_merge line 103
  11. lemma OAI.CriticalStrip.Diagram.nextScalar_delete_previous line 122
  12. theorem OAI.CriticalStrip.Diagram.archCandidate_delete line 134
  13. def OAI.CriticalStrip.Diagram.twoPair line 156
  14. lemma OAI.CriticalStrip.Diagram.twoPair_adj line 158
  15. lemma OAI.CriticalStrip.Diagram.twoPair_occupied line 161
  16. def OAI.CriticalStrip.Diagram.oneSourcePair line 164
  17. lemma OAI.CriticalStrip.Diagram.SourcePairing.one_eq line 166
  18. instance OAI.CriticalStrip.Diagram.(instance at line 187) line 187
  19. lemma OAI.CriticalStrip.Diagram.oneSourcePair_glues line 190
  20. lemma OAI.CriticalStrip.Diagram.sourceGlue_one line 197
  21. lemma OAI.CriticalStrip.Diagram.sourceGlue_zero line 202
  22. lemma OAI.CriticalStrip.Diagram.archCandidate_zero line 207
  23. lemma OAI.CriticalStrip.Diagram.polynomialNorthGluing_zero line 210
  24. lemma OAI.CriticalStrip.Diagram.empty_insertCup_two line 212
  25. lemma OAI.CriticalStrip.Diagram.localR_deletion_twoPair line 217
  26. lemma OAI.CriticalStrip.Diagram.deletionMap_zero_twoPair line 228
  27. lemma OAI.CriticalStrip.Diagram.reducedNodalDatum_one line 239
  28. lemma OAI.CriticalStrip.Diagram.northNumerator_one line 253
  29. lemma OAI.CriticalStrip.Diagram.polynomialNorthSource_one line 270
  30. lemma OAI.CriticalStrip.Diagram.scalarArchNumerator_one line 277
  31. lemma OAI.CriticalStrip.Diagram.arch_one_constants line 294
  32. lemma OAI.CriticalStrip.Diagram.arch_one_field_constants line 314
  33. lemma OAI.CriticalStrip.Diagram.polynomialNorthGluing_one line 323
  34. theorem OAI.CriticalStrip.Diagram.polynomialNorthGluing_eq_archCandidate line 348
  35. lemma OAI.CriticalStrip.Diagram.scalarValue_allFlat_ne_zero line 370
  36. lemma OAI.CriticalStrip.Diagram.allFlat_rowCosine line 389
  37. theorem OAI.CriticalStrip.Diagram.spectralNormalization_ne_zero line 397
  38. lemma OAI.CriticalStrip.Diagram.scalarValue_spectral line 409
  39. def OAI.CriticalStrip.Diagram.rationalArchPolynomial line 414
  40. lemma OAI.CriticalStrip.Diagram.rationalArchPolynomial_coeff line 418
  41. theorem OAI.CriticalStrip.Diagram.rationalArchPolynomial_monic_degree line 425
  42. lemma OAI.CriticalStrip.Diagram.previousCoeff_rationalArchPolynomial line 439
  43. theorem OAI.CriticalStrip.Diagram.northSeparatorMoment_arch line 447