OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumCrossingCompiled.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Full-space correctness of the computed crossing transformation, starting from an ordinary finite bond tape and its selected physical terminals.

  1. def OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.retainedGraph line 17
  2. def OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.computedLayer line 24
  3. theorem OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.packed_ofBonds line 31
  4. theorem OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.compiled_packet line 37
  5. theorem OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.retainedGraph_matrix line 60
  6. theorem OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.computedLayer_source_matrix line 71
  7. theorem OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.computedLayer_source_energy line 90
  8. theorem OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.compiled_energy_error line 93