OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumSpatialSlotProgram.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The actual fine-grid positions and lane colors of the ordinal-slot model are computed directly from encoded lists of cells.

  1. def OAI.ContinuumCoulomb.QuantumSpatialSlotProgram.fineSite line 14
  2. def OAI.ContinuumCoulomb.QuantumSpatialSlotProgram.lane line 18
  3. def OAI.ContinuumCoulomb.QuantumSpatialSlotProgram.cellProgram line 22
  4. def OAI.ContinuumCoulomb.QuantumSpatialSlotProgram.fineSiteProgram line 28
  5. def OAI.ContinuumCoulomb.QuantumSpatialSlotProgram.laneProgram line 37
  6. theorem OAI.ContinuumCoulomb.QuantumSpatialSlotProgram.colorEquiv_val line 51
  7. theorem OAI.ContinuumCoulomb.QuantumSpatialSlotProgram.fineSite_actual line 55
  8. theorem OAI.ContinuumCoulomb.QuantumSpatialSlotProgram.lane_actual line 63