Jtilde_zero_iff

formal source

 107  · intro h; rw [h, cosh_zero]
 108
 109/-- J̃(lam, δ) = 0 iff δ is an integer, for lam ≠ 0. -/
 110theorem Jtilde_zero_iff {lam : ℝ} (hlam : lam ≠ 0) (δ : ℝ) :
 111    Jtilde lam δ = 0 ↔ ∃ n : ℤ, δ = ↑n := by
 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. -/
 133theorem Jtilde_stiffness_lb (lam : ℝ) (δ : ℝ) :
 134    (lam * distZ δ) ^ 2 / 2 ≤ Jtilde lam δ := by
 135  unfold Jtilde
 136  linarith [cosh_quadratic_lower_bound (lam * distZ δ)]
 137
 138/-- The GCIC stiffness for base φ: κ = (ln φ)²/2. -/
 139noncomputable def gcic_kappa : ℝ := (log Constants.phi) ^ 2 / 2
 140