OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumTaggedRouteProgram.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Evaluate each candidate together with its finite permission bit. Keeping that bit attached to the path preserves the exact catalog order during the bounded search, including reversed paths.

  1. abbrev OAI.ContinuumCoulomb.QuantumTaggedRouteProgram.Tagged line 16
  2. def OAI.ContinuumCoulomb.QuantumTaggedRouteProgram.taggedCode line 17
  3. def OAI.ContinuumCoulomb.QuantumTaggedRouteProgram.bodyPermitted line 18
  4. theorem OAI.ContinuumCoulomb.QuantumTaggedRouteProgram.bodyPermitted_eq_true line 20
  5. def OAI.ContinuumCoulomb.QuantumTaggedRouteProgram.tagged line 25
  6. def OAI.ContinuumCoulomb.QuantumTaggedRouteProgram.oriented line 27
  7. def OAI.ContinuumCoulomb.QuantumTaggedRouteProgram.append line 29
  8. def OAI.ContinuumCoulomb.QuantumTaggedRouteProgram.fixedFlat line 34
  9. opaque OAI.ContinuumCoulomb.QuantumTaggedRouteProgram.orientedProgram line 45
  10. def OAI.ContinuumCoulomb.QuantumTaggedRouteProgram.bodyProgram line 55
  11. opaque OAI.ContinuumCoulomb.QuantumTaggedRouteProgram.rayProgram line 62
  12. opaque OAI.ContinuumCoulomb.QuantumTaggedRouteProgram.pairProgram line 71
  13. opaque OAI.ContinuumCoulomb.QuantumTaggedRouteProgram.patchProgram line 80
  14. opaque OAI.ContinuumCoulomb.QuantumTaggedRouteProgram.cellPositiveProgram line 89
  15. opaque OAI.ContinuumCoulomb.QuantumTaggedRouteProgram.corridorProgram line 101
  16. opaque OAI.ContinuumCoulomb.QuantumTaggedRouteProgram.corridorBlock line 113
  17. opaque OAI.ContinuumCoulomb.QuantumTaggedRouteProgram.cellProgram line 126