Descent of winnability and rank from a regular subdivision #

Let spec present a finite loopless multigraph with positive integral slot lengths, and let spec.scale N be its uniform N-fold refinement: every unit step of spec becomes a block of N unit steps. A divisor supported on the coarse vertices embeds into the fine graph, and this file studies what happens to a fine divisor of the form

embed D₀ + x₁ + ⋯ + xₘ

whose extra chips xᵢ sit at fine vertices strictly inside coarse steps. Each such chip is rounded to one end of its coarse step, at a cost equal to its fine distance to that end.

Theorem (winnable_of_winnable_scale). If the total rounding cost is less than N, then winnability of the fine divisor implies winnability of the rounded coarse divisor D₀ + z₁ + ⋯ + zₘ. The same holds for every rank lower bound (rank_ge_of_rank_scale_ge), because the coarse rank tests embed into fine rank tests. The sharper forms winnable_of_winnable_scale_cost and rank_ge_of_rank_scale_ge_cost charge each coarse step only the absolute value of the signed sum of its chips' costs (stepCost), so chips on one step rounded in opposite directions cancel each other.

Two chips on an odd refinement always satisfy the budget: each is within (N - 1) / 2 of its nearest coarse vertex, so the total cost is at most N - 1. That is the odd-subdivision descent used by Utilities/Subdivision/OddSubdivisionDescent.lean for Brill--Noether rank.

The proof #

Let σ be a fine winning script. Along each coarse step, the fine slopes of σ are nondecreasing except that they may drop by the number of chips at a fine vertex (prin_interiorVertex_eq_slopeDifference). Consequently the height difference B - A of σ across the step, corrected by the signed rounding cost δ of the chips in that step, lies between N * (s₁ - cL) and N * (s_N + cR), where s₁, s_N are the first and last fine slopes and cL, cR count the chips rounded to the left and right ends (Utilities.BlockSlopeRounding).

Because ∑ |δ| < N, CommonOffsetRounding.exists_common_offset gives one residue κ with round κ (B + δ) = round κ B for every step at once. The coarse script g v := round κ (σ (fineOf v)) therefore has, on every step, a slope between s₁ - cL and s_N + cR (round_sub_bounds). Summing the endpoint slopes at a coarse vertex shows that g loses, relative to σ, at most the number of chips rounded to that vertex — exactly what the rounded chips supply. No total unimodularity, period lattice, or cycle space is involved; the argument is one-dimensional on each step.

The proof is a genuine descent theorem and not the "prove it metrically, then round" fallacy recorded in the research notes: the rounding is justified step by step from the fine script, and the budget hypothesis is exactly what fails for two chips at the midpoints of an even refinement.

Descent of winnability and rank from a regular subdivision #

The proof #

Coarse vertices inside the fine graph #

Embedding coarse divisors #

Moving chips and their rounding #

Slot values of a fine script #

The step inequality #