OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumForkListData.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Ordered rational data for the degree-three fork compiler. Original centers retain their numbers. Each pair of active ports receives two consecutive new spin numbers, and an unpaired port remains active at its original center.

  1. abbrev OAI.ContinuumCoulomb.QuantumForkList.Port line 14
  2. abbrev OAI.ContinuumCoulomb.QuantumForkList.Pair line 15
  3. abbrev OAI.ContinuumCoulomb.QuantumForkList.Groups line 16
  4. abbrev OAI.ContinuumCoulomb.QuantumForkList.State line 17
  5. abbrev OAI.ContinuumCoulomb.QuantumForkList.TaggedPair line 18
  6. def OAI.ContinuumCoulomb.QuantumForkList.portAt line 20
  7. def OAI.ContinuumCoulomb.QuantumForkList.groupAt line 21
  8. def OAI.ContinuumCoulomb.QuantumForkList.pairs line 23
  9. def OAI.ContinuumCoulomb.QuantumForkList.unpaired line 26
  10. def OAI.ContinuumCoulomb.QuantumForkList.catalog line 28
  11. def OAI.ContinuumCoulomb.QuantumForkList.pairCount line 31
  12. def OAI.ContinuumCoulomb.QuantumForkList.pairStart line 32
  13. def OAI.ContinuumCoulomb.QuantumForkList.pairLinear line 34
  14. def OAI.ContinuumCoulomb.QuantumForkList.pairSquare line 35
  15. def OAI.ContinuumCoulomb.QuantumForkList.pairOffset line 36
  16. def OAI.ContinuumCoulomb.QuantumForkList.retained line 38
  17. def OAI.ContinuumCoulomb.QuantumForkList.scale line 41
  18. def OAI.ContinuumCoulomb.QuantumForkList.pairBonds line 48
  19. def OAI.ContinuumCoulomb.QuantumForkList.addedBonds line 54
  20. def OAI.ContinuumCoulomb.QuantumForkList.nextGroup line 59
  21. def OAI.ContinuumCoulomb.QuantumForkList.next line 63
  22. def OAI.ContinuumCoulomb.QuantumForkList.iterate line 71
  23. theorem OAI.ContinuumCoulomb.QuantumForkList.pairs_length line 75
  24. theorem OAI.ContinuumCoulomb.QuantumForkList.unpaired_length line 78
  25. theorem OAI.ContinuumCoulomb.QuantumForkList.unpaired_length_le line 82
  26. theorem OAI.ContinuumCoulomb.QuantumForkList.pairCount_cons line 86
  27. theorem OAI.ContinuumCoulomb.QuantumForkList.groupAt_cons_zero line 89
  28. theorem OAI.ContinuumCoulomb.QuantumForkList.groupAt_cons_succ line 91
  29. theorem OAI.ContinuumCoulomb.QuantumForkList.catalog_length line 95
  30. theorem OAI.ContinuumCoulomb.QuantumForkList.pairBonds_length line 103
  31. theorem OAI.ContinuumCoulomb.QuantumForkList.nextGroup_length line 106
  32. theorem OAI.ContinuumCoulomb.QuantumForkList.next_centers line 110
  33. theorem OAI.ContinuumCoulomb.QuantumForkList.next_count line 113
  34. theorem OAI.ContinuumCoulomb.QuantumForkList.iterate_centers line 115
  35. theorem OAI.ContinuumCoulomb.QuantumForkList.next_group_length line 121
  36. theorem OAI.ContinuumCoulomb.QuantumForkList.iterate_group_length line 130
  37. theorem OAI.ContinuumCoulomb.QuantumForkList.addedBonds_length line 139
  38. theorem OAI.ContinuumCoulomb.QuantumForkList.next_bonds_length line 147
  39. theorem OAI.ContinuumCoulomb.QuantumForkList.iterate_group_bound line 152