OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumOrderedSampling.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Sampling the exact ordered-history coefficients controls the actual full-space ground energy. Odd-Y words are omitted by the proved real Pauli expansion, leaving at most 4096 words per six-site history term.

  1. abbrev OAI.ContinuumCoulomb.QuantumAlgebraicHistory.OrderedPauliTerm line 15
  2. def OAI.ContinuumCoulomb.QuantumAlgebraicHistory.orderedWord line 18
  3. def OAI.ContinuumCoulomb.QuantumAlgebraicHistory.orderedRealCoefficient line 22
  4. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.orderedRealCoefficient_value line 26
  5. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.orderedWord_even line 33
  6. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.orderedWord_support line 37
  7. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.orderedWord_count line 41
  8. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.orderedPauli_sum line 52
  9. def OAI.ContinuumCoulomb.QuantumAlgebraicHistory.sampledOrderedWeight line 60
  10. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.sampledOrdered_error line 64