OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumSpatialPlanarRealization.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Every actual degree-three spatial exchange model has a nearest-neighbor square-lattice realization. The number of layers and the size factor depend only on its fixed spatial-density constants.

  1. theorem OAI.ContinuumCoulomb.QMASpatialExchangeModel.placedVertex_positive line 18
  2. theorem OAI.ContinuumCoulomb.QMASpatialExchangeModel.planar_realize line 24