OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumForkListActive.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exact active-star matrices of the ordered compiler state. The pairing identity applies to every matrix entry, including the retained odd port.

  1. def OAI.ContinuumCoulomb.QuantumForkList.starBonds line 13
  2. def OAI.ContinuumCoulomb.QuantumForkList.activeBonds line 16
  3. def OAI.ContinuumCoulomb.QuantumForkList.unpairedBonds line 19
  4. def OAI.ContinuumCoulomb.QuantumForkList.pairedBonds line 22
  5. theorem OAI.ContinuumCoulomb.QuantumForkList.catalog_sum line 25
  6. theorem OAI.ContinuumCoulomb.QuantumForkList.active_pairing line 31
  7. def OAI.ContinuumCoulomb.QuantumForkList.matrix line 54
  8. theorem OAI.ContinuumCoulomb.QuantumForkList.matrix_pairing line 56