OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumCircuitTwoLocal.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual unary-clock circuit matrix admits a polynomial-size real 2-local approximation with an explicit finite interaction family.

  1. def OAI.ContinuumCoulomb.qmaCircuitLocalModel line 13
  2. theorem OAI.ContinuumCoulomb.qmaCircuitLocalModel_energy line 26
  3. theorem OAI.ContinuumCoulomb.qmaCircuitLocalModel_size line 31
  4. theorem OAI.ContinuumCoulomb.qmaCircuitLocalModel_yes line 36
  5. theorem OAI.ContinuumCoulomb.qmaCircuitLocalModel_no line 46
  6. theorem OAI.ContinuumCoulomb.qmaCircuit_two_local line 59