OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ContactGadgetStability.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The prescribed nineteen-link gadgets retain the nonlink separation of the base shapes. All estimates concern the actual coordinate constructions.

  1. theorem OAI.ContinuumCoulomb.contactPoint_axis_dist line 11
  2. theorem OAI.ContinuumCoulomb.contactPoint_vertical_dist line 17
  3. theorem OAI.ContinuumCoulomb.contactGadgetOrigin_near line 23
  4. theorem OAI.ContinuumCoulomb.contactGadgetPosition_near line 36

    Source documentation

    The complete actual gadget, including the central partner, stays inside the same fixed separation guard as the independently adjusted paths.

    theorem contactGadgetPosition_near (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 : ℝ}
    (hleftHeight : leftHeight ∈ Set.Icc (contactHeightLow (contactGadgetSlope negative))
      (contactHeightHigh (contactGadgetSlope negative)))
    (hrightHeight : rightHeight ∈ Set.Icc (contactHeightLow (contactGadgetSlope negative))
      (contactHeightHigh (contactGadgetSlope negative))) (x : ContactGadgetSite) :
…

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

  5. theorem OAI.ContinuumCoulomb.contactGadget_nonlink_separation line 79

    Source documentation

    The actual variable-link gadget retains distance greater than1.2 for every distinct pair which is not one of its nineteen links.

    theorem contactGadget_nonlink_separation (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 : ℝ}
    (hleftHeight : leftHeight ∈ Set.Icc (contactHeightLow (contactGadgetSlope negative))
      (contactHeightHigh (contactGadgetSlope negative)))
    (hrightHeight : rightHeight ∈ Set.Icc (contactHeightLow (contactGadgetSlope negative))
      (contactHeightHigh (contactGadgetSlope negative)))
…

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