OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumBufferedArmProgram.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Literal evaluation and enumeration of the three buffered endpoint arms. The lane color is unary, as required by the polynomial geometric size bound.

  1. def OAI.ContinuumCoulomb.QuantumBufferedArmProgram.add line 15
  2. def OAI.ContinuumCoulomb.QuantumBufferedArmProgram.sub line 18
  3. def OAI.ContinuumCoulomb.QuantumBufferedArmProgram.mul line 21
  4. def OAI.ContinuumCoulomb.QuantumBufferedArmProgram.le line 24
  5. def OAI.ContinuumCoulomb.QuantumBufferedArmProgram.u line 29
  6. def OAI.ContinuumCoulomb.QuantumBufferedArmProgram.v line 30
  7. def OAI.ContinuumCoulomb.QuantumBufferedArmProgram.k line 31
  8. def OAI.ContinuumCoulomb.QuantumBufferedArmProgram.c line 32
  9. def OAI.ContinuumCoulomb.QuantumBufferedArmProgram.doglegProgram line 35
  10. def OAI.ContinuumCoulomb.QuantumBufferedArmProgram.detourProgram line 43
  11. def OAI.ContinuumCoulomb.QuantumBufferedArmProgram.point line 54
  12. def OAI.ContinuumCoulomb.QuantumBufferedArmProgram.length line 60
  13. theorem OAI.ContinuumCoulomb.QuantumBufferedArmProgram.point_eq line 63
  14. theorem OAI.ContinuumCoulomb.QuantumBufferedArmProgram.length_eq line 66
  15. def OAI.ContinuumCoulomb.QuantumBufferedArmProgram.pointProgram line 72
  16. def OAI.ContinuumCoulomb.QuantumBufferedArmProgram.lengthProgram line 89
  17. def OAI.ContinuumCoulomb.QuantumBufferedArmProgram.listProgram line 98