OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumEndpointListProgram.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The endpoint arm list is computed from its ordinal port, lane color and coarse vertex. All three quantities are supplied by the explicit slot and incident-rank programs.

  1. abbrev OAI.ContinuumCoulomb.QuantumEndpointListProgram.ArmInput line 15
  2. def OAI.ContinuumCoulomb.QuantumEndpointListProgram.armCode line 16
  3. def OAI.ContinuumCoulomb.QuantumEndpointListProgram.armList line 18
  4. theorem OAI.ContinuumCoulomb.QuantumEndpointListProgram.armList_fin line 26
  5. def OAI.ContinuumCoulomb.QuantumEndpointListProgram.armProgram line 31
  6. def OAI.ContinuumCoulomb.QuantumEndpointListProgram.translate line 41
  7. def OAI.ContinuumCoulomb.QuantumEndpointListProgram.translateProgram line 43
  8. abbrev OAI.ContinuumCoulomb.QuantumEndpointListProgram.Input line 57
  9. def OAI.ContinuumCoulomb.QuantumEndpointListProgram.inputCode line 58
  10. def OAI.ContinuumCoulomb.QuantumEndpointListProgram.value line 59
  11. def OAI.ContinuumCoulomb.QuantumEndpointListProgram.program line 61
  12. theorem OAI.ContinuumCoulomb.QuantumEndpointListProgram.value_actual line 66