Documentation

LeanPool.BrillNoetherGraphs.LowGenus.GenusFiveRow06

The Atanasov--Ranganathan construction on row 06, as a guarding set #

Row 06 is the theta with three bananas: two hub vertices 2 and 3, joined by three disjoint handles, each handle a path

   2 -- x == y -- 3        (x == y a banana pair of slots)

with (x, y) = (0, 1), (4, 5) and (7, 6). The twelve slots are

  0, 1 : 0 == 1     2 : 2 -- 0    3 : 1 -- 3
  5, 6 : 7 == 6     4 : 2 -- 7    7 : 6 -- 3
 10,11 : 4 == 5     9 : 2 -- 4    8 : 3 -- 5

The guarding set is {0, 3, 4, 7} -- the hub 3 together with the near end of each banana. It leaves chip free the other hub 2 and the far end of each banana, and each of those four vertices is the centre of a picture that is already in the configuration library:

2 is a configuration-2 tripod: its three slots 2, 4, 9 end on the three distinct chips 0, 7, 4;
1, 5 and 6 are each the centre of AR's sixth picture, the banana tail of LowGenus/ConfigurationBananaTail.lean: for the centre 1 the arm vertex is c = 2, the arm chips are a = 7 and b = 4, the middle slot is 2 -- 0, the banana chip is d = 0, and the tail slot 1 -- 3 lands on the chip f = 3.

This is exactly the decomposition of GenusFiveRow14, with the multiplicities exchanged: row 14 is three tripods and one banana tail, row 06 is one tripod and three banana tails. The three banana tails are images of one another under the handle-permuting symmetry of the core, so the banana argument is written once, parameterized by the centre 1, 5 or 6; every lookup table below is a Fin 8-indexed function of that centre and every proof splits on it.

The closing step is not written by hand at all: the four pictures are packaged as an AtanasovRanganathan.Guarding.GuardingSet and GuardingSet.closedConstruction supplies the row's ClosedSubdivisionDharConstruction.

This replaces the generated fixed cover. The eight modules GenusFiveRow06Symmetry, GenusFiveRow06CoverBase, GenusFiveRow06CoverCells0--4 and GenusFiveRow06FixedCover give an independent machine-generated chamber-cover proof of the same theorem.

The divisor #

def AtanasovRanganathan.GenusFiveRow06.IsChipVertex (v : Fin 8) :

The hub 3 together with the near end of each of the three bananas.

Equations

AtanasovRanganathan.GenusFiveRow06.IsChipVertex v = (v = 0 ∨ v = 3 ∨ v = 4 ∨ v = 7)

Instances For

@[instance_reducible]

instance AtanasovRanganathan.GenusFiveRow06.instDecidableIsChipVertex (v : Fin 8) :

Decidable (IsChipVertex v)

Equations

AtanasovRanganathan.GenusFiveRow06.instDecidableIsChipVertex v = id inferInstance

def AtanasovRanganathan.GenusFiveRow06.chipWeight (v : Fin 8) :

Indicator weight of the four guarding-set vertices 0, 3, 4, and 7.

Equations

AtanasovRanganathan.GenusFiveRow06.chipWeight v = if AtanasovRanganathan.GenusFiveRow06.IsChipVertex v then 1 else 0

Instances For

theorem AtanasovRanganathan.GenusFiveRow06.chipWeight_nonneg (v : Fin 8) :

0 ≤ chipWeight v

theorem AtanasovRanganathan.GenusFiveRow06.sum_chipWeight :

∑ v : Fin 8, chipWeight v = 4

theorem AtanasovRanganathan.GenusFiveRow06.chipWeight_eq_fourChipWeight :

chipWeight = Guarding.fourChipWeight 0 3 4 7

The row's weight is the four-chip indicator of the guarding-set glue.

def AtanasovRanganathan.GenusFiveRow06.rowDivisor (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) :

The graph divisor obtained by pushing the four guarding-set chips to their core equivalence classes.

Equations

AtanasovRanganathan.GenusFiveRow06.rowDivisor d = d.coreClassDivisor AtanasovRanganathan.GenusFiveRow06.chipWeight

Instances For

theorem AtanasovRanganathan.GenusFiveRow06.rowDivisor_effective (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) :

effective (rowDivisor d)

theorem AtanasovRanganathan.GenusFiveRow06.rowDivisor_degree (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) :

CFDiv.degree (rowDivisor d) = 4

The configuration-2 tripod at the hub `2` #

def AtanasovRanganathan.GenusFiveRow06.isCenter :

Fin 8 → Bool

The predicate selecting vertex 2 as the tripod centre.

Equations

Instances For

def AtanasovRanganathan.GenusFiveRow06.firstArm :

Fin 8 → Fin 12

The first tripod arm at centre 2 is slot 2; the value at any other vertex is the unused default zero.

Equations

Instances For

def AtanasovRanganathan.GenusFiveRow06.secondArm :

Fin 8 → Fin 12

The second tripod arm at centre 2 is slot 4; the value at any other vertex is the unused default zero.

Equations

Instances For

def AtanasovRanganathan.GenusFiveRow06.thirdArm :

Fin 8 → Fin 12

The third tripod arm at centre 2 is slot 9; the value at any other vertex is the unused default zero.

Equations

Instances For

def AtanasovRanganathan.GenusFiveRow06.firstChip :

Fin 8 → Fin 8

The chip at the far end of the first tripod arm is vertex 0; other inputs use the same default.

Equations

Instances For

def AtanasovRanganathan.GenusFiveRow06.secondChip :

Fin 8 → Fin 8

The chip at the far end of the second tripod arm is vertex 7; inputs other than centre 2 use default zero.

Equations

Instances For

def AtanasovRanganathan.GenusFiveRow06.thirdChip :

Fin 8 → Fin 8

The chip at the far end of the third tripod arm is vertex 4; inputs other than centre 2 use default zero.

Equations

Instances For

def AtanasovRanganathan.GenusFiveRow06.spareChip :

Fin 8 → Fin 8

The one chip the tripod centre does not touch: the far hub 3.

Equations

Instances For

def AtanasovRanganathan.GenusFiveRow06.row06TripodConfig :

ConfigurationTwo.ConfigTwo

The hub 2 read as an AR configuration-2 picture.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem AtanasovRanganathan.GenusFiveRow06.rowDivisor_eq_tripodConfig (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) :

rowDivisor d = row06TripodConfig.divisor d

The class-sum form of the displayed divisor agrees with the four-chip form the configuration-2 family uses.

The three banana tails #

The three handles are interchangeable, so the banana argument is written once with the centre as a parameter. For a centre c ∈ {1, 5, 6} the tables below name the six slots and the four other vertices of AR's sixth picture:

centre `c`	arms `a`, `b`	middle `2 -- d`	banana `d == c`	tail `c -- 3`
`1`	`4` to `7`, `9` to `4`	`2`	`0`, `1`	`3`
`5`	`2` to `0`, `4` to `7`	`9`	`10`, `11`	`8`
`6`	`2` to `0`, `9` to `4`	`4`	`5`, `6`	`7`

The arm vertex is the hub 2 and the tail chip is the hub 3 in all three.

def AtanasovRanganathan.GenusFiveRow06.isBananaCenter :

Fin 8 → Bool

The predicate selecting vertices 1, 5, and 6 as the three banana-tail centres.

Equations

Instances For

theorem AtanasovRanganathan.GenusFiveRow06.isBananaCenter_iff (c : Fin 8) :

isBananaCenter c = true ↔ c = 1 ∨ c = 5 ∨ c = 6

def AtanasovRanganathan.GenusFiveRow06.armSlotA :

Fin 8 → Fin 12

First external arm slot for centres 1, 5, and 6, respectively 4, 2, and 2; all other inputs use zero.

Equations

Instances For

def AtanasovRanganathan.GenusFiveRow06.armSlotB :

Fin 8 → Fin 12

Second external arm slot for centres 1, 5, and 6, respectively 9, 4, and 9; all other inputs use zero.

Equations

Instances For

def AtanasovRanganathan.GenusFiveRow06.midSlot :

Fin 8 → Fin 12

Middle slot joining hub 2 to the near banana chip, respectively 2, 9, and 4 for centres 1, 5, and 6.

Equations

Instances For

def AtanasovRanganathan.GenusFiveRow06.banSlotP :

Fin 8 → Fin 12

First parallel banana slot, respectively 0, 10, and 5 for centres 1, 5, and 6; other inputs use zero.

Equations

Instances For

def AtanasovRanganathan.GenusFiveRow06.banSlotQ :

Fin 8 → Fin 12

Second parallel banana slot, respectively 1, 11, and 6 for centres 1, 5, and 6; other inputs use zero.

Equations

Instances For

def AtanasovRanganathan.GenusFiveRow06.tailSlot :

Fin 8 → Fin 12

Tail slot joining the banana centre to the far chip at vertex 3, respectively 3, 8, and 7 for centres 1, 5, and 6.

Equations

Instances For

def AtanasovRanganathan.GenusFiveRow06.armChipA :

Fin 8 → Fin 8

Chip at the end of the first external arm, respectively vertex 7, 0, or 0 for centres 1, 5, or 6.

Equations

Instances For

def AtanasovRanganathan.GenusFiveRow06.armChipB :

Fin 8 → Fin 8

Chip at the end of the second external arm, respectively vertex 4, 7, or 4 for centres 1, 5, or 6.

Equations

Instances For

def AtanasovRanganathan.GenusFiveRow06.banChip :

Fin 8 → Fin 8

The chip at the near end of the banana.

Equations

Instances For

def AtanasovRanganathan.GenusFiveRow06.tailLedger :

Fin 8 → ConfigurationBananaTail.BananaLedger

The tail slot of the centre 5 is the only one of the eighteen displayed slots whose core orientation points into the vertex carrying the higher height; every other slot of every handle points away from it.

Equations

Instances For

The nested-min heights #

armMin is the shorter arm at the hub 2, parMin the shorter banana slot.

def AtanasovRanganathan.GenusFiveRow06.armMin (c : Fin 8) (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) :

The shorter of the two external arms of a banana-tail configuration.

Equations

AtanasovRanganathan.GenusFiveRow06.armMin c d = min (d.length (AtanasovRanganathan.GenusFiveRow06.armSlotA c)) (d.length (AtanasovRanganathan.GenusFiveRow06.armSlotB c))

Instances For

def AtanasovRanganathan.GenusFiveRow06.parMin (c : Fin 8) (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) :

The shorter of the two parallel slots in the selected banana.

Equations

AtanasovRanganathan.GenusFiveRow06.parMin c d = min (d.length (AtanasovRanganathan.GenusFiveRow06.banSlotP c)) (d.length (AtanasovRanganathan.GenusFiveRow06.banSlotQ c))

Instances For

def AtanasovRanganathan.GenusFiveRow06.endHeight (c : Fin 8) (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) :

The height at the centre.

Equations

One or more equations did not get rendered due to their size.

Instances For

def AtanasovRanganathan.GenusFiveRow06.midHeight (c : Fin 8) (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) :

The height at the chip at the near end of the banana.

Equations

One or more equations did not get rendered due to their size.

Instances For

def AtanasovRanganathan.GenusFiveRow06.armHeight (c : Fin 8) (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) :

The height at the chip-free hub 2.

Equations

AtanasovRanganathan.GenusFiveRow06.armHeight c d = min (AtanasovRanganathan.GenusFiveRow06.midHeight c d) (AtanasovRanganathan.GenusFiveRow06.armMin c d)

Instances For

def AtanasovRanganathan.GenusFiveRow06.rawHeight (c : Fin 8) (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (v : Fin 8) :

The unquotiented height profile: use the arm height at hub 2, the middle height at the near banana chip, the end height at the centre, and zero elsewhere.

Equations

One or more equations did not get rendered due to their size.

Instances For

def AtanasovRanganathan.GenusFiveRow06.rawPotential (c : Fin 8) (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (v : Fin 8) :

Integer-valued firing potential given by the negative of the unquotiented height profile.

Equations

AtanasovRanganathan.GenusFiveRow06.rawPotential c d v = -↑(AtanasovRanganathan.GenusFiveRow06.rawHeight c d v)

Instances For

def AtanasovRanganathan.GenusFiveRow06.firingPotential (c : Fin 8) (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (v : Fin 8) :

Reading the raw profile at the canonical representative makes class invariance definitional.

Equations

AtanasovRanganathan.GenusFiveRow06.firingPotential c d v = AtanasovRanganathan.GenusFiveRow06.rawPotential c d (d.rep v)

Instances For

theorem AtanasovRanganathan.GenusFiveRow06.firingPotential_repInvariant (c : Fin 8) (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) :

d.RepInvariant (firingPotential c d)

theorem AtanasovRanganathan.GenusFiveRow06.rawHeight_eq_of_zero_edge (c : Fin 8) (hc : isBananaCenter c = true) (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (e : Fin 12) :

d.length e = 0 → rawHeight c d (GenusFiveCoreAtlas.row06Core.tail e) = rawHeight c d (GenusFiveCoreAtlas.row06Core.head e)

theorem AtanasovRanganathan.GenusFiveRow06.rawPotential_eq_of_zero_edge (c : Fin 8) (hc : isBananaCenter c = true) (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) {e : Fin 12} (hZero : d.length e = 0) :

rawPotential c d (GenusFiveCoreAtlas.row06Core.tail e) = rawPotential c d (GenusFiveCoreAtlas.row06Core.head e)

theorem AtanasovRanganathan.GenusFiveRow06.rawPotential_eq_of_reach (c : Fin 8) (hc : isBananaCenter c = true) (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (F : Finset (Fin 12)) (hFZero : ∀ (e : Fin 12), e ∈ F ↔ d.length e = 0) {u v : Fin 8} (hReach : Utilities.Certificate.ContractionForestCensusGeneral.ReachIn GenusFiveCoreAtlas.row06Core F u v) :

rawPotential c d u = rawPotential c d v

theorem AtanasovRanganathan.GenusFiveRow06.firingPotential_eq_raw (c : Fin 8) (hc : isBananaCenter c = true) (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (F : Finset (Fin 12)) (hRepReach : ∀ (x y : Fin 8), d.rep x = d.rep y ↔ Utilities.Certificate.ContractionForestCensusGeneral.ReachIn GenusFiveCoreAtlas.row06Core F x y) (hFZero : ∀ (e : Fin 12), e ∈ F ↔ d.length e = 0) (v : Fin 8) :

firingPotential c d v = rawPotential c d v

Redistributing chips inside contracted classes #

def AtanasovRanganathan.GenusFiveRow06.shiftWeight (c : Fin 8) (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) :

The conditional transfer that pays for the two banana chips when the middle slot has collapsed.

Equations

One or more equations did not get rendered due to their size.

Instances For

def AtanasovRanganathan.GenusFiveRow06.allocatedWeight (c : Fin 8) (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (vertex : Fin 8) :

The guarding-set weight redistributed across contracted arms and tail, with a further transfer across a contracted middle slot when the end height exceeds the middle height.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem AtanasovRanganathan.GenusFiveRow06.allocated_class_sum_eq (c : Fin 8) (hc : isBananaCenter c = true) (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (hCore : d.core = GenusFiveCoreAtlas.row06Core) (r : Fin 8) :

∑ v : Fin 8 with d.rep v = d.rep r, allocatedWeight c d v = ∑ v : Fin 8 with d.rep v = d.rep r, chipWeight v

Which vertex of the centre's class carries the delivered chip #

def AtanasovRanganathan.GenusFiveRow06.targetOwner (c : Fin 8) (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) :

Target representative after contraction: use the near banana chip when a parallel slot has zero length and the tail is longer than the shorter arm plus the middle slot; use the centre otherwise.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem AtanasovRanganathan.GenusFiveRow06.targetOwner_rep_eq_center (c : Fin 8) (hc : isBananaCenter c = true) (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (hCore : d.core = GenusFiveCoreAtlas.row06Core) :

d.rep (targetOwner c d) = d.rep c

Endpoint accounting on the contracted face #

def AtanasovRanganathan.GenusFiveRow06.heightEndpointSum (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (h : Fin 8 → ℕ) (v : Fin 8) :

The same sum read off a height profile rather than a potential.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem AtanasovRanganathan.GenusFiveRow06.positiveEndpointContribution_eq_heightForm (c : Fin 8) (hc : isBananaCenter c = true) (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (F : Finset (Fin 12)) (hRepReach : ∀ (x y : Fin 8), d.rep x = d.rep y ↔ Utilities.Certificate.ContractionForestCensusGeneral.ReachIn GenusFiveCoreAtlas.row06Core F x y) (hFZero : ∀ (e : Fin 12), e ∈ F ↔ d.length e = 0) (v : Fin 8) :

positiveEndpointContribution d (firingPotential c d) v = heightEndpointSum d (rawHeight c d) v

The per-vertex coefficient of the local residual #

The six vertices of the picture are armChipA c, armChipB c, the hub 2, banChip c, the centre c and the hub 3; on each handle these are six distinct vertices, and every other vertex sits at height zero with no displaced chip.

def AtanasovRanganathan.GenusFiveRow06.bananaCoefficient (c : Fin 8) (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (v : Fin 8) :

Expanded coefficients after adding the banana-tail height endpoint sum to the allocated weight, separated by the six distinguished vertices of the configuration.

Equations

One or more equations did not get rendered due to their size.

Instances For

The endpoint bookkeeping is a single kernel-level computation on each handle. It is stated three times, once per centre, only so that each of the three fin_cases sweeps gets its own elaboration budget.

theorem AtanasovRanganathan.GenusFiveRow06.bananaCoefficient_eq_one (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (hCore : d.core = GenusFiveCoreAtlas.row06Core) (v : Fin 8) :

allocatedWeight 1 d v + heightEndpointSum d (rawHeight 1 d) v = bananaCoefficient 1 d v

theorem AtanasovRanganathan.GenusFiveRow06.bananaCoefficient_eq_five (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (hCore : d.core = GenusFiveCoreAtlas.row06Core) (v : Fin 8) :

allocatedWeight 5 d v + heightEndpointSum d (rawHeight 5 d) v = bananaCoefficient 5 d v

theorem AtanasovRanganathan.GenusFiveRow06.bananaCoefficient_eq_six (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (hCore : d.core = GenusFiveCoreAtlas.row06Core) (v : Fin 8) :

allocatedWeight 6 d v + heightEndpointSum d (rawHeight 6 d) v = bananaCoefficient 6 d v

theorem AtanasovRanganathan.GenusFiveRow06.bananaCoefficient_eq (c : Fin 8) (hc : isBananaCenter c = true) (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (hCore : d.core = GenusFiveCoreAtlas.row06Core) (v : Fin 8) :

allocatedWeight c d v + heightEndpointSum d (rawHeight c d) v = bananaCoefficient c d v

The local residual at the centre #

theorem AtanasovRanganathan.GenusFiveRow06.picture_vertices_distinct (c : Fin 8) (hc : isBananaCenter c = true) :

armChipA c ≠ armChipB c ∧ armChipA c ≠ 2 ∧ armChipA c ≠ banChip c ∧ armChipA c ≠ c ∧ armChipA c ≠ 3 ∧ armChipB c ≠ 2 ∧ armChipB c ≠ banChip c ∧ armChipB c ≠ c ∧ armChipB c ≠ 3 ∧ 2 ≠ banChip c ∧ 2 ≠ c ∧ 2 ≠ 3 ∧ banChip c ≠ c ∧ banChip c ≠ 3 ∧ c ≠ 3

On each handle the six displayed vertices are distinct, so the branches of bananaCoefficient do not interfere.

theorem AtanasovRanganathan.GenusFiveRow06.bananaResidual_nonneg (c : Fin 8) (hc : isBananaCenter c = true) (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (v : Fin 8) :

0 ≤ bananaCoefficient c d v - indicatorWeight v (targetOwner c d)

theorem AtanasovRanganathan.GenusFiveRow06.localResidual_nonneg (c : Fin 8) (hc : isBananaCenter c = true) (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (hCore : d.core = GenusFiveCoreAtlas.row06Core) (F : Finset (Fin 12)) (hRepReach : ∀ (x y : Fin 8), d.rep x = d.rep y ↔ Utilities.Certificate.ContractionForestCensusGeneral.ReachIn GenusFiveCoreAtlas.row06Core F x y) (hFZero : ∀ (e : Fin 12), e ∈ F ↔ d.length e = 0) (v : Fin 8) :

0 ≤ allocatedWeight c d v - indicatorWeight v (targetOwner c d) + positiveEndpointContribution d (firingPotential c d) v

theorem AtanasovRanganathan.GenusFiveRow06.residual_effective (c : Fin 8) (hc : isBananaCenter c = true) (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (hCore : d.core = GenusFiveCoreAtlas.row06Core) (F : Finset (Fin 12)) (hRepReach : ∀ (x y : Fin 8), d.rep x = d.rep y ↔ Utilities.Certificate.ContractionForestCensusGeneral.ReachIn GenusFiveCoreAtlas.row06Core F x y) (hFZero : ∀ (e : Fin 12), e ∈ F ↔ d.length e = 0) :

effective (rowDivisor d - oneChip (d.coreVertex c) + (prin d.graph) (d.interpolatedScript (firingPotential c d)))

The guarding set #

theorem AtanasovRanganathan.GenusFiveRow06.centers_cover (v : Fin 8) :

¬IsChipVertex v → isCenter v = true ∨ isBananaCenter v = true

The tripod table and the three banana centres between them name every chip-free vertex.

def AtanasovRanganathan.GenusFiveRow06.row06Guard :

Guarding.GuardingSet GenusFiveCoreAtlas.row06Core

Row 06 as a guarding set. Chips on 0, 3, 4, 7; the hub 2 guarded by AR's second picture and the three banana far ends by AR's sixth.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem AtanasovRanganathan.GenusFiveRow06.row06_closedConstruction :

Configurations.ClosedSubdivisionDharConstruction GenusFiveCoreAtlas.row06Core row06_closedConstruction._proof_1

AR configurations 2 and 6 on row 06, valid simultaneously on the open cell and every nonloopy forest face. The closing step is GuardingSet.closedConstruction; nothing row-specific happens after the four pictures are named.