Restricted rank and rank-determining sets

This file formalizes the definitions preceding paper Lemma 2.21 and the rank-one characterization used in its proof. We use the lower-bound relation for restricted rank, which is the literal quantified content of r_A(D) ≥ k and avoids making a second noncomputable choice of an integer rank.

def Bananas.DivisorSupportedOn {G : CFGraph} (A : Set G.V) (E : CFDiv G) : Prop

A divisor is supported on A when every vertex with nonzero coefficient belongs to A.

Equations

• Bananas.DivisorSupportedOn A E = ∀ (v : G.V), E v ≠ 0 → v ∈ A

def Bananas.restrictedRankGeq (G : CFGraph) (A : Set G.V) (D : CFDiv G) (k : ℤ) : Prop

The literal restricted-rank lower-bound relation from the paper: r_A(D) ≥ k means that subtracting every effective degree-k divisor supported on A leaves a winnable divisor.

Equations

• Bananas.restrictedRankGeq G A D k = ∀ (E : CFDiv G), effective E → CFDiv.degree E = k → Bananas.DivisorSupportedOn A E → winnable G (D - E)

def Bananas.RankDetermining (G : CFGraph) (A : Set G.V) : Prop

A set is rank determining when restricted rank agrees with ordinary rank at every integer lower bound, equivalently when r_A(D) = r(D) for every divisor D.

Equations

• Bananas.RankDetermining G A = ∀ (D : CFDiv G) (k : ℤ), Bananas.restrictedRankGeq G A D k ↔ rankGeq G D k

theorem Bananas.restrictedRankGeq_of_rank_geq {G : CFGraph} {A : Set G.V} {D : CFDiv G} {k : ℤ} (h : rankGeq G D k) : restrictedRankGeq G A D k

theorem Bananas.rankDetermining_of_rank_one_test {G : CFGraph} (A : Set G.V) (hOne : ∀ (D : CFDiv G), (∀ a ∈ A, winnable G (D - oneChip a)) → 1 ≤ rank G D) : RankDetermining G A

Luo's rank-one characterization, in the direction used by the paper. If the tests obtained by subtracting one chip at every member of A force ordinary rank at least one, then A is rank determining.

theorem Bananas.banana_endpoints_rankDetermining {g : ℕ} (B : Banana g) : RankDetermining (Utilities.Certificate.SubdivisionGraph.Spec.graph B) {leftEndpoint B, rightEndpoint B}

Paper Lemma 2.21 (lem-BananaRDS): the two multivalent endpoints of a banana graph form a rank-determining set.