Rank-one certificates

Rank at least one can be checked one vertex at a time. This module packages that reduction independently of the edge-addition machinery and gives a certificate interface suited to explicit chip-firing arguments.

theorem Utilities.effective_degree_one_eq_one_chip {G : CFGraph} (E : CFDiv G) (hEffective : effective E) (hDegree : CFDiv.degree E = 1) : ∃ (v : G.V), E = oneChip v

An effective divisor of degree one consists of a single chip.

theorem Utilities.rank_ge_one_iff_winnable_sub_one_chip (G : CFGraph) (D : CFDiv G) : rank G D ≥ 1 ↔ ∀ (v : G.V), winnable G (D - oneChip v)

Rank at least one can be tested by subtracting one chip at each vertex.

theorem Utilities.rank_ge_one_of_vertex_certificates (G : CFGraph) (D : CFDiv G) (hCertificates : ∀ (v : G.V), ∃ (E : CFDiv G), effective E ∧ linearEquiv G (D - oneChip v) E) : rank G D ≥ 1

Effective representatives for all one-chip subtractions certify rank at least one. The representatives may be different at different vertices.

theorem Utilities.rank_ge_one_of_firing_certificates (G : CFGraph) (D : CFDiv G) (hCertificates : ∀ (v : G.V), ∃ (E : CFDiv G) (σ : firingScript G), effective E ∧ E = D - oneChip v + (prin G) σ) : rank G D ≥ 1

Explicit firing scripts producing effective representatives for all one-chip subtractions certify rank at least one.

theorem Utilities.BNExists_rank_one_of_firing_certificates (G : CFGraph) (D : CFDiv G) {d : ℤ} (hDegree : CFDiv.degree D = d) (hCertificates : ∀ (v : G.V), ∃ (E : CFDiv G) (σ : firingScript G), effective E ∧ E = D - oneChip v + (prin G) σ) : BNExists G 1 d

A divisor of the requested degree, together with explicit vertexwise firing certificates, is a rank-one Brill--Noether witness.