OAI/MathematicalPhysics/ContinuumCoulomb/Reduction/SourceBondLists.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Complete matrix semantics for the literal bond registers. Removing zero terms preserves the actual Hamiltonian, while valid bounded indices give the exact finite family used in the mediator comparison.

  1. def OAI.ContinuumCoulomb.SourceBondLists.bondMatrix line 15
  2. def OAI.ContinuumCoulomb.SourceBondLists.matrix line 19
  3. theorem OAI.ContinuumCoulomb.SourceBondLists.bondMatrix_zero line 22
  4. theorem OAI.ContinuumCoulomb.SourceBondLists.filter_matrix line 26
  5. def OAI.ContinuumCoulomb.SourceBondLists.bounded line 41
  6. def OAI.ContinuumCoulomb.SourceBondLists.bonds line 43
  7. theorem OAI.ContinuumCoulomb.SourceBondLists.matrix_bonds line 48
  8. theorem OAI.ContinuumCoulomb.SourceBondLists.filter_bounded line 59
  9. theorem OAI.ContinuumCoulomb.SourceBondLists.bonds_noLoops line 64