OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumWalkErasure.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The coarse route's library loop erasure is the explicit right-to-left finite-list algorithm. This identifies the actual path data needed by the literal spatial compiler.

  1. def OAI.ContinuumCoulomb.QuantumWalkErasure.step line 17
  2. def OAI.ContinuumCoulomb.QuantumWalkErasure.erase line 20
  3. theorem OAI.ContinuumCoulomb.QuantumWalkErasure.erase_nil line 22
  4. theorem OAI.ContinuumCoulomb.QuantumWalkErasure.erase_cons line 23
  5. theorem OAI.ContinuumCoulomb.QuantumWalkErasure.step_sublist line 25
  6. theorem OAI.ContinuumCoulomb.QuantumWalkErasure.erase_sublist line 31
  7. theorem OAI.ContinuumCoulomb.QuantumWalkErasure.listCode_length_sublist line 39
  8. theorem OAI.ContinuumCoulomb.QuantumWalkErasure.support_dropUntil line 52
  9. theorem OAI.ContinuumCoulomb.QuantumWalkErasure.support_bypass line 60
  10. theorem OAI.ContinuumCoulomb.QMASpatialExchangeModel.bufferedPath_support_explicit line 75