theorem
proved
gcic_one_statement
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.GlobalCoIdentityConstraint on GitHub at line 305.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
302 edge-wise zero reduced phase cost at any nonzero base `lam`, every
303 pair of vertices has the same wrapped phase modulo 1, and there
304 exists a single `Θ_global ∈ [0, 1)` shared by all vertices. -/
305theorem gcic_one_statement
306 {adj : V → V → Prop}
307 (hconn : ∀ u v : V, Relation.ReflTransGen adj u v)
308 {lam : ℝ} (hlam : lam ≠ 0)
309 {Θ : V → ℝ}
310 (hzero : ∀ v w, adj v w → Jtilde lam (Θ v - Θ w) = 0) :
311 -- (1) Pairwise wrapped-phase equality.
312 (∀ v w : V, wrapPhase (Θ v) = wrapPhase (Θ w)) ∧
313 -- (2) Wrapped phase lands in [0, 1).
314 (∀ v : V, 0 ≤ wrapPhase (Θ v) ∧ wrapPhase (Θ v) < 1) := by
315 refine ⟨gcic_global_phase_unique hconn hlam hzero, ?_⟩
316 intro v
317 exact wrapPhase_bounds (Θ v)
318
319end
320
321end GlobalCoIdentityConstraint
322end Foundation
323end IndisputableMonolith