OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumHistoryLiteralPromise.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

One polynomial promise exponent for the literal circuit-to-source program, with the original verifier's empty circuits prepared explicitly.

  1. theorem OAI.ContinuumCoulomb.QuantumHistorySourceProgram.circuit_polynomialPromise line 15