OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumRawCellDensity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The literal four-spin vertex numbers have exactly four copies of each logical cell. This connects the emitted numeric list to bounded cell density.

  1. def OAI.ContinuumCoulomb.QuantumRawCellLocality.extendCell line 14
  2. theorem OAI.ContinuumCoulomb.QuantumRawCellLocality.extendCell_fin line 18
  3. theorem OAI.ContinuumCoulomb.QuantumRawCellLocality.blockCell_fin line 22
  4. theorem OAI.ContinuumCoulomb.QuantumRawCellLocality.blockCell_density line 30