Atanasov--Ranganathan rank-one reductions

This file records the non-metric logical core of Lemma 4.1 in Atanasov--Ranganathan. For an effective divisor, vertices in its support are automatic rank-one tests. Consequently Dhar calculations are needed only at vertices outside the support. Their seven pictured configurations are local ways to establish precisely the remaining Reaches hypotheses below.

theorem AtanasovRanganathan.rank_ge_one_of_reaches_off_support {G : CFGraph} (D : CFDiv G) (hEffective : effective D) (hOffSupport : ∀ (vertex : G.V), D vertex = 0 → Utilities.Certificate.StrongSeparator.Reaches G D vertex) : rank G D ≥ 1

Formal core of the genus-four configuration lemma: an effective divisor has rank at least one if it reaches every vertex where it has no chip.

theorem AtanasovRanganathan.bnExists_one_of_reaches_off_support {G : CFGraph} (D : CFDiv G) (hEffective : effective D) {degree : ℤ} (hDegree : CFDiv.degree D = degree) (hOffSupport : ∀ (vertex : G.V), D vertex = 0 → Utilities.Certificate.StrongSeparator.Reaches G D vertex) : Utilities.BNExists G 1 degree

Degree bookkeeping wrapper for an arbitrary rank-one pencil. This is the form needed both for the genus-four g^1_3 and the genus-five g^1_4 in the Atanasov--Ranganathan argument.

theorem AtanasovRanganathan.bnExists_one_three_of_reaches_off_support {G : CFGraph} (D : CFDiv G) (hEffective : effective D) (hDegree : CFDiv.degree D = 3) (hOffSupport : ∀ (vertex : G.V), D vertex = 0 → Utilities.Certificate.StrongSeparator.Reaches G D vertex) : Utilities.BNExists G 1 3

Genus-four specialization retained under its original name for existing configuration proofs.