theorem
proved
phase_rigidity
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Papers.GCIC.ReducedPhasePotential on GitHub at line 155.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
152/-- **RESULT 3 (Phase Rigidity).**
153On a connected graph, if the reduced phase cost J̃(lam, Θ_v − Θ_w) vanishes on
154every edge, then the phase field Θ is constant modulo integers. -/
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
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