Descending a doubled degree-two divisor from an odd subdivision #
Utilities/Subdivision/OddSubdivisionDescent.lean rounds each fine chip to its
nearest coarse vertex, at a cost of at most (N - 1) / 2 per chip. That budget
allows only two chips on an odd N-fold refinement. This file treats a
different — and for the genus-six programme more useful — configuration: a fine
divisor of the form 2 • C with C effective of degree two.
Write C = y₁ + y₂. Each yᵢ is either the image fineOf xᵢ of a coarse
vertex, in which case 2 • yᵢ = embed (2 • xᵢ) costs nothing, or an interior
fine point at offset o (with 0 < o < N) inside a coarse step. In the latter
case 2 • yᵢ is a pair of chips at one and the same fine position, and the
two chips may be rounded to opposite ends. With k ∈ {0, 1, 2} of them rounded
to the right end, the signed cost of the pair is k * N - 2 * o, so the pair
can be charged
dist(2 * o, N * ℤ) = min_k |k * N - 2 * o| ≤ N / 2,
and for odd N this reads ≤ (N - 1) / 2. Concretely
Chip.double rounds both chips left when 4 * o ≤ N, both right when
3 * N ≤ 4 * o, and splits them otherwise. Two interior points therefore
contribute at most 2 * ((N - 1) / 2) = N - 1 < N to the signed budget
∑ step, |stepCost step| of
Spec.rank_ge_of_rank_scale_ge_cost — including when they share a coarse step,
since stepCost only sees the sum of the signed costs and
|a + b| ≤ |a| + |b|. The bookkeeping is done by
Spec.sum_abs_stepCost_le_sum_abs_group, which charges a family of chips
group by group whenever each group lies inside a single coarse step.
The conclusion Spec.rank_ge_of_rank_scale_two_smul_two is that a rank bound
for 2 • C on the fine graph descends to a coarse degree-four divisor with
the same rank bound, and
Utilities.Gonality.bnExists_one_four_of_effective_square_root packages the
case r = 1 as BNExists G 1 4.
Why this is wanted #
For a genus-six graph whose specialized tetragonal class A satisfies
5 • A = 2 • K, the class K - 2 • A has degree 2, and any degree-two class
C with 2 • C ∼ A is a "square root" of A. If such a C is effective on
some odd regular subdivision, the theorem below converts the pencil
rank (2 • C) ≥ 1 into an honest w^1_4 ≥ 1 on the original graph.
This is a partial mechanism, not a complete one: a computational scan on 2026-09-05 found effective square roots for 91% of the relevant classes, not for all of them. Nothing in this file asserts that the square root exists; it only exploits one when it does.
Grouping chips that share a coarse step #
Grouped signed budget. If a family of chips is partitioned by g into
groups, each of which lies inside a single coarse step, then the signed budget
∑ step, |stepCost step| of rank_ge_of_rank_scale_ge_cost is at most the sum
over groups of the absolute value of the group's total signed cost. Chips of
one group rounded in opposite directions therefore cancel, and groups sharing a
coarse step are charged separately (by the triangle inequality).
Splitting a doubled interior point #
The two chips of a doubled interior point, rounded so that their total
signed cost is the distance from 2 * offset to N * ℤ: both left when
4 * offset ≤ N, both right when 3 * N ≤ 4 * offset, and split otherwise.
Equations
Instances For
The per-point cost bound. On an odd refinement N = 2 * m + 1 the two
chips of a doubled interior point have total signed cost at most m = (N-1)/2
in absolute value.
Descending a doubled degree-two divisor #
Descent of a doubled degree-two divisor from an odd refinement. If C
is effective of degree two on the N-fold refinement with N odd, and
rank (2 • C) ≥ r there, then the coarse graph carries an effective divisor of
degree four with rank at least r. Each of the two points of C is doubled,
and the doubled pair is rounded so that its signed cost is at most (N-1)/2.
An effective square root on an odd subdivision gives w^1_4 ≥ 1. If
some odd regular subdivision of G carries an effective degree-two divisor C
with rank (2 • C) ≥ 1, then G itself carries a divisor of degree four and
rank at least one. For a genus-six graph this applies to any degree-two class
C with 2 • C linearly equivalent to a specialized tetragonal class.