OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/NuclearPromise.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Exact finite encodings and continuum promise problems of both main theorems. Nuclear coordinates and positive charges are binary, electrons are unary, and the threshold separation is at least one. Energies are the full spinful antisymmetric weak-H¹ infima, with no finite-orbital restriction.

  1. structure OAI.ContinuumCoulomb.BinaryPosition line 14

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:434 (same declaration text).

  2. def OAI.ContinuumCoulomb.BinaryPosition.value line 20

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:440 (same declaration text).

  3. def OAI.ContinuumCoulomb.BinaryPosition.Valid line 22

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:442 (same declaration text).

  4. def OAI.ContinuumCoulomb.binaryPositionEquiv line 25

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:445 (same declaration text).

  5. def OAI.ContinuumCoulomb.binaryPositionCodec line 31

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:451 (same declaration text).

  6. structure OAI.ContinuumCoulomb.BinaryCoulomb line 34

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:454 (same declaration text).

  7. def OAI.ContinuumCoulomb.binaryCoulombEquiv line 41

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:461 (same declaration text).

  8. def OAI.ContinuumCoulomb.binaryCoulombCodec line 48

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:468 (same declaration text).

  9. structure OAI.ContinuumCoulomb.BinaryCoulomb.Valid line 52

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:472 (same declaration text).

  10. def OAI.ContinuumCoulomb.BinaryCoulomb.toData line 62

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:482 (same declaration text).

  11. structure OAI.ContinuumCoulomb.UnitCoulomb line 72

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:492 (same declaration text).

  12. def OAI.ContinuumCoulomb.unitCoulombEquiv line 79

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:499 (same declaration text).

  13. def OAI.ContinuumCoulomb.unitCoulombCodec line 85

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:505 (same declaration text).

  14. structure OAI.ContinuumCoulomb.UnitCoulomb.Valid line 89

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:509 (same declaration text).

  15. def OAI.ContinuumCoulomb.UnitCoulomb.toData line 98

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:518 (same declaration text).

  16. def OAI.ContinuumCoulomb.binaryCoulombPromise line 108

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:526 (same declaration text).

  17. def OAI.ContinuumCoulomb.unitCoulombPromise line 118

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:536 (same declaration text).