OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ContactGadgets.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The two signed-edge contact gadgets. Each has twenty sites, nineteen links, fixed original endpoints, and independently prescribed link lengths. A negative input sign places the central partner off the backbone.

  1. abbrev OAI.ContinuumCoulomb.ContactGadgetSite line 12
  2. def OAI.ContinuumCoulomb.contactGadgetSlope line 14
  3. def OAI.ContinuumCoulomb.contactGadgetSpan line 16
  4. def OAI.ContinuumCoulomb.contactGadgetRightOrigin line 19
  5. def OAI.ContinuumCoulomb.contactGadgetSide line 22
  6. def OAI.ContinuumCoulomb.contactGadgetRightNode line 24
  7. def OAI.ContinuumCoulomb.contactGadgetPosition line 29
  8. theorem OAI.ContinuumCoulomb.contactGadgetSlope_bounds line 38
  9. theorem OAI.ContinuumCoulomb.contactGadgetSpan_bounds line 42
  10. theorem OAI.ContinuumCoulomb.contactGadgetRightNode_position line 51
  11. theorem OAI.ContinuumCoulomb.contactGadget_link_lengths line 76

    Source documentation

    Every physical link has its independently prescribed length.

    theorem contactGadget_link_lengths (negative : Bool) {central : ℝ}
    (hc : 1 - contactLengthTolerance ≤ central)
    (leftLengths rightLengths : ℕ → ℝ)
    (hl : ∀ k < 9, 1 - contactLengthTolerance ≤ leftLengths k)
    (hr : ∀ k < 9, 1 - contactLengthTolerance ≤ rightLengths k)
    {leftHeight rightHeight : ℝ}
    (hleftHeight : leftHeight ∈ Set.Icc (contactHeightLow (contactGadgetSlope negative))
      (contactHeightHigh (contactGadgetSlope negative)))
    (hrightHeight : rightHeight ∈ Set.Icc (contactHeightLow (contactGadgetSlope negative))
      (contactHeightHigh (contactGadgetSlope negative)))
    (hleft : adjustedContactSpan leftLengths leftHeight = contactGadgetSpan negative central) :
    (∀ k : Fin 9,
…

    Mentions: OAI.ContinuumCoulomb.contactLengthTolerance, OAI.ContinuumCoulomb.contactHeightLow, OAI.ContinuumCoulomb.contactGadgetSlope, OAI.ContinuumCoulomb.contactHeightHigh, OAI.ContinuumCoulomb.adjustedContactSpan, OAI.ContinuumCoulomb.contactGadgetSpan

  12. theorem OAI.ContinuumCoulomb.contactGadget_independent_lengths line 127

    Source documentation

    Independent implementation of all nineteen links with the two original vertices fixed. No dimensional parameter of a larger lattice enters.

    theorem contactGadget_independent_lengths (negative : Bool) {central : ℝ}
    (hc : 1 - contactLengthTolerance ≤ central) (hc' : central ≤ 1 + contactLengthTolerance)
    (leftLengths rightLengths : ℕ → ℝ)
    (hl : ∀ k < 9, 1 - contactLengthTolerance ≤ leftLengths k)
    (hl' : ∀ k < 9, leftLengths k ≤ 1 + contactLengthTolerance)
    (hr : ∀ k < 9, 1 - contactLengthTolerance ≤ rightLengths k)
    (hr' : ∀ k < 9, rightLengths k ≤ 1 + contactLengthTolerance) :
    ∃ leftHeight rightHeight,
      leftHeight ∈ Set.Icc (contactHeightLow (contactGadgetSlope negative))
        (contactHeightHigh (contactGadgetSlope negative)) ∧
      rightHeight ∈ Set.Icc (contactHeightLow (contactGadgetSlope negative))
        (contactHeightHigh (contactGadgetSlope negative)) ∧
…

    Mentions: OAI.ContinuumCoulomb.contactLengthTolerance, OAI.ContinuumCoulomb.contactHeightLow, OAI.ContinuumCoulomb.contactGadgetSlope, OAI.ContinuumCoulomb.contactHeightHigh