PlanarCalibration.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Endpoint brackets and an actual contact-hopping calibration. Quantitative scale selection and the polynomial-time numerical implementation remain separate steps; no calibration output is assumed.

theorem OAI.ContinuumCoulomb.planarHopping_short_scaled line 13
theorem OAI.ContinuumCoulomb.planarHopping_long_scaled line 27

theorem OAI.ContinuumCoulomb.planarHopping_contact_calibration line 45

Source documentation

The paper's actual hopping profile attains the distance-dependent superexchange target inside the permitted contact-length interval. Only continuity of the direct Coulomb profile and the explicit endpoint numerical brackets remain as premises here.

theorem planarHopping_contact_calibration {D ε τ K U : ℝ} (v : ℝ → ℝ)
    (hD : 0 ≤ D) (hε : 0 ≤ ε) (hd : 2 ≤ (1 - ε) * D)
    (hv : ContinuousOn v (Set.Icc ((1 - ε) * D) ((1 + ε) * D)))
    (hshort : τ * Real.sqrt (K * (U - v ((1 - ε) * D))) ≤
      planarHoppingLowerConstant / ((1 - ε) * D + 3) * Real.exp (ε * D))
    (hlong : planarHoppingUpperConstant * ((1 + ε) * D + 1) * Real.exp (-ε * D) ≤
      τ * Real.sqrt (K * (U - v ((1 + ε) * D)))) :
    ∃ d ∈ Set.Icc ((1 - ε) * D) ((1 + ε) * D),
      Real.exp D * planarHopping d = τ * Real.sqrt (K * (U - v d)) := by
…

Mentions: OAI.ContinuumCoulomb.planarHoppingLowerConstant, OAI.ContinuumCoulomb.planarHoppingUpperConstant, OAI.ContinuumCoulomb.planarHopping