OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumForkListCellMass.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A literal fork round has bounded density in the original coarse cells. The proof counts its actual fresh indices through the ordered pair catalog.

  1. theorem OAI.ContinuumCoulomb.QuantumForkList.next_cell_mass line 15
  2. theorem OAI.ContinuumCoulomb.QuantumForkList.pair_cell_mass_le line 39
  3. theorem OAI.ContinuumCoulomb.QuantumForkList.prefix_cell_mass_le line 57
  4. theorem OAI.ContinuumCoulomb.QuantumForkList.next_cell_mass_le line 70
  5. theorem OAI.ContinuumCoulomb.QuantumForkList.iterate_group_le line 85
  6. theorem OAI.ContinuumCoulomb.QuantumForkList.iterate_cell_mass_le line 93