A familiar molecule. A first proven floor.

Ethanol is the alcohol in beer and wine, a fuel blended into gasoline, the active ingredient in hand sanitizer, and one of the most common solvents in chemistry.

Because real molecules are too complex to solve exactly, chemists study mathematical models of them—and the most fundamental number a model gives is its ground-state energy, the lowest energy its electrons can have. It underlies how stable a molecule is and how it reacts.

BECOME Quantum has certified both a lower and an upper bound on the ground-state energy of an ethanol active-space Hamiltonian, separated by just 10⁻¹⁰ Ha. That's about 16 million times tighter than "chemical accuracy" (1 kcal/mol), the precision chemists usually aim for.

To our knowledge, this is the first rigorous lower bound ever published for an ethanol Hamiltonian, and the first cryptographically proven one. Both bounds are machine-checked in the Coq proof assistant, and backed by a succinct cryptographic proof that can be verified in seconds by anyone, without having to trust us.

Variational upper-bound estimates for ethanol have existed for decades. A proven floor never has.

Here is the certified result from BECOME Quantum:

Ethanol (C₂H₆O) · PubChem CID 702 · CAS(8e,8o), RHF/6-31G* at the PubChemQC PM6 geometry

• Lower bound: −154.0733873199 Ha
• Upper bound: −154.0733873198 Ha
• Bracket width: 1 × 10⁻¹⁰ Ha (6.3 × 10⁻⁸ kcal/mol)

Yes, a CAS(8,8) can be diagonalized in milliseconds. But that gives a floating-point estimate, not a proof: "exact" diagonalization means no truncation, not exact arithmetic. These bounds are proven, machine-checked, and verifiable in seconds.

Why does a proven lower bound matter?

Every variational workhorse in quantum chemistry (Hartree–Fock, CI, DMRG, variational QMC) gives an upper-bound estimate. They tell us the true model energy is no higher than a calculated value, but not how far below it might sit. A rigorous lower bound closes the other side:

1. It turns estimates into guarantees. A numerical solver tells you what it found; certified lower and upper bounds tell you where the true eigenvalue must lie. Precision tells you what you calculated. Proof tells you how wrong you could be.
2. It isolates model error from solver error. Reaction barriers, binding energies, and conformer preferences depend on tiny energy differences. Certified intervals eliminate numerical solver uncertainty so researchers know whether an error comes from the physics of the model or the math of the solver. Better bounds mean more trustworthy benchmarks.
3. It rules out impossible answers. If any method reports an energy below the certified lower bound for the same Hamiltonian, that answer is wrong. This settles disagreements between solvers and exposes bugs and input errors. Methods can disagree. Mathematics rules out impossible answers.
4. It gives quantum computing and AI a verifiable ground truth. Training machine-learning potentials and benchmarking quantum algorithms require reference values with proven error bounds, not unverified floating-point estimates. You can't prove computational advantage with an unproven reference.

Rigorous lower bounds have historically been rare because classical lower-bound techniques are either too loose or computationally intractable beyond tiny toy systems.

And ethanol isn't a one-off. It is one of 125,999 molecules we have certified the exact same way. Each comes with a standardized CAS(8e,8o) Hamiltonian (HOMO−3 to LUMO+3, RHF/6-31G*) and a machine-checked lower and upper bound on its ground-state energy, cryptographically tied to the exact FCIDUMP by its SHA-256 fingerprint.

The certified energies are available under a commercial license: https://become.belovedecosystem.com/licensing/certified-ground-state-energies/cas-8e-8o-active-space-hamiltonians/

Computational chemistry has spent decades chasing better estimates. BECOME Quantum replaces estimates with mathematical proof—a certified floor and ceiling on the Hamiltonian in front of you, verifiable by anyone.