GlobalCoIdentityConstraintCert

formal source

 261    3. The global GCIC theorem holds at any nonzero base.
 262    4. There exists a single `Θ_global ∈ [0, 1)` shared by every vertex.
 263    5. The global phase is independent of basepoint. -/
 264structure GlobalCoIdentityConstraintCert (V : Type*) [Inhabited V] where
 265  wrap_in_unit_interval : ∀ x : ℝ, 0 ≤ wrapPhase x ∧ wrapPhase x < 1
 266  wrap_invariant_under_int : ∀ (x : ℝ) (n : ℤ),
 267    wrapPhase (x + (n : ℝ)) = wrapPhase x
 268  gcic_global_unique :
 269    ∀ {adj : V → V → Prop} (_hconn : ∀ u v : V, Relation.ReflTransGen adj u v)
 270      {lam : ℝ} (_hlam : lam ≠ 0) {Θ : V → ℝ}
 271      (_hzero : ∀ v w, adj v w → Jtilde lam (Θ v - Θ w) = 0)
 272      (v w : V), wrapPhase (Θ v) = wrapPhase (Θ w)
 273  gcic_global_existence :
 274    ∀ {adj : V → V → Prop} (_hconn : ∀ u v : V, Relation.ReflTransGen adj u v)
 275      {lam : ℝ} (_hlam : lam ≠ 0) {Θ : V → ℝ}
 276      (_hzero : ∀ v w, adj v w → Jtilde lam (Θ v - Θ w) = 0),
 277      ∃ Θ_global : ℝ,
 278        (0 ≤ Θ_global ∧ Θ_global < 1) ∧
 279        (∀ v : V, wrapPhase (Θ v) = Θ_global)
 280  gcic_basepoint_independent :
 281    ∀ {adj : V → V → Prop} (_hconn : ∀ u v : V, Relation.ReflTransGen adj u v)
 282      {lam : ℝ} (_hlam : lam ≠ 0) {Θ : V → ℝ}
 283      (_hzero : ∀ v w, adj v w → Jtilde lam (Θ v - Θ w) = 0)
 284      (b1 b2 : V), wrapPhase (Θ b1) = wrapPhase (Θ b2)
 285
 286/-- The master certificate is inhabited for any `Inhabited V`. -/
 287def gcicCert (V : Type*) [Inhabited V] : GlobalCoIdentityConstraintCert V where
 288  wrap_in_unit_interval := wrapPhase_bounds
 289  wrap_invariant_under_int := wrapPhase_add_int
 290  gcic_global_unique := @fun _adj hconn _lam hlam _Θ hzero v w =>
 291    gcic_global_phase_unique hconn hlam hzero v w
 292  gcic_global_existence := @fun _adj hconn _lam hlam _Θ hzero =>
 293    gcic_existence_of_global_phase hconn hlam hzero
 294  gcic_basepoint_independent := @fun _adj hconn _lam hlam _Θ hzero b1 b2 =>