OAI/Combinatorics/PolynomialVacuum/Geometry/HoneycombVertex.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PolynomialVacuumAlgebra.upTurn line 11
  2. def OAI.PolynomialVacuumAlgebra.downTurn line 12
  3. def OAI.PolynomialVacuumAlgebra.occupied line 13
  4. def OAI.PolynomialVacuumAlgebra.anglePhase line 15
  5. theorem OAI.PolynomialVacuumAlgebra.anglePhase_three line 17
  6. theorem OAI.PolynomialVacuumAlgebra.anglePhase_zero line 24
  7. def OAI.PolynomialVacuumAlgebra.honeycombPiece line 28
  8. def OAI.PolynomialVacuumAlgebra.honeycombEntry line 33
  9. lemma OAI.PolynomialVacuumAlgebra.anglePhase_three_neg line 35
  10. lemma OAI.PolynomialVacuumAlgebra.anglePhase_three_pos line 36
  11. lemma OAI.PolynomialVacuumAlgebra.anglePhase_six_neg line 37
  12. lemma OAI.PolynomialVacuumAlgebra.anglePhase_six_pos line 38
  13. lemma OAI.PolynomialVacuumAlgebra.anglePhase_nine_neg line 39
  14. lemma OAI.PolynomialVacuumAlgebra.anglePhase_nine_pos line 40
  15. theorem OAI.PolynomialVacuumAlgebra.honeycomb_entry_exact line 42