OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumUnarySpectrum.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The full qubit-space history Hamiltonian has a strict inverse-polynomial promise gap. No restriction to the valid clock subspace is assumed.

  1. theorem OAI.ContinuumCoulomb.qmaUnaryMass_norm line 12
  2. theorem OAI.ContinuumCoulomb.qmaUnaryHamiltonian_sound line 16
  3. theorem OAI.ContinuumCoulomb.qmaUnaryHamiltonian_accepting line 25
  4. theorem OAI.ContinuumCoulomb.qmaUnaryBasis_card line 46