OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumCrossingListFamily.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

A literal simultaneous crossing layer: nine bonds and two fresh spins per crossing, with every scalar correction retained.

  1. abbrev OAI.ContinuumCoulomb.QuantumCrossingListBlock.FamilyInput line 12
  2. def OAI.ContinuumCoulomb.QuantumCrossingListBlock.familyCode line 13
  3. def OAI.ContinuumCoulomb.QuantumCrossingListBlock.zeroCrossing line 14
  4. def OAI.ContinuumCoulomb.QuantumCrossingListBlock.indexed line 15
  5. def OAI.ContinuumCoulomb.QuantumCrossingListBlock.family line 17
  6. def OAI.ContinuumCoulomb.QuantumCrossingListBlock.offset line 19
  7. def OAI.ContinuumCoulomb.QuantumCrossingListBlock.familyOffset line 20
  8. opaque OAI.ContinuumCoulomb.QuantumCrossingListBlock.indexedProgram line 22
  9. opaque OAI.ContinuumCoulomb.QuantumCrossingListBlock.familyProgram line 29
  10. opaque OAI.ContinuumCoulomb.QuantumCrossingListBlock.offsetProgram line 35
  11. opaque OAI.ContinuumCoulomb.QuantumCrossingListBlock.familyOffsetProgram line 36
  12. theorem OAI.ContinuumCoulomb.QuantumCrossingListBlock.family_length line 44
  13. theorem OAI.ContinuumCoulomb.QuantumCrossingListBlock.indexed_mem line 49
  14. theorem OAI.ContinuumCoulomb.QuantumCrossingListBlock.family_bounded line 55
  15. theorem OAI.ContinuumCoulomb.QuantumCrossingListBlock.family_noLoops line 65