OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumRealLocalFamily.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

A real Hermitian six-local circuit Hamiltonian, with explicit linear term count and the proved complete Hilbert-space promise gap.

  1. theorem OAI.ContinuumCoulomb.qmaRebitOnQubits_zero line 13
  2. theorem OAI.ContinuumCoulomb.qmaRebitOnQubits_sum line 18
  3. theorem OAI.ContinuumCoulomb.qmaRebitOnQubits_hermitian line 28
  4. def OAI.ContinuumCoulomb.qmaRealCircuitTermSites line 33
  5. def OAI.ContinuumCoulomb.qmaRealCircuitTermMatrix line 36
  6. theorem OAI.ContinuumCoulomb.qmaRealCircuitTerm_local line 39
  7. theorem OAI.ContinuumCoulomb.qmaRealCircuitTerm_support_card line 43
  8. theorem OAI.ContinuumCoulomb.qmaRealCircuitTerm_hermitian line 50
  9. theorem OAI.ContinuumCoulomb.qmaRealCircuitTerm_real line 54
  10. theorem OAI.ContinuumCoulomb.qmaRealCircuitTerm_sum line 58
  11. theorem OAI.ContinuumCoulomb.qmaRealCircuitTerm_sound line 64
  12. theorem OAI.ContinuumCoulomb.qmaRealCircuitQubit_card line 73
  13. theorem OAI.ContinuumCoulomb.qmaRealCircuitTerm_accepting line 78