OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumCrossingListLayer.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

The complete rational crossing transformation, including its calibrated scale, retained edges, mediator pairs and exact scalar shift.

  1. abbrev OAI.ContinuumCoulomb.QuantumCrossingListLayer.Input line 15
  2. def OAI.ContinuumCoulomb.QuantumCrossingListLayer.inputCode line 16
  3. def OAI.ContinuumCoulomb.QuantumCrossingListLayer.scaleInput line 19
  4. def OAI.ContinuumCoulomb.QuantumCrossingListLayer.parameters line 21
  5. def OAI.ContinuumCoulomb.QuantumCrossingListLayer.familyInput line 22
  6. def OAI.ContinuumCoulomb.QuantumCrossingListLayer.count line 23
  7. def OAI.ContinuumCoulomb.QuantumCrossingListLayer.bonds line 24
  8. def OAI.ContinuumCoulomb.QuantumCrossingListLayer.constant line 25
  9. def OAI.ContinuumCoulomb.QuantumCrossingListLayer.value line 26
  10. opaque OAI.ContinuumCoulomb.QuantumCrossingListLayer.packetProgram line 28
  11. opaque OAI.ContinuumCoulomb.QuantumCrossingListLayer.nProgram line 32
  12. opaque OAI.ContinuumCoulomb.QuantumCrossingListLayer.oldProgram line 34
  13. opaque OAI.ContinuumCoulomb.QuantumCrossingListLayer.oldBondsProgram line 37
  14. opaque OAI.ContinuumCoulomb.QuantumCrossingListLayer.oldConstantProgram line 40
  15. opaque OAI.ContinuumCoulomb.QuantumCrossingListLayer.crossingProgram line 43
  16. opaque OAI.ContinuumCoulomb.QuantumCrossingListLayer.scaleInputProgram line 45
  17. opaque OAI.ContinuumCoulomb.QuantumCrossingListLayer.parametersProgram line 53
  18. opaque OAI.ContinuumCoulomb.QuantumCrossingListLayer.familyInputProgram line 55
  19. opaque OAI.ContinuumCoulomb.QuantumCrossingListLayer.countProgram line 57
  20. opaque OAI.ContinuumCoulomb.QuantumCrossingListLayer.bondsProgram line 61
  21. opaque OAI.ContinuumCoulomb.QuantumCrossingListLayer.constantProgram line 64
  22. opaque OAI.ContinuumCoulomb.QuantumCrossingListLayer.program line 67
  23. theorem OAI.ContinuumCoulomb.QuantumCrossingListLayer.bonds_bounded line 70
  24. theorem OAI.ContinuumCoulomb.QuantumCrossingListLayer.bonds_noLoops line 80
  25. def OAI.ContinuumCoulomb.QuantumCrossingListLayer.graph line 90