OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumSupportLookup.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

The actual local support coordinates are read by literal label lookup. This identifies a small matrix input with its zero extension on spectator qubits, without enumerating the ambient spin basis.

  1. abbrev OAI.ContinuumCoulomb.QuantumSupportLookup.Input line 15
  2. def OAI.ContinuumCoulomb.QuantumSupportLookup.inputCode line 16
  3. def OAI.ContinuumCoulomb.QuantumSupportLookup.value line 19
  4. def OAI.ContinuumCoulomb.QuantumSupportLookup.matchesProgram line 21
  5. def OAI.ContinuumCoulomb.QuantumSupportLookup.indexProgram line 28
  6. def OAI.ContinuumCoulomb.QuantumSupportLookup.program line 39
  7. def OAI.ContinuumCoulomb.QuantumSupportLookup.certificate line 47
  8. theorem OAI.ContinuumCoulomb.QuantumSupportLookup.value_get line 50
  9. theorem OAI.ContinuumCoulomb.QuantumSupportLookup.value_absent line 58
  10. theorem OAI.ContinuumCoulomb.QuantumSupportLookup.value_map_get line 64
  11. theorem OAI.ContinuumCoulomb.QuantumSupportLookup.value_not_mem line 77
  12. theorem OAI.ContinuumCoulomb.QuantumSupportLookup.extend_mem line 86
  13. theorem OAI.ContinuumCoulomb.QuantumSupportLookup.extend_not_mem line 91
  14. def OAI.ContinuumCoulomb.QuantumSupportLookup.supportBits line 96
  15. theorem OAI.ContinuumCoulomb.QuantumSupportLookup.support_value line 101
  16. def OAI.ContinuumCoulomb.QuantumSupportLookup.readBit line 137
  17. theorem OAI.ContinuumCoulomb.QuantumSupportLookup.support_readBit line 139
  18. theorem OAI.ContinuumCoulomb.QuantumSupportLookup.orderedTable_lookup line 150