The Atanasov--Ranganathan construction on row 05

Row 05 is AR's sixth genus-five family: two bananas, each attached by one leg to each of the two opposite vertices of a four-cycle.

 e0, e1 : 0 == 1     e2 : 2 -> 0     e3 : 1 -> 3
 e4 : 2 -> 5   e5 : 3 -> 5   e9 : 4 -> 3   e7 : 2 -> 4        (the square)
 e6 : 5 -> 7   e8 : 4 -> 6   e10, e11 : 6 == 7

AR's own figure does not use a core-supported divisor: two of its four chips sit at interior points of a leg, at an offset equal to another leg's length. The certificate here is therefore a marked script (Utilities/Subdivision/SplitRampScript.lean), which bends downward at the chip and lets the chip pay for the kink.

The proof below uses the marked divisor displayed in the source and a script that bends at each interior chip. The chamber hypotheses ensure that the local configuration lemmas apply.

On chamber A -- |e2| ≤ |e3| and |e6| ≤ |e8| -- the displayed divisor is

 D = [2] + [5] + (e3 at offset |e2| from 1) + (e8 at offset |e8| - |e6| from 4)

and the six chip-free vertices fall into three pictures:

• {0, 1} and {6, 7} -- AR's seventh picture, a banana pair whose two arms have equal length (|e2| on the left, |e6| on the right). That equality is exactly what the interior chip placement buys.
• {3, 4} -- AR's third picture, a chip-free pair with two chip arms each, read through ConfigurationMarkedThree: vertex 3's arms are the far half of e3 and the slot e5, vertex 4's are e7 and the near half of e8.

The other three chambers are the images of this one under the two leg swaps, so GenusFiveRow05Symmetry and ClosedOrbit.closedConstruction_of_chamber finish the closed orthant.

The two marks

The left chip sits on e3 at distance |e2| from vertex 1; the right chip sits on e8 at distance |e6| from vertex 6, i.e. at offset |e8| - |e6| from vertex 4.

def AtanasovRanganathan.GenusFiveRow05.markL (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : ℕ

Offset of the left interior chip along slot 3, measured from vertex 1 and equal to the length of slot 2.

Equations

• AtanasovRanganathan.GenusFiveRow05.markL d = d.length 2

def AtanasovRanganathan.GenusFiveRow05.markR (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : ℕ

Offset of the right interior chip along slot 8, measured from vertex 4 using truncated subtraction of the length of slot 6.

Equations

• AtanasovRanganathan.GenusFiveRow05.markR d = d.length 8 - d.length 6

def AtanasovRanganathan.GenusFiveRow05.rowMark (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (e : Fin 12) : ℕ

The marked offsets on slots 3 and 8; every other slot receives offset zero.

Equations

• AtanasovRanganathan.GenusFiveRow05.rowMark d e = if e = 3 then AtanasovRanganathan.GenusFiveRow05.markL d else if e = 8 then AtanasovRanganathan.GenusFiveRow05.markR d else 0

@[simp]

theorem AtanasovRanganathan.GenusFiveRow05.rowMark_three (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : rowMark d 3 = markL d

@[simp]

theorem AtanasovRanganathan.GenusFiveRow05.rowMark_eight (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : rowMark d 8 = markR d

theorem AtanasovRanganathan.GenusFiveRow05.rowMark_other (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) {e : Fin 12} (h3 : e ≠ 3) (h8 : e ≠ 8) : rowMark d e = 0

theorem AtanasovRanganathan.GenusFiveRow05.marked_of_rowMark_pos (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) {e : Fin 12} (h : 0 < rowMark d e) : e = 3 ∨ e = 8

The four nested-min heights of the pair {3, 4}

def AtanasovRanganathan.GenusFiveRow05.armA (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : ℕ

Vertex 3's arm minimum: the far half of e3, and e5.

Equations

• AtanasovRanganathan.GenusFiveRow05.armA d = min (d.length 3 - AtanasovRanganathan.GenusFiveRow05.markL d) (d.length 5)

def AtanasovRanganathan.GenusFiveRow05.armB (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : ℕ

Vertex 4's arm minimum: e7, and the near half of e8.

Equations

• AtanasovRanganathan.GenusFiveRow05.armB d = min (d.length 7) (AtanasovRanganathan.GenusFiveRow05.markR d)

def AtanasovRanganathan.GenusFiveRow05.pairLow (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : ℕ

The partner height, shared by both readings of the pair.

Equations

• AtanasovRanganathan.GenusFiveRow05.pairLow d = min (AtanasovRanganathan.GenusFiveRow05.armA d) (AtanasovRanganathan.GenusFiveRow05.armB d)

def AtanasovRanganathan.GenusFiveRow05.targetThree (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : ℕ

The height at vertex 3 when 3 is the target.

Equations

• AtanasovRanganathan.GenusFiveRow05.targetThree d = min (AtanasovRanganathan.GenusFiveRow05.armA d) (AtanasovRanganathan.GenusFiveRow05.pairLow d + d.length 9)

def AtanasovRanganathan.GenusFiveRow05.targetFour (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : ℕ

The height at vertex 4 when 4 is the target.

Equations

• AtanasovRanganathan.GenusFiveRow05.targetFour d = min (AtanasovRanganathan.GenusFiveRow05.armB d) (AtanasovRanganathan.GenusFiveRow05.pairLow d + d.length 9)

The four height profiles

def AtanasovRanganathan.GenusFiveRow05.heightLB (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (v : Fin 8) : ℕ

The left banana pair {0, 1}, both arms of length |e2|.

Equations

• AtanasovRanganathan.GenusFiveRow05.heightLB d v = if v = 0 then d.length 2 else if v = 1 then d.length 2 else 0

def AtanasovRanganathan.GenusFiveRow05.heightRB (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (v : Fin 8) : ℕ

The right banana pair {6, 7}, both arms of length |e6|.

Equations

• AtanasovRanganathan.GenusFiveRow05.heightRB d v = if v = 6 then d.length 6 else if v = 7 then d.length 6 else 0

def AtanasovRanganathan.GenusFiveRow05.heightT3 (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (v : Fin 8) : ℕ

The configuration-3 pair read at the target 3.

Equations

• AtanasovRanganathan.GenusFiveRow05.heightT3 d v = if v = 3 then AtanasovRanganathan.GenusFiveRow05.targetThree d else if v = 4 then AtanasovRanganathan.GenusFiveRow05.pairLow d else 0

def AtanasovRanganathan.GenusFiveRow05.heightT4 (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (v : Fin 8) : ℕ

The configuration-3 pair read at the target 4.

Equations

• AtanasovRanganathan.GenusFiveRow05.heightT4 d v = if v = 4 then AtanasovRanganathan.GenusFiveRow05.targetFour d else if v = 3 then AtanasovRanganathan.GenusFiveRow05.pairLow d else 0

The script

def AtanasovRanganathan.GenusFiveRow05.rowPotential (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (h : Fin 8 → ℕ) (v : Fin 8) : ℤ

The potential of a height profile, read at the canonical class representative so that class invariance is definitional.

Equations

• AtanasovRanganathan.GenusFiveRow05.rowPotential d h v = -↑(h (d.rep v))

theorem AtanasovRanganathan.GenusFiveRow05.rowPotential_repInvariant (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (h : Fin 8 → ℕ) : d.RepInvariant (rowPotential d h)

def AtanasovRanganathan.GenusFiveRow05.rowMarkValue (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (h : Fin 8 → ℕ) (e : Fin 12) : ℤ

The script's value at each mark: zero on the two marked slots (the chips sit at the ambient level), the tail's own value elsewhere.

Equations

• AtanasovRanganathan.GenusFiveRow05.rowMarkValue d h e = if e = 3 ∨ e = 8 then 0 else AtanasovRanganathan.GenusFiveRow05.rowPotential d h (d.core.tail e)

theorem AtanasovRanganathan.GenusFiveRow05.rowMarkValue_other (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (h : Fin 8 → ℕ) {e : Fin 12} (h3 : e ≠ 3) (h8 : e ≠ 8) : rowMarkValue d h e = rowPotential d h (d.rep (d.core.tail e))

@[simp]

theorem AtanasovRanganathan.GenusFiveRow05.rowMarkValue_three (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (h : Fin 8 → ℕ) : rowMarkValue d h 3 = 0

@[simp]

theorem AtanasovRanganathan.GenusFiveRow05.rowMarkValue_eight (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (h : Fin 8 → ℕ) : rowMarkValue d h 8 = 0

Class constancy of a profile

theorem AtanasovRanganathan.GenusFiveRow05.height_eq_of_zero_edge (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (h : Fin 8 → ℕ) (hConst : ∀ (e : Fin 12), d.length e = 0 → h (GenusFiveCoreAtlas.row05Core.tail e) = h (GenusFiveCoreAtlas.row05Core.head e)) {e : Fin 12} (hZero : d.length e = 0) : h (GenusFiveCoreAtlas.row05Core.tail e) = h (GenusFiveCoreAtlas.row05Core.head e)

theorem AtanasovRanganathan.GenusFiveRow05.height_eq_of_reach (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (h : Fin 8 → ℕ) (hConst : ∀ (e : Fin 12), d.length e = 0 → h (GenusFiveCoreAtlas.row05Core.tail e) = h (GenusFiveCoreAtlas.row05Core.head e)) (F : Finset (Fin 12)) (hFZero : ∀ (e : Fin 12), e ∈ F ↔ d.length e = 0) {u v : Fin 8} (hReach : Utilities.Certificate.ContractionForestCensusGeneral.ReachIn GenusFiveCoreAtlas.row05Core F u v) : h u = h v

theorem AtanasovRanganathan.GenusFiveRow05.height_rep_eq (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (h : Fin 8 → ℕ) (hConst : ∀ (e : Fin 12), d.length e = 0 → h (GenusFiveCoreAtlas.row05Core.tail e) = h (GenusFiveCoreAtlas.row05Core.head e)) (F : Finset (Fin 12)) (hRepReach : ∀ (x y : Fin 8), d.rep x = d.rep y ↔ Utilities.Certificate.ContractionForestCensusGeneral.ReachIn GenusFiveCoreAtlas.row05Core F x y) (hFZero : ∀ (e : Fin 12), e ∈ F ↔ d.length e = 0) (v : Fin 8) : h (d.rep v) = h v

theorem AtanasovRanganathan.GenusFiveRow05.rowPotential_eq (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) {h : Fin 8 → ℕ} (hRep : ∀ (v : Fin 8), h (d.rep v) = h v) (v : Fin 8) : rowPotential d h v = -↑(h v)

The two marked slots, spelled out

theorem AtanasovRanganathan.GenusFiveRow05.tail_three {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row05Core) : d.core.tail 3 = 1

theorem AtanasovRanganathan.GenusFiveRow05.head_three {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row05Core) : d.core.head 3 = 3

theorem AtanasovRanganathan.GenusFiveRow05.tail_eight {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row05Core) : d.core.tail 8 = 4

theorem AtanasovRanganathan.GenusFiveRow05.head_eight {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row05Core) : d.core.head 8 = 6

theorem AtanasovRanganathan.GenusFiveRow05.riseIn_three {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} {h : Fin 8 → ℕ} (hCore : d.core = GenusFiveCoreAtlas.row05Core) (hRep : ∀ (v : Fin 8), h (d.rep v) = h v) : d.markRiseIn (rowPotential d h) (rowMarkValue d h) 3 = ↑(h 1)

theorem AtanasovRanganathan.GenusFiveRow05.riseOut_three {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} {h : Fin 8 → ℕ} (hCore : d.core = GenusFiveCoreAtlas.row05Core) (hRep : ∀ (v : Fin 8), h (d.rep v) = h v) : d.markRiseOut (rowPotential d h) (rowMarkValue d h) 3 = -↑(h 3)

theorem AtanasovRanganathan.GenusFiveRow05.riseIn_eight {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} {h : Fin 8 → ℕ} (hCore : d.core = GenusFiveCoreAtlas.row05Core) (hRep : ∀ (v : Fin 8), h (d.rep v) = h v) : d.markRiseIn (rowPotential d h) (rowMarkValue d h) 8 = ↑(h 4)

theorem AtanasovRanganathan.GenusFiveRow05.riseOut_eight {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} {h : Fin 8 → ℕ} (hCore : d.core = GenusFiveCoreAtlas.row05Core) (hRep : ∀ (v : Fin 8), h (d.rep v) = h v) : d.markRiseOut (rowPotential d h) (rowMarkValue d h) 8 = -↑(h 6)

theorem AtanasovRanganathan.GenusFiveRow05.riseIn_other {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} {h : Fin 8 → ℕ} {e : Fin 12} (h3 : e ≠ 3) (h8 : e ≠ 8) : d.markRiseIn (rowPotential d h) (rowMarkValue d h) e = 0

theorem AtanasovRanganathan.GenusFiveRow05.riseOut_other {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} {h : Fin 8 → ℕ} {e : Fin 12} (h3 : e ≠ 3) (h8 : e ≠ 8) (hRep : ∀ (v : Fin 8), h (d.rep v) = h v) : d.markRiseOut (rowPotential d h) (rowMarkValue d h) e = ↑(h (d.core.tail e)) - ↑(h (d.core.head e))

Admissibility of the two marks

mark 3 ≤ |e3| is the chamber inequality |e2| ≤ |e3|; the degenerate cases mark = 0 and mark = length are exactly where the profile's height at that end vanishes.

theorem AtanasovRanganathan.GenusFiveRow05.marks_admissible {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row05Core) {h : Fin 8 → ℕ} (hRep : ∀ (v : Fin 8), h (d.rep v) = h v) (hL : d.length 2 ≤ d.length 3) (hIn3 : h 1 ≤ markL d) (hOut3 : h 3 ≤ d.length 3 - markL d) (hIn8 : h 4 ≤ markR d) (hOut8 : h 6 ≤ d.length 8 - markR d) : d.MarksAdmissible (rowPotential d h) (rowMark d) (rowMarkValue d h)

Each slot as one or two ordinary arms

def AtanasovRanganathan.GenusFiveRow05.slotTailForm (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (h : Fin 8 → ℕ) (e : Fin 12) : ℤ

Tail contribution of a slot to the marked script: a positive marked offset cuts the ramp at height zero; otherwise use the complete slot.

Equations

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

def AtanasovRanganathan.GenusFiveRow05.slotHeadForm (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (h : Fin 8 → ℕ) (e : Fin 12) : ℤ

Head contribution of a slot to the marked script, using the segment beyond an interior mark on slots 3 and 8 and the complete slot otherwise.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow05.slotTailTerm_eq {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row05Core) {h : Fin 8 → ℕ} (hRep : ∀ (v : Fin 8), h (d.rep v) = h v) (hMarks : d.MarksAdmissible (rowPotential d h) (rowMark d) (rowMarkValue d h)) (hflat3 : h 1 = 0 ∨ h 3 = 0) (hflat8 : h 4 = 0 ∨ h 6 = 0) (e : Fin 12) : ConfigurationMarkedThree.slotTailTerm d (rowPotential d h) (rowMark d) (rowMarkValue d h) e = slotTailForm d h e

theorem AtanasovRanganathan.GenusFiveRow05.slotHeadTerm_eq {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row05Core) {h : Fin 8 → ℕ} (hRep : ∀ (v : Fin 8), h (d.rep v) = h v) (hMarks : d.MarksAdmissible (rowPotential d h) (rowMark d) (rowMarkValue d h)) (hflat3 : h 1 = 0 ∨ h 3 = 0) (hflat8 : h 4 = 0 ∨ h 6 = 0) (e : Fin 12) : ConfigurationMarkedThree.slotHeadTerm d (rowPotential d h) (rowMark d) (rowMarkValue d h) e = slotHeadForm d h e

The endpoint ledger, vertex by vertex

def AtanasovRanganathan.GenusFiveRow05.contribForm (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (h : Fin 8 → ℕ) (v : Fin 8) : ℤ

The total incident-slot contribution at each row-05 core vertex, with the two marked slots evaluated by their split-ramp formulas.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow05.contrib_eq {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row05Core) {h : Fin 8 → ℕ} (hRep : ∀ (v : Fin 8), h (d.rep v) = h v) (hMarks : d.MarksAdmissible (rowPotential d h) (rowMark d) (rowMarkValue d h)) (hflat3 : h 1 = 0 ∨ h 3 = 0) (hflat8 : h 4 = 0 ∨ h 6 = 0) (v : Fin 8) : ConfigurationMarkedThree.positiveEndpointContribution d (rowPotential d h) (rowMark d) (rowMarkValue d h) v = contribForm d h v

The displayed divisor

def AtanasovRanganathan.GenusFiveRow05.chipWeight (v : Fin 8) : ℤ

The two core-supported chips of the row-05 divisor, one each at vertices 2 and 5; the remaining chips lie at the marks.

Equations

• AtanasovRanganathan.GenusFiveRow05.chipWeight v = if v = 2 then 1 else if v = 5 then 1 else 0

theorem AtanasovRanganathan.GenusFiveRow05.chipWeight_nonneg (v : Fin 8) : 0 ≤ chipWeight v

theorem AtanasovRanganathan.GenusFiveRow05.sum_chipWeight : ∑ v : Fin 8, chipWeight v = 2

def AtanasovRanganathan.GenusFiveRow05.rowDivisor (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : CFDiv d.graph

AR's divisor on chamber A: chips at the two square vertices 2 and 5, and one chip inside each of the two marked legs.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow05.rowDivisor_effective (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : effective (rowDivisor d)

theorem AtanasovRanganathan.GenusFiveRow05.rowDivisor_degree (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : CFDiv.degree (rowDivisor d) = 4

def AtanasovRanganathan.GenusFiveRow05.baseWeight (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (v : Fin 8) : ℤ

The core-class weight of the divisor: the two square chips, plus each marked chip when its mark has reached an end of its slot.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow05.baseWeight_nonneg (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (v : Fin 8) : 0 ≤ baseWeight d v

theorem AtanasovRanganathan.GenusFiveRow05.rowDivisor_coreVertex_eq (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (r : Fin 8) : rowDivisor d (d.coreVertex r) = ∑ v : Fin 8 with d.rep v = d.rep r, baseWeight d v

theorem AtanasovRanganathan.GenusFiveRow05.rowDivisor_interiorVertex (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (e : Fin 12) (o : Fin (d.length e - 1)) : rowDivisor d (d.interiorVertex e o) = oneChip (d.pathAt 3 (rowMark d 3)) (d.interiorVertex e o) + oneChip (d.pathAt 8 (rowMark d 8)) (d.interiorVertex e o)

theorem AtanasovRanganathan.GenusFiveRow05.one_le_rowDivisor_at_chip (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) {c : Fin 8} (hc : chipWeight c = 1) : 1 ≤ rowDivisor d (d.coreVertex c)

theorem AtanasovRanganathan.GenusFiveRow05.one_le_rowDivisor_at_mark (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) {e : Fin 12} {o : Fin (d.length e - 1)} (hmark : ↑o + 1 = rowMark d e) (hlt : rowMark d e < d.length e) : 1 ≤ rowDivisor d (d.interiorVertex e o)

The chip at a mark strictly inside its slot.

The two chip allocations

The banana pictures charge the divisor exactly as it stands; the configuration-3 pair moves each collapsed arm's chip onto the centre it feeds, which is a transfer inside a contracted class and so leaves every class sum alone.

def AtanasovRanganathan.GenusFiveRow05.pairAlloc (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (v : Fin 8) : ℤ

Core chip allocation for the central pair: redistribute the base weight across contracted slots 3, 5, and 7 before applying the height script.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow05.baseWeight_classSum (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (r : Fin 8) : ∑ v : Fin 8 with d.rep v = d.rep r, baseWeight d v = rowDivisor d (d.coreVertex r)

theorem AtanasovRanganathan.GenusFiveRow05.pairAlloc_classSum (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (hCore : d.core = GenusFiveCoreAtlas.row05Core) (r : Fin 8) : ∑ v : Fin 8 with d.rep v = d.rep r, pairAlloc d v = ∑ v : Fin 8 with d.rep v = d.rep r, baseWeight d v

The slot forms of the two marked legs, under a profile

theorem AtanasovRanganathan.GenusFiveRow05.slotTailForm_three_eq {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row05Core) {h : Fin 8 → ℕ} (hHeadZero : h 3 = 0) (hIn3 : h 1 ≤ markL d) : slotTailForm d h 3 = ConfigurationFive.tailContribution (markL d) (h 1) 0

theorem AtanasovRanganathan.GenusFiveRow05.slotHeadForm_three_eq {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row05Core) {h : Fin 8 → ℕ} (hTailZero : h 1 = 0) (hOut3 : h 3 ≤ d.length 3 - markL d) : slotHeadForm d h 3 = ConfigurationFive.headContribution (d.length 3 - markL d) 0 (h 3)

theorem AtanasovRanganathan.GenusFiveRow05.slotTailForm_eight_eq {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row05Core) {h : Fin 8 → ℕ} (hHeadZero : h 6 = 0) (hIn8 : h 4 ≤ markR d) : slotTailForm d h 8 = ConfigurationFive.tailContribution (markR d) (h 4) 0

theorem AtanasovRanganathan.GenusFiveRow05.slotHeadForm_eight_eq {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row05Core) {h : Fin 8 → ℕ} (hTailZero : h 4 = 0) (hOut8 : h 6 ≤ d.length 8 - markR d) : slotHeadForm d h 8 = ConfigurationFive.headContribution (d.length 8 - markR d) 0 (h 6)

theorem AtanasovRanganathan.GenusFiveRow05.slotTailForm_three_split {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row05Core) (h : Fin 8 → ℕ) : slotTailForm d h 3 = if 0 < markL d then ConfigurationFive.tailContribution (markL d) (h 1) 0 else ConfigurationFive.tailContribution (d.length 3) (h 1) (h 3)

The tail of the left marked leg, with the split kept: the profiles of the pair {3, 4} have a nonzero height at the far end.

theorem AtanasovRanganathan.GenusFiveRow05.slotHeadForm_eight_split {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row05Core) (h : Fin 8 → ℕ) : slotHeadForm d h 8 = if markR d < d.length 8 then ConfigurationFive.headContribution (d.length 8 - markR d) 0 (h 6) else ConfigurationFive.headContribution (d.length 8) (h 4) (h 6)

theorem AtanasovRanganathan.GenusFiveRow05.slotTailForm_eight_split {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row05Core) (h : Fin 8 → ℕ) : slotTailForm d h 8 = if 0 < markR d then ConfigurationFive.tailContribution (markR d) (h 4) 0 else ConfigurationFive.tailContribution (d.length 8) (h 4) (h 6)

theorem AtanasovRanganathan.GenusFiveRow05.slotHeadForm_three_split {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row05Core) (h : Fin 8 → ℕ) : slotHeadForm d h 3 = if markL d < d.length 3 then ConfigurationFive.headContribution (d.length 3 - markL d) 0 (h 3) else ConfigurationFive.headContribution (d.length 3) (h 1) (h 3)

The core-class weights, vertex by vertex

theorem AtanasovRanganathan.GenusFiveRow05.baseWeight_eq {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row05Core) (v : Fin 8) : baseWeight d v = (chipWeight v + if markL d = 0 then if v = 1 then 1 else 0 else if d.length 3 ≤ markL d then if v = 3 then 1 else 0 else 0) + if markR d = 0 then if v = 4 then 1 else 0 else if d.length 8 ≤ markR d then if v = 6 then 1 else 0 else 0

The banana pair {0, 1}

theorem AtanasovRanganathan.GenusFiveRow05.heightLB_const (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (hL : d.length 2 ≤ d.length 3) (e : Fin 12) : d.length e = 0 → heightLB d (GenusFiveCoreAtlas.row05Core.tail e) = heightLB d (GenusFiveCoreAtlas.row05Core.head e)

def AtanasovRanganathan.GenusFiveRow05.lbCoeff (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (v : Fin 8) : ℤ

The per-vertex coefficient of the left banana script.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow05.lbCoeff_eq {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row05Core) (v : Fin 8) : baseWeight d v + contribForm d (heightLB d) v = lbCoeff d v

theorem AtanasovRanganathan.GenusFiveRow05.lbCoeff_nonneg {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hL : d.length 2 ≤ d.length 3) (v : Fin 8) : 0 ≤ lbCoeff d v

def AtanasovRanganathan.GenusFiveRow05.ownerZero (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : Fin 8

The vertex of the class of 0 that owns the delivered chip.

Equations

• AtanasovRanganathan.GenusFiveRow05.ownerZero d = if d.length 2 = 0 then 2 else 0

theorem AtanasovRanganathan.GenusFiveRow05.lbCoeff_owner_zero {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} : 1 ≤ lbCoeff d (ownerZero d)

theorem AtanasovRanganathan.GenusFiveRow05.lbCoeff_owner_one {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} : 1 ≤ lbCoeff d 1

The banana pair {6, 7}

theorem AtanasovRanganathan.GenusFiveRow05.heightRB_const (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (hR : d.length 6 ≤ d.length 8) (e : Fin 12) : d.length e = 0 → heightRB d (GenusFiveCoreAtlas.row05Core.tail e) = heightRB d (GenusFiveCoreAtlas.row05Core.head e)

def AtanasovRanganathan.GenusFiveRow05.rbCoeff (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (v : Fin 8) : ℤ

Expanded core coefficients after applying the right-banana height script to the base weight; rbCoeff_eq relates this formula to the endpoint contributions.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow05.rbCoeff_eq {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row05Core) (hR : d.length 6 ≤ d.length 8) (v : Fin 8) : baseWeight d v + contribForm d (heightRB d) v = rbCoeff d v

theorem AtanasovRanganathan.GenusFiveRow05.rbCoeff_nonneg {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hR : d.length 6 ≤ d.length 8) (v : Fin 8) : 0 ≤ rbCoeff d v

def AtanasovRanganathan.GenusFiveRow05.ownerSix (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : Fin 8

Representative receiving the chip for vertex 6: choose vertex 4 when slot 8 is contracted, and vertex 6 otherwise.

Equations

• AtanasovRanganathan.GenusFiveRow05.ownerSix d = if d.length 8 = 0 then 4 else 6

def AtanasovRanganathan.GenusFiveRow05.ownerSeven (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : Fin 8

Representative receiving the chip for vertex 7: choose vertex 5 when slot 6 is contracted, and vertex 7 otherwise.

Equations

• AtanasovRanganathan.GenusFiveRow05.ownerSeven d = if d.length 6 = 0 then 5 else 7

theorem AtanasovRanganathan.GenusFiveRow05.rbCoeff_owner_seven {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (_hR : d.length 6 ≤ d.length 8) : 1 ≤ rbCoeff d (ownerSeven d)

theorem AtanasovRanganathan.GenusFiveRow05.rbCoeff_owner_six {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hR : d.length 6 ≤ d.length 8) : 1 ≤ rbCoeff d (ownerSix d)

The configuration-3 pair {3, 4}, read at the target 3

theorem AtanasovRanganathan.GenusFiveRow05.heightT3_const (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (hL : d.length 2 ≤ d.length 3) (hR : d.length 6 ≤ d.length 8) (e : Fin 12) : d.length e = 0 → heightT3 d (GenusFiveCoreAtlas.row05Core.tail e) = heightT3 d (GenusFiveCoreAtlas.row05Core.head e)

def AtanasovRanganathan.GenusFiveRow05.t3Coeff (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (v : Fin 8) : ℤ

Expanded coefficients of the allocated central-pair divisor after the script targeting vertex 3; t3Coeff_eq identifies the endpoint-sum formula.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow05.t3Coeff_eq {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row05Core) (hL : d.length 2 ≤ d.length 3) (hR : d.length 6 ≤ d.length 8) (v : Fin 8) : pairAlloc d v + contribForm d (heightT3 d) v = t3Coeff d v

theorem AtanasovRanganathan.GenusFiveRow05.t3Coeff_nonneg {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hL : d.length 2 ≤ d.length 3) (hR : d.length 6 ≤ d.length 8) (v : Fin 8) : 0 ≤ t3Coeff d v

def AtanasovRanganathan.GenusFiveRow05.ownerThree (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : Fin 8

The vertex of the class of 3 that owns the delivered chip: the partner, when the middle slot has collapsed and the partner's arms are the shorter.

Equations

• AtanasovRanganathan.GenusFiveRow05.ownerThree d = if d.length 9 = 0 ∧ ¬AtanasovRanganathan.GenusFiveRow05.armA d ≤ AtanasovRanganathan.GenusFiveRow05.armB d then 4 else 3

theorem AtanasovRanganathan.GenusFiveRow05.t3Coeff_owner {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} : 1 ≤ t3Coeff d (ownerThree d)

The configuration-3 pair {3, 4}, read at the target 4

theorem AtanasovRanganathan.GenusFiveRow05.heightT4_const (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (hL : d.length 2 ≤ d.length 3) (hR : d.length 6 ≤ d.length 8) (e : Fin 12) : d.length e = 0 → heightT4 d (GenusFiveCoreAtlas.row05Core.tail e) = heightT4 d (GenusFiveCoreAtlas.row05Core.head e)

def AtanasovRanganathan.GenusFiveRow05.t4Coeff (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (v : Fin 8) : ℤ

Expanded coefficients of the allocated central-pair divisor after the script targeting vertex 4; t4Coeff_eq identifies the endpoint-sum formula.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow05.t4Coeff_eq {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row05Core) (hL : d.length 2 ≤ d.length 3) (hR : d.length 6 ≤ d.length 8) (v : Fin 8) : pairAlloc d v + contribForm d (heightT4 d) v = t4Coeff d v

theorem AtanasovRanganathan.GenusFiveRow05.pairLow_comm (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : pairLow d = min (armB d) (armA d)

theorem AtanasovRanganathan.GenusFiveRow05.t4Coeff_nonneg {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hL : d.length 2 ≤ d.length 3) (hR : d.length 6 ≤ d.length 8) (v : Fin 8) : 0 ≤ t4Coeff d v

def AtanasovRanganathan.GenusFiveRow05.ownerFour (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : Fin 8

Representative for the vertex-4 target: use vertex 3 when slot 9 is contracted and the second arm is longer, and vertex 4 otherwise.

Equations

• AtanasovRanganathan.GenusFiveRow05.ownerFour d = if d.length 9 = 0 ∧ ¬AtanasovRanganathan.GenusFiveRow05.armB d ≤ AtanasovRanganathan.GenusFiveRow05.armA d then 3 else 4

theorem AtanasovRanganathan.GenusFiveRow05.t4Coeff_owner {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} : 1 ≤ t4Coeff d (ownerFour d)

From the per-vertex coefficients to the residual

theorem AtanasovRanganathan.GenusFiveRow05.residual_of_coeff {alloc contrib : Fin 8 → ℤ} {owner : Fin 8} (hAll : ∀ (v : Fin 8), 0 ≤ alloc v + contrib v) (hOwner : 1 ≤ alloc owner + contrib owner) (v : Fin 8) : 0 ≤ alloc v - ConfigurationCommon.indicatorWeight v owner + contrib v

theorem AtanasovRanganathan.GenusFiveRow05.mark_bounds {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row05Core) {h : Fin 8 → ℕ} (hRep : ∀ (v : Fin 8), h (d.rep v) = h v) (hIn3 : h 1 ≤ markL d) (hOut3 : h 3 ≤ d.length 3 - markL d) (hIn8 : h 4 ≤ markR d) (hOut8 : h 6 ≤ d.length 8 - markR d) (hflat3 : h 1 = 0 ∨ h 3 = 0) (hflat8 : h 4 = 0 ∨ h 6 = 0) {e : Fin 12} (hpos : 0 < rowMark d e) : d.markRiseIn (rowPotential d h) (rowMarkValue d h) e ≤ ↑(rowMark d e) ∧ -↑(d.length e - rowMark d e) ≤ d.markRiseOut (rowPotential d h) (rowMarkValue d h) e ∧ (d.markRiseIn (rowPotential d h) (rowMarkValue d h) e = 0 ∨ d.markRiseOut (rowPotential d h) (rowMarkValue d h) e = 0)

The hypotheses of the kink lemma at a mark strictly inside its slot.

theorem AtanasovRanganathan.GenusFiveRow05.residual_effective {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row05Core) {h : Fin 8 → ℕ} (hRep : ∀ (v : Fin 8), h (d.rep v) = h v) (hL : d.length 2 ≤ d.length 3) (hIn3 : h 1 ≤ markL d) (hOut3 : h 3 ≤ d.length 3 - markL d) (hIn8 : h 4 ≤ markR d) (hOut8 : h 6 ≤ d.length 8 - markR d) (hflat3 : h 1 = 0 ∨ h 3 = 0) (hflat8 : h 4 = 0 ∨ h 6 = 0) {alloc : Fin 8 → ℤ} (hAlloc : ∀ (r : Fin 8), ∑ v : Fin 8 with d.rep v = d.rep r, alloc v = ∑ v : Fin 8 with d.rep v = d.rep r, baseWeight d v) {center owner : Fin 8} (hOwnerRep : d.rep owner = d.rep center) (hLocal : ∀ (v : Fin 8), 0 ≤ alloc v - ConfigurationCommon.indicatorWeight v owner + contribForm d h v) : effective (rowDivisor d - oneChip (d.coreVertex center) + (prin d.graph) (d.splitScript (rowPotential d h) (rowMark d) (rowMarkValue d h)))

The local Dhar move. With the profile's four mark bounds and a chip allocation whose class sums are the divisor's, the marked script leaves an effective residual at the named centre.

The owners lie in their centres' classes

theorem AtanasovRanganathan.GenusFiveRow05.ownerZero_rep {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row05Core) : d.rep (ownerZero d) = d.rep 0

theorem AtanasovRanganathan.GenusFiveRow05.ownerSix_rep {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row05Core) : d.rep (ownerSix d) = d.rep 6

theorem AtanasovRanganathan.GenusFiveRow05.ownerSeven_rep {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row05Core) : d.rep (ownerSeven d) = d.rep 7

theorem AtanasovRanganathan.GenusFiveRow05.ownerThree_rep {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row05Core) : d.rep (ownerThree d) = d.rep 3

theorem AtanasovRanganathan.GenusFiveRow05.ownerFour_rep {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row05Core) : d.rep (ownerFour d) = d.rep 4

Every contracted core class is reached

theorem AtanasovRanganathan.GenusFiveRow05.rowDivisor_reaches_coreVertex {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row05Core) (hL : d.length 2 ≤ d.length 3) (hR : d.length 6 ≤ d.length 8) (F : Finset (Fin 12)) (hRepReach : ∀ (x y : Fin 8), d.rep x = d.rep y ↔ Utilities.Certificate.ContractionForestCensusGeneral.ReachIn GenusFiveCoreAtlas.row05Core F x y) (hFZero : ∀ (e : Fin 12), e ∈ F ↔ d.length e = 0) (center : Fin 8) : Utilities.Certificate.StrongSeparator.Reaches d.graph (rowDivisor d) (d.coreVertex center)

Chamber A, and the whole closed orthant

theorem AtanasovRanganathan.GenusFiveRow05.chamber_pencil (length : Fin 12 → ℕ) (forest : Utilities.Certificate.ContractionForestCensusGeneral.IsForest GenusFiveCoreAtlas.row05Core (Configurations.zeroSlots length)) (notLoopy : ¬Utilities.Certificate.ContractionForestCensusGeneral.IsLoopy GenusFiveCoreAtlas.row05Core (Configurations.zeroSlots length)) (hP : GenusFiveRow05Symmetry.Chamber length) : Nonempty (Configurations.DegreeFourDharPencil (Configurations.faceSpec GenusFiveCoreAtlas.row05Core chamber_pencil._proof_1 length forest notLoopy).graph)

theorem AtanasovRanganathan.GenusFiveRow05.row05_closedConstruction : Configurations.ClosedSubdivisionDharConstruction GenusFiveCoreAtlas.row05Core chamber_pencil._proof_1

AR's sixth family on row 05. The paper's own divisor -- two chips on the square and one inside each of the two marked legs -- has rank at least one on every nonloopy forest face, all four chambers at once.