OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumListLattice.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The actual computed coordinate and bond tapes define a valid lattice source. Canonical merging preserves its full matrix and scalar threshold shift.

  1. def OAI.ContinuumCoulomb.QuantumListLattice.Adjacent line 15
  2. theorem OAI.ContinuumCoulomb.QuantumListLattice.merge_adjacent line 19
  3. def OAI.ContinuumCoulomb.QuantumListLattice.source line 33
  4. theorem OAI.ContinuumCoulomb.QuantumListLattice.source_matrix line 59
  5. theorem OAI.ContinuumCoulomb.QuantumListLattice.source_energy line 67
  6. theorem OAI.ContinuumCoulomb.QuantumListLattice.source_energy_shift line 76
  7. theorem OAI.ContinuumCoulomb.QuantumListLattice.source_yes line 89
  8. theorem OAI.ContinuumCoulomb.QuantumListLattice.source_no line 102
  9. theorem OAI.ContinuumCoulomb.QuantumListLattice.source_polynomialPromise line 115