Odd subdivision descent for Brill--Noether rank #
Utilities/Subdivision/SubdivisionChipDescent.lean rounds finitely many
moving chips on an N-fold refinement to chosen ends of their coarse steps,
provided the total rounding distance is less than N. This file chooses the
ends: every fine vertex is rounded to its nearest coarse vertex, at distance
at most N / 2, and strictly less than N / 2 when N is odd. Two chips on
an odd refinement therefore always fit the budget.
The consequence for the discrete Brill--Noether rank w^r_d of
Utilities/Foundations/BrillNoetherRank.lean is:
bnRankGe_of_bnRankGe_scale_two: ifd = r + k + 2andNis odd, thenw^r_d(σ_N G) ≥ kimpliesw^r_d(G) ≥ k, for a subdivision-presentedG;Utilities.Gonality.bnRankGe_of_bnRankGe_regularSubdivision: the same for an arbitrary finite loopless multigraph and its regular subdivisionσ_N G;Utilities.Gonality.bnRankGe_one_four_of_exists_odd_regularSubdivision: the genus-five-relevant instance(∃ odd N, w^1_4(σ_N G) ≥ 1) → w^1_4(G) ≥ 1;Utilities.Gonality.bnRankGe_one_four_of_oddPairWitness: the pairwise form, in which the odd scale may depend on the prescribed pair of vertices and only the pencil through that pair is required on the refinement.
None of this needs a genus hypothesis or any algebraic-geometric input. The
production of an odd refinement carrying w^1_4 ≥ 1 (or of the pairwise
witnesses) for a genus-five graph is a separate matter, discussed in the
private research notes; this file proves only the descent.
Rounding every fine vertex to its nearest coarse vertex #
Classify a fine vertex: either it is the image of a coarse vertex, or it is a chip strictly inside a coarse step, rounded to the nearer end (ties go left).
Equations
Instances For
Descent of rank with nearest rounding. Any family of fine chips whose
total nearest-rounding distance is less than N may be rounded to nearest
coarse vertices without lowering any rank bound of the embedded divisor plus
the chips.
Brill--Noether rank descends along odd refinements #
Two residual chips, odd scale. If d = r + k + 2 and N is odd, then
w^r_d(σ_N) ≥ k implies w^r_d ≥ k on the coarse graph.
One residual chip, any scale. If d = r + k + 1, then w^r_d(σ_N) ≥ k
implies w^r_d ≥ k on the coarse graph for every N ≥ 1.
The image of an original vertex of G in its regular subdivision
σ_N G.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Odd subdivision descent for Brill--Noether rank, two residual chips.
For every finite loopless multigraph G, odd N, and d = r + k + 2,
w^r_d(σ_N G) ≥ k implies w^r_d(G) ≥ k.
The genus-five descent statement. If some odd regular subdivision of
G has w^1_4 ≥ 1, so does G itself. No genus hypothesis is needed.
The odd pair witness. Every pair of original vertices x, y (equal
or not) admits, on some odd regular subdivision depending on the pair, an
effective degree-two completion of x + y to a divisor of rank at least
one. This is the exact combinatorial input that the algebraic degree-five
argument of the research notes is meant to produce for genus-five graphs.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The pairwise form of the descent. An odd pair witness already gives
w^1_4(G) ≥ 1; the odd scale may depend on the pair, and only the pencil
through that pair is required on the refinement.