OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumSpatialPortMatching.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact geometric matching for the actual spatial compiler. Its position tape is a permutation of the canonical completed port graph.

  1. theorem OAI.ContinuumCoulomb.QuantumSpatialPortProgram.port_layout_matches line 14
  2. theorem OAI.ContinuumCoulomb.QuantumSpatialPortProgram.value_matches line 36