OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumRouteLanes.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Distinct residue lanes separate parallel routes and keep crossings away from bends.

  1. def OAI.ContinuumCoulomb.qmaLanePoint line 9
  2. theorem OAI.ContinuumCoulomb.qmaLanePoint_row_mod line 12
  3. theorem OAI.ContinuumCoulomb.qmaLanePoint_col_mod line 16
  4. theorem OAI.ContinuumCoulomb.qmaLanePoint_eq_color line 20
  5. theorem OAI.ContinuumCoulomb.qmaLanePoint_injective line 26
  6. def OAI.ContinuumCoulomb.qmaHorizontalLane line 36
  7. def OAI.ContinuumCoulomb.qmaVerticalLane line 39
  8. theorem OAI.ContinuumCoulomb.qmaHorizontalLane_color line 42
  9. theorem OAI.ContinuumCoulomb.qmaVerticalLane_color line 48
  10. theorem OAI.ContinuumCoulomb.qmaLane_crossing_not_vertex line 55

    Source documentation

    A transverse crossing between distinct lanes cannot coincide with any lane vertex.

    theorem qmaLane_crossing_not_vertex {C : ℕ} {c d : Fin C} (hcd : c ≠ d)
    {x y : ℕ} {p : ℕ × ℕ} (hh : qmaHorizontalLane c y p) (hv : qmaVerticalLane d x p)
    (e : Fin C) (q : ℕ × ℕ) : p ≠ qmaLanePoint e q := by
…

    Mentions: OAI.ContinuumCoulomb.qmaHorizontalLane, OAI.ContinuumCoulomb.qmaVerticalLane, OAI.ContinuumCoulomb.qmaLanePoint