OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumForkListRealization.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Exact correspondence between the emitted ordered state and the finite parallel-fork Hamiltonian. The mediator numbering is the proved prefix index.

  1. theorem OAI.ContinuumCoulomb.QuantumForkList.retained_graph_list line 13
  2. theorem OAI.ContinuumCoulomb.QuantumForkList.packet_graph_list line 23
  3. theorem OAI.ContinuumCoulomb.QuantumForkList.graph_bonds_eq line 36
  4. theorem OAI.ContinuumCoulomb.QuantumForkList.next_constant line 45
  5. def OAI.ContinuumCoulomb.QuantumForkList.rawBottom line 54
  6. theorem OAI.ContinuumCoulomb.QuantumForkList.next_bottom_graph line 57