OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPortChainActual.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The literal port-chain program returns precisely the sites used by the physical subdivision construction, including its two endpoint centers.

  1. theorem OAI.ContinuumCoulomb.QuantumPortChainProgram.lookup_support line 14
  2. theorem OAI.ContinuumCoulomb.QuantumPortChainProgram.point_eq line 20
  3. theorem OAI.ContinuumCoulomb.QuantumPortChainProgram.value_support line 35
  4. def OAI.ContinuumCoulomb.QuantumPortChainProgram.routed line 46
  5. opaque OAI.ContinuumCoulomb.QuantumPortChainProgram.routedProgram line 49
  6. def OAI.ContinuumCoulomb.QuantumPortChainProgram.allRouted line 53
  7. opaque OAI.ContinuumCoulomb.QuantumPortChainProgram.allRoutedProgram line 56
  8. theorem OAI.ContinuumCoulomb.QuantumPortChainProgram.allRouted_length line 71
  9. theorem OAI.ContinuumCoulomb.QuantumPortChainProgram.allRouted_get line 75
  10. theorem OAI.ContinuumCoulomb.QuantumPortChainProgram.routed_actual line 80
  11. theorem OAI.ContinuumCoulomb.QuantumPortChainProgram.routed_actual_length line 90