OAI/MathematicalPhysics/ContinuumCoulomb/Programs/UnitBinaryProgram.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Literal polynomial-time inclusion of unit-charge Coulomb instances into the binary-charge promise. The machine parses the position list, attaches charge one to each position and preserves the entire encoded electron/threshold tail.

  1. abbrev OAI.ContinuumCoulomb.UnitBinaryProgram.positionListCodec line 15
  2. abbrev OAI.ContinuumCoulomb.UnitBinaryProgram.nucleusCodec line 16
  3. abbrev OAI.ContinuumCoulomb.UnitBinaryProgram.nucleusListCodec line 17
  4. abbrev OAI.ContinuumCoulomb.UnitBinaryProgram.tailCodec line 18
  5. def OAI.ContinuumCoulomb.UnitBinaryProgram.zeroPosition line 20
  6. opaque OAI.ContinuumCoulomb.UnitBinaryProgram.positionSplitter line 22
  7. theorem OAI.ContinuumCoulomb.UnitBinaryProgram.position_length_pos line 27
  8. opaque OAI.ContinuumCoulomb.UnitBinaryProgram.positionListSplitter line 34
  9. opaque OAI.ContinuumCoulomb.UnitBinaryProgram.inputTuple line 37
  10. opaque OAI.ContinuumCoulomb.UnitBinaryProgram.positionsRaw line 41
  11. opaque OAI.ContinuumCoulomb.UnitBinaryProgram.tailRaw line 43
  12. opaque OAI.ContinuumCoulomb.UnitBinaryProgram.positions line 45
  13. opaque OAI.ContinuumCoulomb.UnitBinaryProgram.attachOne line 49
  14. opaque OAI.ContinuumCoulomb.UnitBinaryProgram.nuclei line 55
  15. opaque OAI.ContinuumCoulomb.UnitBinaryProgram.program line 60
  16. def OAI.ContinuumCoulomb.UnitBinaryProgram.certificate line 65
  17. def OAI.ContinuumCoulomb.UnitBinaryProgram.reduction line 68
  18. theorem OAI.ContinuumCoulomb.UnitBinaryProgram.binary_hard_of_unit line 75