OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumForkListCellIteration.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The finite label array computed by each literal round represents the geometric cell map at every emitted spin. Fixed-round iteration is polynomial.

  1. def OAI.ContinuumCoulomb.QuantumForkList.RepresentsCells line 14
  2. theorem OAI.ContinuumCoulomb.QuantumForkList.cellAt_nextCells line 17
  3. theorem OAI.ContinuumCoulomb.QuantumForkList.nextCell_congr line 24
  4. theorem OAI.ContinuumCoulomb.QuantumForkList.next_representsCells line 36
  5. def OAI.ContinuumCoulomb.QuantumForkList.cellStep line 44
  6. def OAI.ContinuumCoulomb.QuantumForkList.cellStepProgram line 46
  7. def OAI.ContinuumCoulomb.QuantumForkList.cellIterate line 51
  8. def OAI.ContinuumCoulomb.QuantumForkList.cellIterateProgram line 55
  9. theorem OAI.ContinuumCoulomb.QuantumForkList.cellIterate_state line 60
  10. theorem OAI.ContinuumCoulomb.QuantumForkList.cellIterate_represents line 66