OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumCellCatalogProgram.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Literal polynomial evaluation of all 140 path candidates. Every template is constant-sized, and only its endpoint cell coordinates vary.

  1. def OAI.ContinuumCoulomb.QuantumCellPathProgram.appendPaths line 13
  2. def OAI.ContinuumCoulomb.QuantumCellPathProgram.singletonPath line 19
  3. def OAI.ContinuumCoulomb.QuantumCellPathProgram.flatFamilyProgram line 25
  4. opaque OAI.ContinuumCoulomb.QuantumCellPathProgram.corridorBlockProgram line 36
  5. opaque OAI.ContinuumCoulomb.QuantumCellPathProgram.bodyPathsProgram line 47
  6. opaque OAI.ContinuumCoulomb.QuantumCellPathProgram.orientedPathProgram line 58
  7. opaque OAI.ContinuumCoulomb.QuantumCellPathProgram.bodyAtProgram line 66
  8. theorem OAI.ContinuumCoulomb.QuantumCellPathProgram.ofFn_headD_map line 71
  9. opaque OAI.ContinuumCoulomb.QuantumCellPathProgram.cellPathsProgram line 80
  10. abbrev OAI.ContinuumCoulomb.QuantumCellPathProgram.Endpoints line 95
  11. def OAI.ContinuumCoulomb.QuantumCellPathProgram.endpointsCode line 96
  12. opaque OAI.ContinuumCoulomb.QuantumCellPathProgram.pointCellProgram line 98
  13. opaque OAI.ContinuumCoulomb.QuantumCellPathProgram.candidatePathsProgram line 103