OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumLocalModel.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Finite real local families and the three gadget stages used by the circuit-to-spin reduction. This records mathematical families, not a compiler.

  1. structure OAI.ContinuumCoulomb.QMARealLocalModel line 14
  2. def OAI.ContinuumCoulomb.QMARealLocalModel.energy line 29
  3. def OAI.ContinuumCoulomb.QMARealLocalModel.qubits line 32
  4. def OAI.ContinuumCoulomb.QMARealLocalModel.terms line 34
  5. theorem OAI.ContinuumCoulomb.QMARealLocalModel.subdivision line 36
  6. theorem OAI.ContinuumCoulomb.QMARealLocalModel.third line 46
  7. theorem OAI.ContinuumCoulomb.QMARealLocalModel.six_to_two line 56