OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumHistoryDeltaProgram.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A polynomial exact-arithmetic program for the propagation delta entry. Only equality scans depend on circuit size; the matrix arity stays local.

  1. opaque OAI.ContinuumCoulomb.QuantumHistoryDelta.guardProgram line 14
  2. opaque OAI.ContinuumCoulomb.QuantumHistoryDelta.clockCountProgram line 31
  3. opaque OAI.ContinuumCoulomb.QuantumHistoryDelta.allCountProgram line 37
  4. opaque OAI.ContinuumCoulomb.QuantumHistoryDelta.flippedProgram line 42
  5. opaque OAI.ContinuumCoulomb.QuantumHistoryDelta.sameClockProgram line 50
  6. opaque OAI.ContinuumCoulomb.QuantumHistoryDelta.gateEntryProgram line 57
  7. opaque OAI.ContinuumCoulomb.QuantumHistoryDelta.program line 66
  8. def OAI.ContinuumCoulomb.QuantumHistoryDelta.certificate line 79