OAI/Combinatorics/StripMass/PhysicalPorts.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. def OAI.CriticalStrip.HoneycombBranch.bandVertices line 14
  2. def OAI.CriticalStrip.HoneycombBranch.stripPort line 16
  3. lemma OAI.CriticalStrip.HoneycombBranch.stripPort_injective line 20
  4. lemma OAI.CriticalStrip.HoneycombBranch.stripPort_inside line 23
  5. lemma OAI.CriticalStrip.HoneycombBranch.stripPort_outside line 26
  6. lemma OAI.CriticalStrip.HoneycombBranch.stripPort_complete line 29
  7. def OAI.CriticalStrip.HoneycombBranch.stripBoundaryPorts line 45
  8. abbrev OAI.CriticalStrip.HoneycombBranch.StepEndpoint line 52
  9. def OAI.CriticalStrip.HoneycombBranch.stepPort line 54
  10. lemma OAI.CriticalStrip.HoneycombBranch.stepPort_injective line 59
  11. lemma OAI.CriticalStrip.HoneycombBranch.stepPort_inside line 65
  12. lemma OAI.CriticalStrip.HoneycombBranch.stepPort_outside line 73
  13. lemma OAI.CriticalStrip.HoneycombBranch.stepPort_complete line 81
  14. def OAI.CriticalStrip.HoneycombBranch.stepBoundaryPorts line 106
  15. lemma OAI.CriticalStrip.HoneycombBranch.retract_bottom line 113
  16. lemma OAI.CriticalStrip.HoneycombBranch.retract_top line 114
  17. lemma OAI.CriticalStrip.HoneycombBranch.retract_side line 118
  18. lemma OAI.CriticalStrip.HoneycombBranch.boundaryPathWeight_strip_bottom line 121
  19. def OAI.CriticalStrip.HoneycombBranch.betweenBridgeWeight line 134
  20. lemma OAI.CriticalStrip.HoneycombBranch.betweenBridgeWeight_nonneg line 137
  21. lemma OAI.CriticalStrip.HoneycombBranch.betweenBridgeWeight_translate line 142
  22. lemma OAI.CriticalStrip.HoneycombBranch.betweenBridgeWeight_summable line 148
  23. lemma OAI.CriticalStrip.HoneycombBranch.betweenArchWeight_summable line 164
  24. lemma OAI.CriticalStrip.HoneycombBranch.boundaryPathWeight_strip_top line 173
  25. lemma OAI.CriticalStrip.HoneycombBranch.boundaryPathWeight_step_bottom line 187
  26. lemma OAI.CriticalStrip.HoneycombBranch.boundaryPathWeight_step_side line 198
  27. lemma OAI.CriticalStrip.HoneycombBranch.summable_sumProd line 214
  28. lemma OAI.CriticalStrip.HoneycombBranch.tsum_sumProd line 221
  29. lemma OAI.CriticalStrip.HoneycombBranch.phase_re line 229
  30. lemma OAI.CriticalStrip.HoneycombBranch.phase_im line 233
  31. lemma OAI.CriticalStrip.HoneycombBranch.boundary_complex_summable line 239
  32. lemma OAI.CriticalStrip.HoneycombBranch.boundary_real_summable line 245
  33. lemma OAI.CriticalStrip.HoneycombBranch.boundary_imaginary_summable line 250
  34. theorem OAI.CriticalStrip.HoneycombBranch.boundary_real_flux line 256
  35. theorem OAI.CriticalStrip.HoneycombBranch.boundary_imaginary_flux line 264
  36. lemma OAI.CriticalStrip.HoneycombBranch.stripBoundary_summable line 272
  37. def OAI.CriticalStrip.HoneycombBranch.stripTurn line 278
  38. lemma OAI.CriticalStrip.HoneycombBranch.strip_turn line 282
  39. lemma OAI.CriticalStrip.HoneycombBranch.stripTurn_cos_bottom line 291
  40. lemma OAI.CriticalStrip.HoneycombBranch.stripTurn_cos_top line 295
  41. theorem OAI.CriticalStrip.HoneycombBranch.physical_strip_flux line 300
  42. def OAI.CriticalStrip.HoneycombBranch.extendStepTop line 333
  43. lemma OAI.CriticalStrip.HoneycombBranch.extendStepTop_injective line 336
  44. lemma OAI.CriticalStrip.HoneycombBranch.extendStepTop_spec line 343
  45. lemma OAI.CriticalStrip.HoneycombBranch.extendStepTop_weight line 372
  46. lemma OAI.CriticalStrip.HoneycombBranch.stepBoundary_top_summable line 390
  47. lemma OAI.CriticalStrip.HoneycombBranch.stepArchWeight_summable line 409
  48. theorem OAI.CriticalStrip.HoneycombBranch.stepBoundary_summable line 416
  49. lemma OAI.CriticalStrip.HoneycombBranch.summable_sumProd_left line 435
  50. lemma OAI.CriticalStrip.HoneycombBranch.summable_sumProd_right line 442
  51. def OAI.CriticalStrip.HoneycombBranch.stepTurn line 449
  52. lemma OAI.CriticalStrip.HoneycombBranch.step_turn line 454
  53. lemma OAI.CriticalStrip.HoneycombBranch.stepTurn_sine_right line 464
  54. lemma OAI.CriticalStrip.HoneycombBranch.stepTurn_sine_left line 469
  55. lemma OAI.CriticalStrip.HoneycombBranch.stepArchKernel_self line 474
  56. lemma OAI.CriticalStrip.HoneycombBranch.step_bottom_imaginary_tsum line 477
  57. theorem OAI.CriticalStrip.HoneycombBranch.physical_stepped_flux line 509
  58. theorem OAI.CriticalStrip.critical_strip_mass line 552

    Distinct definitions of this name: ComparatorChallenges/CriticalStripMass.lean:76 (same statement text; different proof or body). Qualify references as OAI.CriticalStrip.critical_strip_mass@path.