OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumHistorySpatial.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The actual sparse verifier history has a fixed-density, degree-three spatial exchange output. Its energy is that of the literal fork compiler.

  1. def OAI.ContinuumCoulomb.QuantumHistorySpatial.rawDensity line 14
  2. def OAI.ContinuumCoulomb.QuantumHistorySpatial.finalDensity line 15
  3. theorem OAI.ContinuumCoulomb.QuantumHistorySpatial.padded_anchor_density line 17
  4. def OAI.ContinuumCoulomb.QuantumHistorySpatial.input line 27
  5. theorem OAI.ContinuumCoulomb.QuantumHistorySpatial.input_state line 48
  6. def OAI.ContinuumCoulomb.QuantumHistorySpatial.model line 56
  7. theorem OAI.ContinuumCoulomb.QuantumHistorySpatial.model_energy line 60
  8. theorem OAI.ContinuumCoulomb.QuantumHistorySpatial.model_history_error line 67
  9. theorem OAI.ContinuumCoulomb.QuantumHistorySpatial.model_degree line 75