OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/PrefactorSourceContactCorrectness.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The prefactor-aware program retains the exact final graph enumeration, and calibrates its original weights at the physical unit-charge scale.

  1. def OAI.ContinuumCoulomb.PrefactorSourceContactProgram.weights line 12
  2. theorem OAI.ContinuumCoulomb.PrefactorSourceContactProgram.electron_count line 16
  3. theorem OAI.ContinuumCoulomb.PrefactorSourceContactProgram.electron_count_positive line 23
  4. theorem OAI.ContinuumCoulomb.PrefactorSourceContactProgram.input_eq_graphInput line 29
  5. theorem OAI.ContinuumCoulomb.PrefactorSourceContactProgram.value_eq_array line 40
  6. theorem OAI.ContinuumCoulomb.PrefactorSourceContactProgram.source_weight_range line 54