OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumForkDegrees.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

The parallel fork graph halves the degree of its center.

  1. def OAI.ContinuumCoulomb.qmaForkPortEquiv line 11
  2. abbrev OAI.ContinuumCoulomb.QMAForkStarVertex line 15
  3. abbrev OAI.ContinuumCoulomb.QMAForkStarEdge line 16
  4. def OAI.ContinuumCoulomb.qmaForkStarLeft line 19
  5. def OAI.ContinuumCoulomb.qmaForkStarRight line 26
  6. def OAI.ContinuumCoulomb.qmaForkStarDegree line 33
  7. theorem OAI.ContinuumCoulomb.qmaForkStar_center_degree line 36
  8. theorem OAI.ContinuumCoulomb.qmaForkStar_center_decreases line 39
  9. theorem OAI.ContinuumCoulomb.qmaForkStar_no_loops line 44
  10. theorem OAI.ContinuumCoulomb.qmaForkStar_new_degree line 59
  11. theorem OAI.ContinuumCoulomb.qmaForkStar_paired_degree line 65
  12. theorem OAI.ContinuumCoulomb.qmaForkStar_leftover_degree line 70
  13. theorem OAI.ContinuumCoulomb.qmaForkStar_noncenter_degree line 74
  14. theorem OAI.ContinuumCoulomb.qmaForkStar_vertex_count line 87
  15. theorem OAI.ContinuumCoulomb.qmaForkStar_edge_count line 92
  16. def OAI.ContinuumCoulomb.qmaForkDegreeAfter line 98

    Source documentation

    A constant degree bound permits a constant number of fork rounds.

    def qmaForkDegreeAfter (d : ℕ) : ℕ → ℕ
  | 0 => d
  | k+1 => qmaForkDegreeAfter d k / 2 + qmaForkDegreeAfter d k % 2
  17. theorem OAI.ContinuumCoulomb.qmaForkDegreeAfter_bound line 102
  18. theorem OAI.ContinuumCoulomb.qmaForkDegreeAfter_constant line 115