OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumParallelRouteSearch.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The predicate mask and the path list have the same 140-entry order. Searching the mask therefore returns the path of the actual first permitted catalog route, without encoding proof-carrying route objects.

  1. theorem OAI.ContinuumCoulomb.QuantumFiniteRouteSearch.mapped_drop_findIdx line 13
  2. def OAI.ContinuumCoulomb.QuantumFiniteRouteSearch.selectParallelValue line 23
  3. theorem OAI.ContinuumCoulomb.QuantumFiniteRouteSearch.selectParallelValue_eq line 26
  4. def OAI.ContinuumCoulomb.QuantumFiniteRouteSearch.selectParallelProgram line 36