OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumRoutingProgram.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Literal polynomial rational programs for the crossing coefficients and penalty.

  1. abbrev OAI.ContinuumCoulomb.QuantumRoutingCode.Triple line 13
  2. def OAI.ContinuumCoulomb.QuantumRoutingCode.tripleCode line 14
  3. opaque OAI.ContinuumCoulomb.QuantumRoutingCode.firstProgram line 16
  4. opaque OAI.ContinuumCoulomb.QuantumRoutingCode.tailProgram line 17
  5. opaque OAI.ContinuumCoulomb.QuantumRoutingCode.secondProgram line 19
  6. opaque OAI.ContinuumCoulomb.QuantumRoutingCode.thirdProgram line 21
  7. def OAI.ContinuumCoulomb.QuantumRoutingCode.squareProgram line 24
  8. def OAI.ContinuumCoulomb.QuantumRoutingCode.twiceProductProgram line 28
  9. opaque OAI.ContinuumCoulomb.QuantumRoutingCode.sumPlusOneProgram line 34
  10. opaque OAI.ContinuumCoulomb.QuantumRoutingCode.cubeProgram line 39
  11. opaque OAI.ContinuumCoulomb.QuantumRoutingCode.scaleProgram line 43
  12. def OAI.ContinuumCoulomb.QuantumRoutingCode.scaleCertificate line 51
  13. theorem OAI.ContinuumCoulomb.QuantumRoutingCode.scale_cast line 54
  14. opaque OAI.ContinuumCoulomb.QuantumRoutingCode.offsetProgram line 59
  15. def OAI.ContinuumCoulomb.QuantumRoutingCode.coefficients line 66
  16. opaque OAI.ContinuumCoulomb.QuantumRoutingCode.coefficientProgram line 70
  17. opaque OAI.ContinuumCoulomb.QuantumRoutingCode.coefficientListProgram line 105
  18. def OAI.ContinuumCoulomb.QuantumRoutingCode.coefficientListCertificate line 109
  19. theorem OAI.ContinuumCoulomb.QuantumRoutingCode.coefficients_spoke line 112
  20. theorem OAI.ContinuumCoulomb.QuantumRoutingCode.coefficients_perimeter line 117
  21. theorem OAI.ContinuumCoulomb.QuantumRoutingCode.coefficients_offset line 121