OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumForkGridInitial.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

The initial subdivision computes its row/column array from the actual endpoint list, before the same fixed-round grid program is applied.

  1. abbrev OAI.ContinuumCoulomb.QuantumForkGridProgram.InitialCells line 13
  2. def OAI.ContinuumCoulomb.QuantumForkGridProgram.initialCellsCode line 14
  3. def OAI.ContinuumCoulomb.QuantumForkGridProgram.initialQueryCode line 16
  4. def OAI.ContinuumCoulomb.QuantumForkGridProgram.initialCellProgram line 18
  5. def OAI.ContinuumCoulomb.QuantumForkGridProgram.initialCells line 37
  6. def OAI.ContinuumCoulomb.QuantumForkGridProgram.initialCellsProgram line 40
  7. theorem OAI.ContinuumCoulomb.QuantumForkGridProgram.lookup_initialCells line 59
  8. abbrev OAI.ContinuumCoulomb.QuantumForkGridProgram.PreparedInput line 65
  9. def OAI.ContinuumCoulomb.QuantumForkGridProgram.preparedCode line 66
  10. def OAI.ContinuumCoulomb.QuantumForkGridProgram.prepare line 69
  11. def OAI.ContinuumCoulomb.QuantumForkGridProgram.prepareProgram line 73
  12. def OAI.ContinuumCoulomb.QuantumForkGridProgram.output line 83
  13. def OAI.ContinuumCoulomb.QuantumForkGridProgram.outputProgram line 85
  14. theorem OAI.ContinuumCoulomb.QuantumForkGridProgram.output_state line 88
  15. theorem OAI.ContinuumCoulomb.QuantumForkGridProgram.output_length line 92
  16. theorem OAI.ContinuumCoulomb.QuantumForkGridProgram.prepare_represents line 97
  17. theorem OAI.ContinuumCoulomb.QuantumForkGridProgram.output_represents line 102