OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumManhattanListProgram.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Enumerate the Manhattan segment with an explicit fixed route budget. The cap makes enumeration polynomial on every input, and disappears for the spatial routes satisfying the proved length bound.

  1. abbrev OAI.ContinuumCoulomb.QuantumManhattanListProgram.Ends line 15
  2. def OAI.ContinuumCoulomb.QuantumManhattanListProgram.endsCode line 16
  3. def OAI.ContinuumCoulomb.QuantumManhattanListProgram.value line 18
  4. def OAI.ContinuumCoulomb.QuantumManhattanListProgram.distanceProgram line 21
  5. def OAI.ContinuumCoulomb.QuantumManhattanListProgram.program line 26
  6. theorem OAI.ContinuumCoulomb.QuantumManhattanListProgram.value_exact line 35