OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumLocalFamily.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A linear-size explicit interaction family for the verified circuit Hamiltonian. Its supports contain at most five qubits.

  1. abbrev OAI.ContinuumCoulomb.QMACircuitTerm line 13
  2. def OAI.ContinuumCoulomb.qmaCircuitTermSites line 16
  3. def OAI.ContinuumCoulomb.qmaCircuitTermMatrix line 23
  4. theorem OAI.ContinuumCoulomb.qmaCircuitTerm_card line 32
  5. theorem OAI.ContinuumCoulomb.qmaCircuitTerm_local line 37
  6. theorem OAI.ContinuumCoulomb.qmaCircuitTerm_support_card line 48
  7. theorem OAI.ContinuumCoulomb.qmaCircuitTerm_sum line 60
  8. theorem OAI.ContinuumCoulomb.qmaCircuitTerm_hermitian line 71