OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ContactAdjustment.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

An explicit one-variable continuation for independent contact lengths. Four sloping links share a transverse height; the other five remain axial. Thus each nine-link path is adjusted by one scalar intermediate-value solve, with fixed endpoints and no solve whose dimension grows with the lattice.

  1. def OAI.ContinuumCoulomb.contactLengthTolerance line 15
  2. def OAI.ContinuumCoulomb.contactHeightLow line 17
  3. def OAI.ContinuumCoulomb.contactHeightHigh line 18
  4. def OAI.ContinuumCoulomb.adjustedContactForward line 20
  5. def OAI.ContinuumCoulomb.adjustedContactStepX line 22
  6. def OAI.ContinuumCoulomb.adjustedContactStepY line 26
  7. def OAI.ContinuumCoulomb.adjustedContactVertex line 29
  8. def OAI.ContinuumCoulomb.adjustedContactSpan line 33
  9. theorem OAI.ContinuumCoulomb.adjustedContactForward_bound line 37

    Source documentation

    A quantitative square-root estimate, with fixed rational margins.

    theorem adjustedContactForward_bound {length c h : ℝ}
    (hl : 1 - contactLengthTolerance ≤ length) (hl' : length ≤ 1 + contactLengthTolerance)
    (hc : 7 / 10 ≤ c) (hc' : c ≤ 9 / 10) (hh : h ^ 2 = 1 - c ^ 2) :
    c - 1 / 10000 ≤ adjustedContactForward length h ∧
      adjustedContactForward length h ≤ c + 1 / 10000 := by
…

    Mentions: OAI.ContinuumCoulomb.contactLengthTolerance, OAI.ContinuumCoulomb.adjustedContactForward

  10. theorem OAI.ContinuumCoulomb.contactHeightLow_sq line 62
  11. theorem OAI.ContinuumCoulomb.contactHeightHigh_sq line 67
  12. theorem OAI.ContinuumCoulomb.contactHeight_order line 72
  13. theorem OAI.ContinuumCoulomb.adjustedContactSpan_continuous line 80
  14. theorem OAI.ContinuumCoulomb.adjustedContactSpan_low line 88

    Source documentation

    The low-height endpoint overshoots the desired unperturbed span.

    theorem adjustedContactSpan_low {c : ℝ} (hc : 3 / 4 ≤ c) (hc' : c ≤ 7 / 8)
    (lengths : ℕ → ℝ)
    (hl : ∀ k < 9, 1 - contactLengthTolerance ≤ lengths k)
    (hl' : ∀ k < 9, lengths k ≤ 1 + contactLengthTolerance) :
    5 + 4 * c + contactLengthTolerance ≤ adjustedContactSpan lengths (contactHeightLow c) := by
…

    Mentions: OAI.ContinuumCoulomb.contactLengthTolerance, OAI.ContinuumCoulomb.adjustedContactSpan, OAI.ContinuumCoulomb.contactHeightLow

  15. theorem OAI.ContinuumCoulomb.adjustedContactSpan_high line 110

    Source documentation

    The high-height endpoint undershoots the desired unperturbed span.

    theorem adjustedContactSpan_high {c : ℝ} (hc : 3 / 4 ≤ c) (hc' : c ≤ 7 / 8)
    (lengths : ℕ → ℝ)
    (hl : ∀ k < 9, 1 - contactLengthTolerance ≤ lengths k)
    (hl' : ∀ k < 9, lengths k ≤ 1 + contactLengthTolerance) :
    adjustedContactSpan lengths (contactHeightHigh c) ≤ 5 + 4 * c - contactLengthTolerance := by
…

    Mentions: OAI.ContinuumCoulomb.contactLengthTolerance, OAI.ContinuumCoulomb.adjustedContactSpan, OAI.ContinuumCoulomb.contactHeightHigh

  16. theorem OAI.ContinuumCoulomb.adjustedContactSpan_exists line 133

    Source documentation

    All nine link lengths can be prescribed independently while both endpoints remain fixed at any allowed span.

    theorem adjustedContactSpan_exists {c span : ℝ} (hc : 3 / 4 ≤ c) (hc' : c ≤ 7 / 8)
    (lengths : ℕ → ℝ)
    (hl : ∀ k < 9, 1 - contactLengthTolerance ≤ lengths k)
    (hl' : ∀ k < 9, lengths k ≤ 1 + contactLengthTolerance)
    (hspan : 5 + 4 * c - contactLengthTolerance ≤ span)
    (hspan' : span ≤ 5 + 4 * c + contactLengthTolerance) :
    ∃ h ∈ Set.Icc (contactHeightLow c) (contactHeightHigh c), adjustedContactSpan lengths h = span := by
…

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

  17. theorem OAI.ContinuumCoulomb.adjustedContactVertex_end line 145
  18. theorem OAI.ContinuumCoulomb.adjustedContact_link_length line 153

    Source documentation

    The continued path has the prescribed actual Euclidean link lengths.

    theorem adjustedContact_link_length {c h : ℝ} (hc : 3 / 4 ≤ c) (hc' : c ≤ 7 / 8)
    (hh : h ∈ Set.Icc (contactHeightLow c) (contactHeightHigh c))
    (lengths : ℕ → ℝ)
    (hl : ∀ k < 9, 1 - contactLengthTolerance ≤ lengths k) {k : ℕ} (hk : k < 9) :
    dist (adjustedContactVertex lengths h (k + 1)) (adjustedContactVertex lengths h k) = lengths k := by
…

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