OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ContactBaseSeparation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The exact nineteen-link base gadget and all of its nonlink separations.

  1. def OAI.ContinuumCoulomb.contactBaseGadgetPosition line 12
  2. def OAI.ContinuumCoulomb.contactGadgetLinked line 18
  3. theorem OAI.ContinuumCoulomb.contactPath_second_axial_lower line 29
  4. theorem OAI.ContinuumCoulomb.contact_axial_separation line 38
  5. theorem OAI.ContinuumCoulomb.contactBase_left_left_separation line 42
  6. theorem OAI.ContinuumCoulomb.contactBase_left_right_separation line 57
  7. theorem OAI.ContinuumCoulomb.contactBase_side_left_separation line 96
  8. theorem OAI.ContinuumCoulomb.contactBase_side_right_separation line 133
  9. theorem OAI.ContinuumCoulomb.contactBaseGadget_nonlink_separation line 169

    Source documentation

    Every distinct nonlinked pair in either actual base gadget is at least1.4 apart, including the negative-sign side site.

    theorem contactBaseGadget_nonlink_separation (negative : Bool) (x y : ContactGadgetSite)
    (hne : x ≠ y) (hlink : ¬ contactGadgetLinked negative x y) :
    7 / 5 ≤ dist (contactBaseGadgetPosition negative x) (contactBaseGadgetPosition negative y) := by
…

    Mentions: OAI.ContinuumCoulomb.ContactGadgetSite, OAI.ContinuumCoulomb.contactGadgetLinked, OAI.ContinuumCoulomb.contactBaseGadgetPosition