OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumFinalRoutingProgram.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Literal fixed-round routing to the serialized square-lattice source.

  1. abbrev OAI.ContinuumCoulomb.QuantumFinalRoutingProgram.Input line 13
  2. def OAI.ContinuumCoulomb.QuantumFinalRoutingProgram.inputCode line 14
  3. def OAI.ContinuumCoulomb.QuantumFinalRoutingProgram.planar line 16
  4. def OAI.ContinuumCoulomb.QuantumFinalRoutingProgram.even line 18
  5. opaque OAI.ContinuumCoulomb.QuantumFinalRoutingProgram.roundsValue line 20
  6. def OAI.ContinuumCoulomb.QuantumFinalRoutingProgram.rounds line 21
  7. theorem OAI.ContinuumCoulomb.QuantumFinalRoutingProgram.rounds_eq line 22
  8. def OAI.ContinuumCoulomb.QuantumFinalRoutingProgram.routed line 23
  9. def OAI.ContinuumCoulomb.QuantumFinalRoutingProgram.value line 25
  10. opaque OAI.ContinuumCoulomb.QuantumFinalRoutingProgram.spatialInputProgram line 28
  11. opaque OAI.ContinuumCoulomb.QuantumFinalRoutingProgram.thresholdsProgram line 30
  12. opaque OAI.ContinuumCoulomb.QuantumFinalRoutingProgram.precisionProgram line 32
  13. opaque OAI.ContinuumCoulomb.QuantumFinalRoutingProgram.planarProgram line 34
  14. opaque OAI.ContinuumCoulomb.QuantumFinalRoutingProgram.evenProgram line 38
  15. opaque OAI.ContinuumCoulomb.QuantumFinalRoutingProgram.routedProgram line 41
  16. opaque OAI.ContinuumCoulomb.QuantumFinalRoutingProgram.program line 44
  17. theorem OAI.ContinuumCoulomb.QuantumFinalRoutingProgram.planar_value_bounded line 48
  18. theorem OAI.ContinuumCoulomb.QuantumFinalRoutingProgram.planar_bounded line 53
  19. theorem OAI.ContinuumCoulomb.QuantumFinalRoutingProgram.even_valid line 57
  20. theorem OAI.ContinuumCoulomb.QuantumFinalRoutingProgram.routed_valid line 61
  21. theorem OAI.ContinuumCoulomb.QuantumFinalRoutingProgram.energy_error line 66
  22. def OAI.ContinuumCoulomb.QuantumFinalRoutingProgram.certificate line 87