pith. machine review for the scientific record. sign in
theorem proved tactic proof

Jtilde_zero_iff

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 110theorem Jtilde_zero_iff {lam : ℝ} (hlam : lam ≠ 0) (δ : ℝ) :
 111    Jtilde lam δ = 0 ↔ ∃ n : ℤ, δ = ↑n := by

proof body

Tactic-mode proof.

 112  unfold Jtilde
 113  constructor
 114  · intro h
 115    have h1 : cosh (lam * distZ δ) = 1 := by linarith
 116    have h2 : lam * distZ δ = 0 := (cosh_eq_one_iff _).mp h1
 117    have h3 : distZ δ = 0 := by
 118      rcases mul_eq_zero.mp h2 with h | h
 119      · exact absurd h hlam
 120      · exact h
 121    exact (distZ_eq_zero_iff δ).mp h3
 122  · intro ⟨n, hn⟩
 123    have hd : distZ δ = 0 := (distZ_eq_zero_iff δ).mpr ⟨n, hn⟩
 124    simp [hd, cosh_zero]
 125
 126/-! ### Stiffness (small-gradient regime)
 127
 128For small δ (near an integer), J̃(lam, δ) ≈ lam² δ² / 2.
 129The stiffness is κ = lam²/2. -/
 130
 131/-- Small-gradient lower bound: J̃(lam, δ) ≥ (lam · d_ℤ(δ))² / 2.
 132    This follows from the quadratic lower bound cosh(t) − 1 ≥ t²/2. -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (12)

Lean names referenced from this declaration's body.