OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumForkListMatrix.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The four literal bonds emitted for one port pair are exactly its correction, singlet penalty and two outer couplings in the fork Hamiltonian.

  1. def OAI.ContinuumCoulomb.QuantumForkList.typedPairBonds line 13
  2. theorem OAI.ContinuumCoulomb.QuantumForkList.pairBonds_eq line 20
  3. theorem OAI.ContinuumCoulomb.QuantumForkList.pairBonds_matrix line 26