OAI/Combinatorics/StripMass/NodalExchange.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. lemma OAI.CriticalStrip.Diagram.topPerm_swap line 14
  2. lemma OAI.CriticalStrip.Diagram.rationalVacuum_exchange line 24
  3. lemma OAI.CriticalStrip.Diagram.nodalVacuum_exchange line 44
  4. lemma OAI.CriticalStrip.Diagram.localR_padTop_zero_last line 107
  5. lemma OAI.CriticalStrip.Diagram.lastPolynomial_unique line 115
  6. def OAI.CriticalStrip.Diagram.nodalExchangePolynomial line 142
  7. lemma OAI.CriticalStrip.Diagram.nodalExchangePolynomial_coeff line 149
  8. lemma OAI.CriticalStrip.Diagram.nodalExchangePolynomial_degree line 159
  9. lemma OAI.CriticalStrip.Diagram.nodalExchangePolynomial_leading line 169
  10. lemma OAI.CriticalStrip.Diagram.nodalExchangePolynomial_node line 181
  11. theorem OAI.CriticalStrip.Diagram.rationalNodalPolynomial_covariance line 211
  12. lemma OAI.CriticalStrip.Diagram.signSpectral_nodal_eval line 234
  13. theorem OAI.CriticalStrip.Diagram.rationalNodalPolynomial_parity line 258
  14. lemma OAI.CriticalStrip.Diagram.rationalNodalPolynomial_eval_div line 285
  15. lemma OAI.CriticalStrip.Diagram.nodalDatumL_map_eval line 292
  16. lemma OAI.CriticalStrip.Diagram.nodalDatumL_sign line 297
  17. theorem OAI.CriticalStrip.Diagram.torus_sine_pair line 320
  18. theorem OAI.CriticalStrip.Diagram.torus_twice_denominator line 330
  19. theorem OAI.CriticalStrip.Diagram.torus_last_cleared line 351
  20. theorem OAI.CriticalStrip.Diagram.torus_column_lastValue line 375
  21. def OAI.CriticalStrip.Diagram.rationalResidualPolynomial line 416
  22. theorem OAI.CriticalStrip.Diagram.rationalVacuum_stationary line 421
  23. theorem OAI.CriticalStrip.Diagram.rationalResidualPolynomial_degree line 430
  24. theorem OAI.CriticalStrip.Diagram.rationalResidualPolynomial_at_node line 460
  25. def OAI.CriticalStrip.Diagram.rationalResidualCoefficient line 509
  26. theorem OAI.CriticalStrip.Diagram.rationalResidualPolynomial_factor line 512