OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumForkRoutingData.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

A literal routing-input tape from the full fork state. Active-star bonds are retained, and each anchor is the integer midpoint of its endpoint cells.

  1. def OAI.ContinuumCoulomb.QuantumForkRoutingData.star line 14
  2. def OAI.ContinuumCoulomb.QuantumForkRoutingData.starProgram line 16
  3. def OAI.ContinuumCoulomb.QuantumForkRoutingData.starBondsProgram line 19
  4. def OAI.ContinuumCoulomb.QuantumForkRoutingData.activeProgram line 27
  5. def OAI.ContinuumCoulomb.QuantumForkRoutingData.fullProgram line 33
  6. def OAI.ContinuumCoulomb.QuantumForkRoutingData.endpoint line 37
  7. def OAI.ContinuumCoulomb.QuantumForkRoutingData.endpointProgram line 39
  8. abbrev OAI.ContinuumCoulomb.QuantumForkRoutingData.Query line 43
  9. def OAI.ContinuumCoulomb.QuantumForkRoutingData.queryCode line 44
  10. def OAI.ContinuumCoulomb.QuantumForkRoutingData.anchor line 46
  11. def OAI.ContinuumCoulomb.QuantumForkRoutingData.anchorProgram line 49
  12. def OAI.ContinuumCoulomb.QuantumForkRoutingData.value line 59
  13. def OAI.ContinuumCoulomb.QuantumForkRoutingData.program line 63
  14. theorem OAI.ContinuumCoulomb.QuantumForkRoutingData.lookup_ofFn line 76
  15. theorem OAI.ContinuumCoulomb.QuantumForkRoutingData.value_spatialModel line 80