OAI/MathematicalPhysics/ContinuumCoulomb/Programs/PrefactorSourceContactProgram.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Raw-source contact coordinates with precisely the amplification forced by the unit-charge mesh. The calibration base is the thirtieth power of the encoded source size, so its amplification is a cube.

  1. def OAI.ContinuumCoulomb.PrefactorSourceContactProgram.input line 14
  2. def OAI.ContinuumCoulomb.PrefactorSourceContactProgram.value line 22
  3. opaque OAI.ContinuumCoulomb.PrefactorSourceContactProgram.coefficientsProgram line 26
  4. opaque OAI.ContinuumCoulomb.PrefactorSourceContactProgram.inputProgram line 33
  5. opaque OAI.ContinuumCoulomb.PrefactorSourceContactProgram.program line 41
  6. def OAI.ContinuumCoulomb.PrefactorSourceContactProgram.certificate line 46