Row 12 as a guarding set #
LowGenus/GuardingSet.lean claims that the closing step of an
Atanasov--Ranganathan row proof is generic: pick a core-supported chip
assignment of degree four, cover every chip-free vertex by library pictures,
and the closed-orthant construction follows. This file cashes that claim on
the row where the composition is most visible.
Row 12's chip-free vertices are covered by two different pictures -- the
AR configuration-3 pair 2--7 and the AR configuration-2 tripods -- and
GenusFiveRow12.centers_cover is the row's hand-written statement that
between them they name every chip-free vertex. Here that same fact is fed
straight into the guard field of a GuardingSet, and
GuardingSet.closedConstruction produces the row's theorem with no further
row-specific work: no divisor bookkeeping, no fin_cases, no separator
argument.
coreClassDivisor_eq_fourChipDivisor identifies the guarding set's class
divisor with the four-chip divisor the two configuration files display, so this
is a proof about AR's own divisor and not merely a similar one. As of
2026-08-25 it is the row's only proof: GenusFiveRow12's hand-written
rowDivisor_reaches_coreVertex / row12_closedConstruction tail has been
deleted, and GenusFiveConstructions.row12_straightforward points here.
The guarding set of row 12: chips on 3, 4, 5, 6, with the AR
configuration-3 pair and the AR configuration-2 tripods between them guarding
every chip-free vertex.
Equations
- One or more equations did not get rendered due to their size.
Instances For
AR row 12, proved from a guarding set. Every step after "here are the
chips and here are their pictures" is generic. This is the row's canonical
proof: GenusFiveConstructions.row12_straightforward points here, and the
hand-written composition that used to live in GenusFiveRow12 is retired.