OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPreparedVerifier.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual verifier generator followed by the sparse-circuit compiler. The unary size certificate is computed from the original input and retained through the arbitrary given generator before its binary registers are parsed.

  1. def OAI.ContinuumCoulomb.QuantumVerifier.prefixProgram line 17
  2. def OAI.ContinuumCoulomb.QuantumVerifier.generateUnary line 23
  3. def OAI.ContinuumCoulomb.QuantumVerifier.preparedUniform line 45
  4. theorem OAI.ContinuumCoulomb.QuantumVerifier.prepared_complete line 50
  5. theorem OAI.ContinuumCoulomb.QuantumVerifier.prepared_sound line 59