OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumSweepCells.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Literal natural row/column tags for the sparse sweep. The three gates of each wire transfer carry the same column; the original gate keeps its proved arrival column.

  1. def OAI.ContinuumCoulomb.QuantumSweepCells.repeatColumns line 14
  2. def OAI.ContinuumCoulomb.QuantumSweepCells.columns line 16
  3. def OAI.ContinuumCoulomb.QuantumSweepCells.rowColumns line 19
  4. def OAI.ContinuumCoulomb.QuantumSweepCells.rowCells line 25
  5. def OAI.ContinuumCoulomb.QuantumSweepCells.sweepCells line 28
  6. def OAI.ContinuumCoulomb.QuantumSweepCells.value line 32
  7. theorem OAI.ContinuumCoulomb.QuantumSweepCells.transfer_columns line 35
  8. theorem OAI.ContinuumCoulomb.QuantumSweepCells.columns_actual line 47
  9. theorem OAI.ContinuumCoulomb.QuantumSweepCells.arrival_actual line 55
  10. theorem OAI.ContinuumCoulomb.QuantumSweepCells.rowColumns_actual line 61
  11. theorem OAI.ContinuumCoulomb.QuantumSweepCells.rowCells_actual line 69
  12. theorem OAI.ContinuumCoulomb.QuantumSweepCells.sweepCells_cons line 82
  13. theorem OAI.ContinuumCoulomb.QuantumSweepCells.sweepCells_actual line 96
  14. theorem OAI.ContinuumCoulomb.QuantumSweepCells.value_actual line 108
  15. theorem OAI.ContinuumCoulomb.QuantumSweepCells.value_length line 112