OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumForkListInitialSpatial.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

A bounded-density local input list yields the actual degree-three spatial output, with its full Hamiltonian and fixed density constant.

  1. def OAI.ContinuumCoulomb.QuantumForkList.spatialDensity line 14
  2. structure OAI.ContinuumCoulomb.QuantumForkList.SpatialInput line 16
  3. def OAI.ContinuumCoulomb.QuantumForkList.SpatialInput.state line 31
  4. def OAI.ContinuumCoulomb.QuantumForkList.SpatialInput.cells line 33
  5. theorem OAI.ContinuumCoulomb.QuantumForkList.SpatialInput.validPorts line 37
  6. theorem OAI.ContinuumCoulomb.QuantumForkList.SpatialInput.state_bounded line 40
  7. theorem OAI.ContinuumCoulomb.QuantumForkList.SpatialInput.state_noLoops line 43
  8. theorem OAI.ContinuumCoulomb.QuantumForkList.SpatialInput.state_density line 46
  9. theorem OAI.ContinuumCoulomb.QuantumForkList.SpatialInput.state_degree line 52
  10. theorem OAI.ContinuumCoulomb.QuantumForkList.SpatialInput.state_locality line 55
  11. def OAI.ContinuumCoulomb.QuantumForkList.SpatialInput.model line 59
  12. theorem OAI.ContinuumCoulomb.QuantumForkList.SpatialInput.model_n line 63
  13. theorem OAI.ContinuumCoulomb.QuantumForkList.SpatialInput.model_rows line 65
  14. theorem OAI.ContinuumCoulomb.QuantumForkList.SpatialInput.model_width line 67
  15. theorem OAI.ContinuumCoulomb.QuantumForkList.SpatialInput.model_ordinal line 69
  16. theorem OAI.ContinuumCoulomb.QuantumForkList.SpatialInput.model_energy line 71
  17. theorem OAI.ContinuumCoulomb.QuantumForkList.SpatialInput.model_degree line 76