OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumHistoryXZ.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The literal X/Z family attached to the actual ordered verifier history, including the scalar-sampling error and polynomial counts.

  1. abbrev OAI.ContinuumCoulomb.QuantumAlgebraicHistory.XZTerm line 13
  2. abbrev OAI.ContinuumCoulomb.QuantumAlgebraicHistory.XZQubit line 16
  3. def OAI.ContinuumCoulomb.QuantumAlgebraicHistory.xzWord line 19
  4. def OAI.ContinuumCoulomb.QuantumAlgebraicHistory.xzSites line 23
  5. def OAI.ContinuumCoulomb.QuantumAlgebraicHistory.xzCoefficient line 27
  6. def OAI.ContinuumCoulomb.QuantumAlgebraicHistory.xzEnergy line 30
  7. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.xz_sites_nodup line 34
  8. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.xz_sites_length line 38
  9. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.xz_sites_cover line 42
  10. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.xz_noY line 50
  11. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.xz_support line 55
  12. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.xz_sampled_error line 59
  13. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.xz_accuracy line 65
  14. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.xz_term_count line 73
  15. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.xz_qubit_count line 78