Response profiles for a two-pole join

For a divisor on a two-pole graph, a boundary response records two fluxes and the displacement of a winning firing script between the poles. Two factor responses glue exactly when their displacement difference equals the flux difference. This is the lossless scalar compatibility condition behind a two-edge cut, stated directly for the reusable TwoPole.join constructor.

The fluxes are not restricted to canonical divisors or to genus two. This is intentional: marked residuals such as 4a - 2u, higher-rank tests, and future multi-stage gluings can all use the same interface.

def Utilities.TwoPole.debit {G : CFGraph} (p : TwoPole G) (D : CFDiv G) (c₁ c₂ : ℤ) : CFDiv G

Debit the two boundary fluxes from a divisor on the left factor.

Equations

• p.debit D c₁ c₂ = D - c₁ • oneChip p.first - c₂ • oneChip p.second

def Utilities.TwoPole.credit {G : CFGraph} (p : TwoPole G) (D : CFDiv G) (c₁ c₂ : ℤ) : CFDiv G

Credit the two boundary fluxes to a divisor on the right factor.

Equations

• p.credit D c₁ c₂ = D + c₁ • oneChip p.first + c₂ • oneChip p.second

def Utilities.TwoPole.IsDebitResponse {G : CFGraph} (p : TwoPole G) (D : CFDiv G) (c₁ c₂ t : ℤ) : Prop

A response of a two-pole divisor to prescribed boundary fluxes. The integer t is the displacement of a script making the debited divisor effective.

Equations

• p.IsDebitResponse D c₁ c₂ t = Utilities.IsDisplacement (p.debit D c₁ c₂) p.first p.second 0 t

def Utilities.TwoPole.IsCreditResponse {G : CFGraph} (p : TwoPole G) (D : CFDiv G) (c₁ c₂ t : ℤ) : Prop

The credited mirror of IsDebitResponse.

Equations

• p.IsCreditResponse D c₁ c₂ t = Utilities.IsDisplacement (p.credit D c₁ c₂) p.first p.second 0 t

@[simp]

theorem Utilities.TwoPole.deg_debit {G : CFGraph} (p : TwoPole G) (D : CFDiv G) (c₁ c₂ : ℤ) : CFDiv.degree (p.debit D c₁ c₂) = CFDiv.degree D - c₁ - c₂

@[simp]

theorem Utilities.TwoPole.deg_credit {G : CFGraph} (p : TwoPole G) (D : CFDiv G) (c₁ c₂ : ℤ) : CFDiv.degree (p.credit D c₁ c₂) = CFDiv.degree D + c₁ + c₂

def Utilities.TwoPole.glueScript (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) (f : firingScript A) (g : firingScript B) (k : ℤ) : firingScript (join A B p q)

Glue factor scripts, translating the right script by a constant. The translation changes neither its factor principal divisor nor its displacement, but it sets the absolute flux through the first cross-edge.

Equations

• Utilities.TwoPole.glueScript A B p q f g k = Sum.elim f fun (b : B.V) => g b + k

@[simp]

theorem Utilities.TwoPole.glueScript_inl (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) (f : firingScript A) (g : firingScript B) (k : ℤ) (a : A.V) : glueScript A B p q f g k (Sum.inl a) = f a

@[simp]

theorem Utilities.TwoPole.glueScript_inr (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) (f : firingScript A) (g : firingScript B) (k : ℤ) (b : B.V) : glueScript A B p q f g k (Sum.inr b) = g b + k

theorem Utilities.TwoPole.prin_bridge_glueScript_inl (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) (f : firingScript A) (g : firingScript B) (k : ℤ) (a : A.V) : (prin (bridge A B p q)) (glueScript A B p q f g k) (Sum.inl a) = (prin A) f a + if a = p.first then g q.first + k - f p.first else 0

The first bridge contributes its flux at a left vertex.

theorem Utilities.TwoPole.prin_bridge_glueScript_inr (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) (f : firingScript A) (g : firingScript B) (k : ℤ) (b : B.V) : (prin (bridge A B p q)) (glueScript A B p q f g k) (Sum.inr b) = (prin B) g b + if b = q.first then f p.first - (g q.first + k) else 0

The first bridge contributes its flux at a right vertex.

theorem Utilities.TwoPole.prin_join_glueScript_inl (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) (f : firingScript A) (g : firingScript B) (k : ℤ) (a : A.V) : (prin (join A B p q)) (glueScript A B p q f g k) (Sum.inl a) = ((prin A) f a + if a = p.first then g q.first + k - f p.first else 0) + if a = p.second then g q.second + k - f p.second else 0

Both cross-edges contribute their fluxes at a left vertex.

theorem Utilities.TwoPole.prin_join_glueScript_inr (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) (f : firingScript A) (g : firingScript B) (k : ℤ) (b : B.V) : (prin (join A B p q)) (glueScript A B p q f g k) (Sum.inr b) = ((prin B) g b + if b = q.first then f p.first - (g q.first + k) else 0) + if b = q.second then f p.second - (g q.second + k) else 0

Both cross-edges contribute their fluxes at a right vertex.

theorem Utilities.TwoPole.winnable_sumDivisor_of_responses (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) (D : CFDiv A) (E : CFDiv B) (c₁ c₂ s t : ℤ) (hLeft : p.IsDebitResponse D c₁ c₂ s) (hRight : q.IsCreditResponse E c₁ c₂ t) (hMatch : s - t = c₁ - c₂) : winnable (join A B p q) (sumDivisor A B p q D E)

Two-pole response gluing. A debited response on the left and the matching credited response on the right make the original factor sum winnable. The sole compatibility equation is left displacement - right displacement = first flux - second flux.

theorem Utilities.TwoPole.exists_responses_of_winnable_sumDivisor (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) (D : CFDiv A) (E : CFDiv B) (hWin : winnable (join A B p q) (sumDivisor A B p q D E)) : ∃ (c₁ : ℤ) (c₂ : ℤ) (s : ℤ) (t : ℤ), p.IsDebitResponse D c₁ c₂ s ∧ q.IsCreditResponse E c₁ c₂ t ∧ s - t = c₁ - c₂

Completeness of two-pole responses. Every global winning script determines its two boundary fluxes and restricts to a response on each factor. Thus the scalar compatibility equation in winnable_sumDivisor_of_responses loses no information.

theorem Utilities.TwoPole.winnable_sumDivisor_iff_exists_responses (A : CFGraph) (B : CFGraph) (p : TwoPole A) (q : TwoPole B) (D : CFDiv A) (E : CFDiv B) : winnable (join A B p q) (sumDivisor A B p q D E) ↔ ∃ (c₁ : ℤ) (c₂ : ℤ) (s : ℤ) (t : ℤ), p.IsDebitResponse D c₁ c₂ s ∧ q.IsCreditResponse E c₁ c₂ t ∧ s - t = c₁ - c₂

Exact two-pole gluing criterion. A factor sum is winnable precisely when the factors admit responses whose displacement difference equals their flux difference.