OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumListPathMatrix.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Matrix semantics of the literal path-subdivision block. Its fresh labels are exactly the two ordinary-spin labels in the singlet gadget.

  1. def OAI.ContinuumCoulomb.QuantumListPathProgram.physicalLeft line 13
  2. def OAI.ContinuumCoulomb.QuantumListPathProgram.physicalRight line 16
  3. theorem OAI.ContinuumCoulomb.QuantumListPathProgram.old_value line 19
  4. theorem OAI.ContinuumCoulomb.QuantumListPathProgram.fresh_value line 21
  5. theorem OAI.ContinuumCoulomb.QuantumListPathProgram.bond_eq line 26
  6. theorem OAI.ContinuumCoulomb.QuantumListPathProgram.block_matrix line 34
  7. theorem OAI.ContinuumCoulomb.QuantumListPathProgram.offset_cast line 44
  8. theorem OAI.ContinuumCoulomb.QuantumListPathProgram.indexed_ofFn line 48
  9. theorem OAI.ContinuumCoulomb.QuantumListPathProgram.family_ofFn line 55
  10. theorem OAI.ContinuumCoulomb.QuantumListPathProgram.matrix_flatten line 68
  11. theorem OAI.ContinuumCoulomb.QuantumListPathProgram.family_matrix line 74
  12. theorem OAI.ContinuumCoulomb.QuantumListPathProgram.physical_sum line 84
  13. theorem OAI.ContinuumCoulomb.QuantumListPathProgram.familyOffset_cast line 98
  14. theorem OAI.ContinuumCoulomb.QuantumListPathProgram.matrix_ofFn line 116
  15. theorem OAI.ContinuumCoulomb.QuantumListPathProgram.retained_matrix line 124
  16. theorem OAI.ContinuumCoulomb.QuantumListPathProgram.fixed_step_matrix line 130