OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumForkListInitialRealization.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Reordering the actual initial bond list gives exactly the typed physical singlet Hamiltonian, including its scalar offset.

  1. def OAI.ContinuumCoulomb.QuantumForkList.initialSourceBonds line 13
  2. theorem OAI.ContinuumCoulomb.QuantumForkList.initialPhysical_sum line 17
  3. theorem OAI.ContinuumCoulomb.QuantumForkList.initialSource_sum line 28
  4. theorem OAI.ContinuumCoulomb.QuantumForkList.initial_constant_eq line 38
  5. theorem OAI.ContinuumCoulomb.QuantumForkList.initial_bottom_physical line 51