OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumSpatialRoutingTape.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The literal initial/fork program supplies the same source-center and coarse-path arrays used by the actual lattice crossing construction.

  1. def OAI.ContinuumCoulomb.QuantumSpatialRoutingTape.value line 13
  2. opaque OAI.ContinuumCoulomb.QuantumSpatialRoutingTape.program line 17
  3. theorem OAI.ContinuumCoulomb.QuantumSpatialRoutingTape.value_actual line 22