Guarding sets: the abstract glue of an Atanasov--Ranganathan row proof #
Read the finished genus-five rows side by side and the same shape appears in
every one of them. A row fixes a core-supported chip assignment and then
shows that every chip-free core vertex is the centre of some local picture
from the configuration library; the chip vertices need no argument at all,
because a divisor that already has a chip at v reaches v. GenusFiveRow12
writes that idiom out in the open: its centers_cover says the two isCenter
tables between them name every chip-free vertex, and the two pictures'
reaches_center lemmas are then glued by hand.
This file names the idiom. A GuardingSet for a core is a nonnegative core
weight of total degree four together with, for each chip-free vertex, a proof
that the induced divisor reaches that vertex on every degenerate spec. The
main theorem turns one into a ClosedSubdivisionDharConstruction, so a row
proof becomes: exhibit a guarding set.
Which rows of the atlas are guarding sets #
Thirteen of the sixteen genus-five rows close through closedConstruction
below. The other three cannot, and the reason splits in two:
Rows 01, 02, 03, 04, 06, 07, 09, 12, 14: a GuardingSet is the row's proof
Rows 11, 13, 15, 16: one configuration instance covers every chip-free vertex, so
ConfigTwo.closedConstruction / ConfigThree.closedConstruction already close them in a line --
see the note below
Rows 05: a core-supported uniform divisor exists (1_{2,3,4,5}), but no library picture recognises
its chip-free set: two banana pairs with unequal arms. A library gap
Rows 08, 10: no core-supported degree-four divisor is uniformly rank one. An interior chip is forced, and no unmarked guarding set can exist at this degree
The two failure modes are the genus-five instances of
auxiliary calculations §2a, and the classification there was reached
with a rank oracle (direct Dhar reduction), not a certificate-search proxy.
Row 05's entry is a correction: its own docstring used to claim it had no
core-supported divisor at all, and so did row 01's before row 01 was reproved
from {2, 3, 4, 5}.
Rows 11, 13, 15 and 16 are not converted, and the obstruction is structural
rather than cosmetic: ConfigTwo and ConfigThree do not require their four
chip vertices to be pairwise distinct -- chipSum stands in for that -- so a
generic instance's displayed fourChipDivisor need not be the class divisor
of any weight, and ConfigX.closedConstruction cannot be re-derived from
closedConstruction at the library level. On those four rows the chips do
happen to be distinct, but paying coreClassDivisor_eq_fourChipDivisor to say
so makes the proof longer, not shorter.
Nothing here is new mathematics; it is the statement that the per-row gluing step is generic. What that buys is a precise reduction: with this theorem in hand, Brill--Noether existence for a family of cores is exactly the pure graph theory question "does every core in the family admit a guarding set?", with no Dhar arithmetic left in it. The numerical side of that question is probed in auxiliary calculations.
Why the chip side is free #
chip_reaches below is the whole argument for a vertex that carries a chip:
the class of v in the contracted core carries at least the weight of v
itself, because all the other weights are nonnegative, so the divisor is its
own effective representative with a chip at v.
Relation to the configuration library #
Every configuration file already proves exactly the field guard asks for,
one centre at a time and stated against an arbitrary DegSpec whose core is
the fixed one and whose representative map is reachability through the zero
slots -- see ConfigurationTwo.ConfigTwo.reaches_center,
ConfigurationThree.ConfigThree.reaches_center, and the reaches lemmas of
the reservoir, banana-tail, chipped-triangle and three-chain files. The one
adjustment is bookkeeping: those files display their divisor as a
fourChipDivisor on four named core vertices, whereas a guarding set carries
a weight function. coreClassDivisor_eq_fourChipDivisor below is that
translation, proved for four pairwise-distinct chips.
A guarding set for a core.
chips is the divisor, supported on core vertices; guard is the only
per-graph content of an AR row proof, and the configuration library is the
list of ways it is ever discharged.
The core-supported chip assignment.
Chips are chips.
The critical pencil's degree.
- guard (v : Fin n) : self.chips v = 0 → ∀ (d : Utilities.Certificate.DegenerateSpec.DegSpec n p), d.core = core → (∀ (x y : Fin n), d.rep x = d.rep y ↔ Utilities.Certificate.ContractionForestCensusGeneral.ReachIn core (Configurations.zeroSlots d.length) x y) → Utilities.Certificate.StrongSeparator.Reaches d.graph (d.coreClassDivisor self.chips) (d.coreVertex v)
Every chip-free core vertex is reached, on every degenerate spec over this core whose classes are the zero-slot components. This is precisely the statement each configuration file proves for its centres.
Instances For
The displayed divisor on one degenerate spec.
Equations
- G.divisor d = d.coreClassDivisor G.chips
Instances For
A vertex carrying a chip contributes its own weight to its class, and the
other members of the class contribute nothing negative. A corollary of
DegSpec.one_le_coreClassDivisor_of_chip, which is the same fact for an
arbitrary core weight.
A centre whose contracted class carries a chip needs no picture. The
divisor is its own effective representative, and it already has a chip at the
class, so v is reached.
This is the abstract form of chip_reaches: its proof never used
1 ≤ G.chips v, only 1 ≤ G.divisor d (d.coreVertex v), which is strictly
weaker — the chip may sit on any other member of v's contracted class.
That is what makes the collapsed-arm cases of a row's guard obligation
disappear rather than having to be discharged.
A vertex carrying a chip needs no picture.
Every contracted core class is reached: the chip vertices for free, the chip-free ones by their guarding picture.
The main theorem. A guarding set is a closed-orthant Atanasov--Ranganathan construction: the displayed divisor is a rank-one pencil of degree four simultaneously on the open cell and on every nonloopy forest face of the length orthant.
This is the abstract form of every row's closing theorem. GenusFiveRow12's
centers_cover argument is the special case where the guard is discharged by
one ConfigTwo and one ConfigThree instance.
Translating the library's displayed divisor #
The configuration files display their divisor as fourChipDivisor on four
named core vertices. A guarding set carries a weight function instead, so
that "chip free" is a statement about the weight and not about a list. The
two agree as soon as the four names are pairwise distinct.
The weight of the four-chip divisor: one on each named vertex.
Equations
- AtanasovRanganathan.Guarding.fourChipWeight a b c e v = if AtanasovRanganathan.ConfigurationThree.IsChipOf a b c e v then 1 else 0
Instances For
Summing anything against the four-chip indicator picks out the four named vertices, as soon as they are pairwise distinct.
The library's displayed divisor is a core-class divisor. With four
pairwise-distinct chip vertices, fourChipDivisor on their contracted classes
is exactly the class divisor of the indicator weight, so a configuration
instance can be read as a guarding picture without changing its divisor.