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

phase_rigidity

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)

 155theorem phase_rigidity {V : Type*} {adj : V → V → Prop}
 156    (hconn : ∀ u v : V, Relation.ReflTransGen adj u v)
 157    {lam : ℝ} (hlam : lam ≠ 0) {Θ : V → ℝ}
 158    (hzero : ∀ v w, adj v w → Jtilde lam (Θ v - Θ w) = 0) :
 159    ∀ v w : V, ∃ n : ℤ, Θ v - Θ w = ↑n := by

proof body

Term-mode proof.

 160  have hadj : ∀ v w, adj v w → ∃ n : ℤ, Θ v - Θ w = ↑n :=
 161    fun v w hvw => (Jtilde_zero_iff hlam _).mp (hzero v w hvw)
 162  intro v w
 163  induction hconn v w with
 164  | refl => exact ⟨0, by simp⟩
 165  | tail _ hbc ih =>
 166    obtain ⟨n₁, hn₁⟩ := ih
 167    obtain ⟨n₂, hn₂⟩ := hadj _ _ hbc
 168    exact ⟨n₁ + n₂, by push_cast; linarith⟩
 169
 170end IndisputableMonolith.Papers.GCIC.ReducedPhasePotential

used by (2)

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

depends on (5)

Lean names referenced from this declaration's body.