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

gcic_one_statement

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)

 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

proof body

Term-mode proof.

 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

depends on (9)

Lean names referenced from this declaration's body.