# QMA-hardness of continuum Coulomb energy

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Continuum Coulomb hardness with binary nuclear charges](../../preprints/Continuum-Coulomb-hardness-with-binary-nuclear-charges-September-24-2026/Continuum-Coulomb-hardness-with-binary-nuclear-charges-September-24-2026.pdf)
- [QMA-hardness of continuum Coulomb energy with unit nuclear charges](../../preprints/QMA-hardness-of-continuum-Coulomb-energy-with-unit-nuclear-charges-September-24-2026/QMA-hardness-of-continuum-Coulomb-energy-with-unit-nuclear-charges-September-24-2026.pdf)

## Scope

The formalization proves QMA-hardness of approximating the electronic Coulomb spectral infimum in three-dimensional continuum space when positive integer nuclear charges are encoded in binary. The instances have distinct rational nuclear positions and a unary electron count, and the energy ranges over antisymmetric continuum states and all spin sectors. A deterministic polynomial-time many-one reduction produces the promise gap with threshold separation at least one, while keeping the complete output length polynomial. The same Comparator file also contains the companion unit-charge result.

The formalization proves QMA-hardness of approximating the electronic ground-energy infimum for clamped unit-charge nuclei in the full spinful fermionic continuum. The reduction is deterministic and polynomial time, with rational nuclear positions and separated rational energy thresholds. No orbital basis, magnetic field, additional external potential, or binding premise is part of the input.

The same Comparator file also includes the companion hardness result when positive integer nuclear charges are encoded in binary.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| QMA-hardness of continuum Coulomb energy with binary charges | [ContinuumCoulombHardness.lean](../ComparatorChallenges/ContinuumCoulombHardness.lean) |
| QMA-hardness of continuum Coulomb ground-energy approximation | [ContinuumCoulombHardness.lean](../ComparatorChallenges/ContinuumCoulombHardness.lean) |