OAI/MathematicalPhysics/ContinuumCoulomb/Reduction/SourceUnitCoulomb.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Literal source-to-unit-Coulomb packaging. The physical nuclei and the full affine threshold pair use the same calibrated sites, amplification, mesh and exact rational slab dimensions.

  1. def OAI.ContinuumCoulomb.SourceUnitCoulomb.input line 13
  2. def OAI.ContinuumCoulomb.SourceUnitCoulomb.value line 18
  3. opaque OAI.ContinuumCoulomb.SourceUnitCoulomb.inputProgram line 22
  4. opaque OAI.ContinuumCoulomb.SourceUnitCoulomb.program line 28
  5. def OAI.ContinuumCoulomb.SourceUnitCoulomb.certificate line 33
  6. theorem OAI.ContinuumCoulomb.SourceUnitCoulomb.nuclei line 38
  7. theorem OAI.ContinuumCoulomb.SourceUnitCoulomb.electrons line 42
  8. theorem OAI.ContinuumCoulomb.SourceUnitCoulomb.lower line 46
  9. theorem OAI.ContinuumCoulomb.SourceUnitCoulomb.upper line 51
  10. theorem OAI.ContinuumCoulomb.SourceUnitCoulomb.nuclei_length line 56
  11. theorem OAI.ContinuumCoulomb.SourceUnitCoulomb.actual_threshold_error line 63
  12. theorem OAI.ContinuumCoulomb.SourceUnitCoulomb.valid_of_nodes line 80