OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumCircuitCode.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Actual parsing of the verifier's prefix circuit encoding. Register sizes are clipped to supplied unary bounds before later finite enumerations.

  1. def OAI.ContinuumCoulomb.QuantumCircuitCode.gateCode line 15
  2. def OAI.ContinuumCoulomb.QuantumCircuitCode.rawCode line 18
  3. def OAI.ContinuumCoulomb.QuantumCircuitCode.circuitCode line 21
  4. def OAI.ContinuumCoulomb.QuantumCircuitCode.sumView line 24
  5. def OAI.ContinuumCoulomb.QuantumCircuitCode.sumSplitter line 30
  6. def OAI.ContinuumCoulomb.QuantumCircuitCode.gateSplitter line 49
  7. def OAI.ContinuumCoulomb.QuantumCircuitCode.gateInput line 54
  8. theorem OAI.ContinuumCoulomb.QuantumCircuitCode.gate_length_pos line 67
  9. def OAI.ContinuumCoulomb.QuantumCircuitCode.gateListSplitter line 70
  10. def OAI.ContinuumCoulomb.QuantumCircuitCode.gateListInput line 73
  11. def OAI.ContinuumCoulomb.QuantumCircuitCode.tailCodec line 79
  12. def OAI.ContinuumCoulomb.QuantumCircuitCode.circuitTuple line 82
  13. def OAI.ContinuumCoulomb.QuantumCircuitCode.workInput line 87
  14. def OAI.ContinuumCoulomb.QuantumCircuitCode.restInput line 90
  15. def OAI.ContinuumCoulomb.QuantumCircuitCode.witnessInput line 97
  16. def OAI.ContinuumCoulomb.QuantumCircuitCode.gatesInput line 100
  17. def OAI.ContinuumCoulomb.QuantumCircuitCode.rawInput line 103
  18. def OAI.ContinuumCoulomb.QuantumCircuitCode.cap line 106
  19. def OAI.ContinuumCoulomb.QuantumCircuitCode.boundedInput line 109
  20. theorem OAI.ContinuumCoulomb.QuantumCircuitCode.cap_eq line 117
  21. theorem OAI.ContinuumCoulomb.QuantumCircuitCode.cap_eq_of_wellFormed line 122
  22. def OAI.ContinuumCoulomb.QuantumCircuitCode.workProgram line 126
  23. def OAI.ContinuumCoulomb.QuantumCircuitCode.tailProgram line 129
  24. def OAI.ContinuumCoulomb.QuantumCircuitCode.witnessProgram line 134
  25. def OAI.ContinuumCoulomb.QuantumCircuitCode.gatesProgram line 137
  26. def OAI.ContinuumCoulomb.QuantumCircuitCode.nonemptyProgram line 140