OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ContactPathBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Coordinate bounds for the two explicit paths. These imply the fixed strip conditions used to separate gadgets throughout an arbitrarily large lattice.

  1. theorem OAI.ContinuumCoulomb.contactSlopeHeight_bounds line 12
  2. theorem OAI.ContinuumCoulomb.contactPath_transverse_bounds line 18
  3. theorem OAI.ContinuumCoulomb.contactPath_axial_bounds line 25
  4. theorem OAI.ContinuumCoulomb.contactPath_internal_axial_bounds line 31
  5. theorem OAI.ContinuumCoulomb.contactPath_off_axis_bounds line 37
  6. def OAI.ContinuumCoulomb.leftContactStripSite line 46

    Source documentation

    Left-path internal sites and its central endpoint satisfy the common length-17 strip bounds.

    def leftContactStripSite (c : ℝ) (hc : 3 / 4 ≤ c) (hc' : c ≤ 7 / 8)
    (k : ℕ) (hk : 1 ≤ k) (hk' : k ≤ 9) : ContactStripSite where
…

    Mentions: OAI.ContinuumCoulomb.ContactStripSite

  7. def OAI.ContinuumCoulomb.rightContactStripSite line 63

    Source documentation

    Right-path internal sites use an origin chosen so their far endpoint is17.

    def rightContactStripSite (c origin : ℝ) (hc : 3 / 4 ≤ c) (hc' : c ≤ 7 / 8)
    (horigin : origin + (5 + 4 * c) = 17)
    (k : ℕ) (hk : 1 ≤ k) (hk' : k ≤ 8) : ContactStripSite where
…

    Mentions: OAI.ContinuumCoulomb.ContactStripSite