Rank profiles under vertex gluing

For divisors D and E on two graphs glued at x and y, the expected tropical-dot-product formula is

rank (D ⊕ E) = min ell, rank (D - (ell+1)x) + rank (E + ell*y) + 1.

This file proves the threshold form of that formula for every k ≥ 0. The forward implication follows from the universal effective-subtraction definition of rank and the exact winnability convolution in VertexWedge.lean. For the converse, the scalar inequalities force a staggered crossing of the two marked rank profiles; its one-step offset is exactly the offset required by the common chip shift on the wedge.

One-dimensional marked rank profiles

theorem Utilities.rank_add_zsmul_one_chip_step (G : CFGraph) (D : CFDiv G) (q : G.V) (n : ℤ) : rank G (D + n • oneChip q) ≤ rank G (D + (n + 1) • oneChip q) ∧ rank G (D + (n + 1) • oneChip q) ≤ rank G (D + n • oneChip q) + 1

Adding one marked chip changes rank by either zero or one. This is the basic discrete Lipschitz property of a marked rank profile.

theorem Utilities.deg_add_zsmul_one_chip (G : CFGraph) (D : CFDiv G) (q : G.V) (n : ℤ) : CFDiv.degree (D + n • oneChip q) = CFDiv.degree D + n

The degree along a marked rank profile is affine with slope one.

theorem Utilities.rank_add_zsmul_one_chip_eq_neg_one_of_degree_neg (G : CFGraph) (D : CFDiv G) (q : G.V) (n : ℤ) (hDegree : CFDiv.degree D + n < 0) : rank G (D + n • oneChip q) = -1

The negative-degree tail of a marked rank profile is constantly -1.

theorem Utilities.rank_add_zsmul_one_chip_eq_degree_sub_genus_of_large (G : CFGraph) (hG : graphConnected G) (D : CFDiv G) (q : G.V) (n : ℤ) (hLarge : 2 * G.genus - 2 < CFDiv.degree D + n) : rank G (D + n • oneChip q) = CFDiv.degree D + n - G.genus

On a connected graph, the sufficiently high-degree tail of a marked rank profile is the affine Riemann--Roch line degree - genus.

theorem Utilities.exists_adjacent_crossing_nat (p : ℕ → Prop) (n : ℕ) (hStart : ¬p 0) (hEnd : p n) : ∃ i < n, ¬p i ∧ p (i + 1)

A finite sequence which starts below a threshold and ends above it has an adjacent crossing. No monotonicity is needed: choose the last failed step.

theorem Utilities.exists_adjacent_crossing_int (p : ℤ → Prop) (lo hi : ℤ) (hlohi : lo ≤ hi) (hStart : ¬p lo) (hEnd : p hi) : ∃ (ell : ℤ), ¬p ell ∧ p (ell + 1)

Integer-indexed form of exists_adjacent_crossing_nat.

theorem Utilities.wedgeAddDivisor_sub (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D A : CFDiv G) (E B : CFDiv H) : wedgeAddDivisor G H x y D E - wedgeAddDivisor G H x y A B = wedgeAddDivisor G H x y (D - A) (E - B)

Wedge addition commutes with subtracting divisors on the two factors.

theorem Utilities.effective_zsmul_one_chip_of_nonneg (G : CFGraph) (q : G.V) (a : ℤ) (ha : 0 ≤ a) : effective (a • oneChip q)

A nonnegative integral multiple of one chip is effective.

theorem Utilities.winnable_add_zsmul_one_chip_mono (G : CFGraph) (D : CFDiv G) (q : G.V) (a b : ℤ) (hab : a ≤ b) (ha : winnable G (D + a • oneChip q)) : winnable G (D + b • oneChip q)

Winnability is monotone as the coefficient of a marked chip increases.

Effective test divisors on the wedge

def Utilities.wedgeRestrictLeftDivisor (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (Q : CFDiv (vertexWedge G H x y)) : CFDiv G

Restrict a wedge divisor to the left factor, assigning the entire common coefficient to the left.

Equations

• Utilities.wedgeRestrictLeftDivisor G H x y Q a = Q (Sum.inl a)

def Utilities.wedgeRestrictRightDivisor (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (Q : CFDiv (vertexWedge G H x y)) : CFDiv H

Restrict a wedge divisor to the right factor, assigning zero chips to its marked vertex (the common coefficient was assigned to the left).

Equations

• Utilities.wedgeRestrictRightDivisor G H x y Q b = if hb : b = y then 0 else Q (Sum.inr ⟨b, hb⟩)

theorem Utilities.wedgeAddDivisor_restrict (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (Q : CFDiv (vertexWedge G H x y)) : wedgeAddDivisor G H x y (wedgeRestrictLeftDivisor G H x y Q) (wedgeRestrictRightDivisor G H x y Q) = Q

The two canonical restrictions reconstruct the original wedge divisor.

theorem Utilities.effective_wedgeRestrictLeftDivisor (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (Q : CFDiv (vertexWedge G H x y)) (hQ : effective Q) : effective (wedgeRestrictLeftDivisor G H x y Q)

Effectivity descends to the canonical left restriction.

theorem Utilities.effective_wedgeRestrictRightDivisor (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (Q : CFDiv (vertexWedge G H x y)) (hQ : effective Q) : effective (wedgeRestrictRightDivisor G H x y Q)

Effectivity descends to the canonical right restriction.

theorem Utilities.deg_wedgeRestrictions (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (Q : CFDiv (vertexWedge G H x y)) : CFDiv.degree (wedgeRestrictLeftDivisor G H x y Q) + CFDiv.degree (wedgeRestrictRightDivisor G H x y Q) = CFDiv.degree Q

The degrees of the two canonical restrictions add to the wedge degree.

theorem Utilities.vertexWedge_rank_ge_of_factor_shift_cover (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) (k : ℤ) (hCover : ∀ (A : CFDiv G) (B : CFDiv H), effective A → effective B → CFDiv.degree A + CFDiv.degree B = k → ∃ (t : ℤ), winnable G (chipShift G (D - A) x t) ∧ winnable H (chipShift H (E - B) y (-t))) : rank (vertexWedge G H x y) (wedgeAddDivisor G H x y D E) ≥ k

A factorwise chip-shift cover for every effective split of degree k implies rank at least k on the wedge. This is the exact converse interface provided by winnable_vertexWedge_iff_exists_chipShift.

theorem Utilities.vertexWedge_rank_ge_of_staggered_profile_split_cover (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) (k : ℤ) (hProfile : ∀ (a b : ℤ), 0 ≤ a → 0 ≤ b → a + b = k → ∃ (ell : ℤ), rank G (D - (ell + 1) • oneChip x) ≥ a ∧ rank H (E + (ell + 1) • oneChip y) ≥ b) : rank (vertexWedge G H x y) (wedgeAddDivisor G H x y D E) ≥ k

The profile cover naturally produced by the scalar rank formula is staggered by one step. This is also the exact staggering of the two factors under a common chip shift: the left phase uses -(ell+1) and the right phase uses ell+1.

theorem Utilities.vertexWedge_rank_ge_of_profile_split_cover (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) (k : ℤ) (hProfile : ∀ (a b : ℤ), 0 ≤ a → 0 ≤ b → a + b = k → ∃ (ell : ℤ), rank G (D - (ell + 1) • oneChip x) ≥ a ∧ rank H (E + ell • oneChip y) ≥ b) : rank (vertexWedge G H x y) (wedgeAddDivisor G H x y D E) ≥ k

A convenient finite-rank-profile sufficient condition for the converse. For every degree split a+b=k, it asks for one profile index at which the two factor ranks simultaneously dominate a and b.

Crossing the two rank profiles

theorem Utilities.exists_staggered_rank_profile_split_of_inequalities (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) (k a b : ℤ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = k) (hProfile : ∀ (ell : ℤ), rank G (D - (ell + 1) • oneChip x) + rank H (E + ell • oneChip y) + 1 ≥ k) : ∃ (ell : ℤ), rank G (D - (ell + 1) • oneChip x) ≥ a ∧ rank H (E + (ell + 1) • oneChip y) ≥ b

The scalar tropical-dot-product inequalities force every nonnegative degree split to occur across one adjacent pair of phases. The proof only uses the two negative-degree tails. Far to the left the right rank is -1, while far to the right the left rank is -1; the assumed scalar inequality forces the opposite profile above the desired threshold at each endpoint.

theorem Utilities.vertexWedge_rank_ge_of_profile_inequalities (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) (k : ℤ) (_hk : 0 ≤ k) (hProfile : ∀ (ell : ℤ), rank G (D - (ell + 1) • oneChip x) + rank H (E + ell • oneChip y) + 1 ≥ k) : rank (vertexWedge G H x y) (wedgeAddDivisor G H x y D E) ≥ k

Converse to vertexWedge_rank_profile_inequality: the full family of scalar profile inequalities supplies the staggered profile cover and hence a rank lower bound on the wedge.

theorem Utilities.vertexWedge_rank_profile_inequality (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) (k : ℤ) (_hk : 0 ≤ k) (hRank : rank (vertexWedge G H x y) (wedgeAddDivisor G H x y D E) ≥ k) (ell : ℤ) : rank G (D - (ell + 1) • oneChip x) + rank H (E + ell • oneChip y) + 1 ≥ k

One direction of the vertex-gluing rank formula: a rank lower bound on the wedge forces every tropical-dot-product inequality.

theorem Utilities.vertexWedge_rank_ge_iff_profile_inequalities (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (D : CFDiv G) (E : CFDiv H) (k : ℤ) (hk : 0 ≤ k) : rank (vertexWedge G H x y) (wedgeAddDivisor G H x y D E) ≥ k ↔ ∀ (ell : ℤ), rank G (D - (ell + 1) • oneChip x) + rank H (E + ell • oneChip y) + 1 ≥ k

Tropical-dot-product rank criterion for a vertex wedge. For every nonnegative threshold k, the wedge has rank at least k exactly when every integer phase satisfies the corresponding sum-of-factor-ranks inequality.