OAI/MathematicalPhysics/ContinuumCoulomb/Reduction/SourceCloudComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual source nuclear program has the manufactured Hubbard ground interval. The remaining premises concern only its finite calibrated sites and hopping matrix, not any continuum energy comparison.

  1. theorem OAI.ContinuumCoulomb.source_cloud_comparison line 18