OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumForkListDegree.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Incidence counts for the literal ordinary-bond list. The four newly emitted bonds have exactly the graph used by the physical fork degree estimate.

  1. def OAI.ContinuumCoulomb.QuantumForkList.incident line 14
  2. def OAI.ContinuumCoulomb.QuantumForkList.degree line 16
  3. theorem OAI.ContinuumCoulomb.QuantumForkList.graph_degree_incident line 19
  4. theorem OAI.ContinuumCoulomb.QuantumForkList.degree_append line 27
  5. theorem OAI.ContinuumCoulomb.QuantumForkList.degree_eq_graph line 31
  6. theorem OAI.ContinuumCoulomb.QuantumForkList.added_sum line 40
  7. theorem OAI.ContinuumCoulomb.QuantumForkList.next_ordinary_degree line 56
  8. structure OAI.ContinuumCoulomb.QuantumForkList.DegreeBounds line 77