OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumOrderedCoefficient.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Exact rational-register tables for every actual ordered history term. Only the propagation core is multiplied, so its summation has at most 32 states regardless of the number of spectator qubits.

  1. def OAI.ContinuumCoulomb.QuantumAlgebraicHistory.diagonal line 14
  2. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.denote_diagonal line 17
  3. def OAI.ContinuumCoulomb.QuantumAlgebraicHistory.distributed line 22
  4. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.denote_distributed line 38
  5. def OAI.ContinuumCoulomb.QuantumAlgebraicHistory.localY line 85
  6. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.value_localY line 88
  7. def OAI.ContinuumCoulomb.QuantumAlgebraicHistory.rebit line 99
  8. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.denote_rebit line 107
  9. def OAI.ContinuumCoulomb.QuantumAlgebraicHistory.pairY line 117
  10. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.value_pairY line 121
  11. def OAI.ContinuumCoulomb.QuantumAlgebraicHistory.referenceEdge line 133
  12. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.denote_referenceEdge line 139
  13. def OAI.ContinuumCoulomb.QuantumAlgebraicHistory.orderedTerm line 153
  14. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.denote_orderedTerm line 161
  15. def OAI.ContinuumCoulomb.QuantumAlgebraicHistory.orderedCore line 172
  16. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.denote_orderedCore line 178
  17. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.orderedCoefficient_eq line 185