Reaching an attachment vertex through two connector paths

ScriptGluing records only the principal-divisor identities needed to insert factor scripts into an ambient graph. The first connector has an arbitrary convex integral path potential; the second connector is constant. This avoids requiring an isomorphism to a separately constructed path-join graph.

structure Utilities.TwoPole.ScriptGluing (A : CFGraph) (B : CFGraph) (G : CFGraph) (p : TwoPole A) (q : TwoPole B) (L : ℕ) : Type (max (max u v) w)

The script-level interface for two factors joined by two paths. Only the first path length is needed: the second path always has constant potential.

• left : A.V → G.V

  The injective placement of the left graph's vertices into the graph carrying the glued firing script.

• right : B.V → G.V

  The injective placement of the right graph's vertices, with image disjoint from the left placement.

• left_injective : Function.Injective self.left
• right_injective : Function.Injective self.right
• disjoint (a : A.V) (b : B.V) : self.left a ≠ self.right b
• length_pos : 0 < L
• glue (f : firingScript A) (g : firingScript B) (h : ℕ → ℤ) : h 0 = f p.first → h L = g q.first → f p.second = g q.second → (∀ (j : ℕ), 0 < j → j < L → 0 ≤ h (j - 1) - 2 * h j + h (j + 1)) → ∃ (σ : firingScript G), (∀ (a : A.V), (prin G) σ (self.left a) = (prin A) f a + if a = p.first then h 1 - h 0 else 0) ∧ (∀ (b : B.V), (prin G) σ (self.right b) = (prin B) g b + if b = q.first then h (L - 1) - h L else 0) ∧ ∀ (z : G.V), (∀ (a : A.V), z ≠ self.left a) → (∀ (b : B.V), z ≠ self.right b) → 0 ≤ (prin G) σ z

def Utilities.TwoPole.ScriptGluing.symm {A : CFGraph} {B : CFGraph} {G : CFGraph} {p : TwoPole A} {q : TwoPole B} {L : ℕ} (J : ScriptGluing A B G p q L) : ScriptGluing B A G q p L

Exchange the factors and reverse the first connector's potential.

Equations

• J.symm = { left := J.right, right := J.left, left_injective := ⋯, right_injective := ⋯, disjoint := ⋯, length_pos := ⋯, glue := ⋯ }

theorem Utilities.TwoPole.ScriptGluing.winnable_sub_left_first_of_scripts {A : CFGraph} {B : CFGraph} {G : CFGraph} {p : TwoPole A} {q : TwoPole B} {L : ℕ} (J : ScriptGluing A B G p q L) (D : CFDiv G) (CA : CFDiv A) (CB : CFDiv B) (hDA : ∀ (a : A.V), D (J.left a) = CA a) (hDB : ∀ (b : B.V), D (J.right b) = CB b) (hOutside : ∀ (z : G.V), (∀ (a : A.V), z ≠ J.left a) → (∀ (b : B.V), z ≠ J.right b) → 0 ≤ D z) (f : firingScript A) (g : firingScript B) (h : ℕ → ℤ) (h0 : h 0 = f p.first) (hL : h L = g q.first) (hSecond : f p.second = g q.second) (hConvex : ∀ (j : ℕ), 0 < j → j < L → 0 ≤ h (j - 1) - 2 * h j + h (j + 1)) (hLeft : ∀ (a : A.V), 0 ≤ CA a - oneChip p.first a + (prin A) f a + if a = p.first then h 1 - h 0 else 0) (hRight : ∀ (b : B.V), 0 ≤ CB b + (prin B) g b + if b = q.first then h (L - 1) - h L else 0) : winnable G (D - oneChip (J.left p.first))

Factor inequalities and a convex connector give a global winning script. The ambient divisor may also carry effective chips outside the factors.

theorem Utilities.TwoPole.ScriptGluing.winnable_sub_left_first {A : CFGraph} {B : CFGraph} {G : CFGraph} {p : TwoPole A} {q : TwoPole B} {L : ℕ} (J : ScriptGluing A B G p q L) (D : CFDiv G) (CA : CFDiv A) (CB : CFDiv B) (hDA : ∀ (a : A.V), D (J.left a) = CA a) (hDB : ∀ (b : B.V), D (J.right b) = CB b) (hOutside : ∀ (z : G.V), (∀ (a : A.V), z ≠ J.left a) → (∀ (b : B.V), z ≠ J.right b) → 0 ≤ D z) (hCA : effective CA) (hCB : effective CB) (hWinA : winnable A (CA - oneChip p.first)) (hWinB : winnable B (CB - oneChip q.first)) : winnable G (D - oneChip (J.left p.first))

The three-case connector argument. Only the two local one-chip tests are needed; the factors need not be connected or carry full pencils here.

theorem Utilities.TwoPole.ScriptGluing.winnable_sub_right_first {A : CFGraph} {B : CFGraph} {G : CFGraph} {p : TwoPole A} {q : TwoPole B} {L : ℕ} (J : ScriptGluing A B G p q L) (D : CFDiv G) (CA : CFDiv A) (CB : CFDiv B) (hDA : ∀ (a : A.V), D (J.left a) = CA a) (hDB : ∀ (b : B.V), D (J.right b) = CB b) (hOutside : ∀ (z : G.V), (∀ (a : A.V), z ≠ J.left a) → (∀ (b : B.V), z ≠ J.right b) → 0 ≤ D z) (hCA : effective CA) (hCB : effective CB) (hWinA : winnable A (CA - oneChip p.first)) (hWinB : winnable B (CB - oneChip q.first)) : winnable G (D - oneChip (J.right q.first))

The symmetric attachment-vertex conclusion, using the same gluing data.