Finite two-pole data for six genus-five rows

Each row is two connected leafless four-vertex, five-slot factors joined by two connector slots. The index focus : Fin 2 chooses which connector is first. The factors are exchanged when necessary to orient that connector from left to right; the second connector may retain either orientation.

All data below concern finite incidence and canonical-weight tables. They contain no rank or length hypotheses. The source slots are exactly those in GenusFiveCoreAtlas, including the reversed connector in rows 02 and 04.

def AtanasovRanganathan.GenusFiveTwoPoleData.permutation {n : ℕ} (forward inverse : Fin n → Fin n) (hLeft : ∀ (i : Fin n), inverse (forward i) = i) (hRight : ∀ (i : Fin n), forward (inverse i) = i) : Equiv.Perm (Fin n)

Bundle mutually inverse finite-index functions as a permutation.

Equations

• AtanasovRanganathan.GenusFiveTwoPoleData.permutation forward inverse hLeft hRight = { toFun := forward, invFun := inverse, left_inv := hLeft, right_inv := hRight }

def AtanasovRanganathan.GenusFiveTwoPoleData.vertexIndex (perm : Equiv.Perm (Fin 8)) : Fin 4 ⊕ Fin 4 ≃ Fin 8

Convert a permutation of eight vertices into the displayed two-core vertex indexing.

Equations

• AtanasovRanganathan.GenusFiveTwoPoleData.vertexIndex perm = finSumFinEquiv.trans perm

def AtanasovRanganathan.GenusFiveTwoPoleData.slotIndex (perm : Equiv.Perm (Fin 12)) : (Fin 5 ⊕ Fin 5) ⊕ Fin 2 ≃ Fin 12

Convert a permutation of twelve slots into the displayed two-core edge indexing.

Equations

• AtanasovRanganathan.GenusFiveTwoPoleData.slotIndex perm = ((finSumFinEquiv.sumCongr (Equiv.refl (Fin 2))).trans finSumFinEquiv).trans perm

Factor cores

def AtanasovRanganathan.GenusFiveTwoPoleData.row01LeftCore : Utilities.Certificate.ExplicitPotential.Core 4 5

The left four-vertex, five-slot component of the row-01 two-pole decomposition, with oriented slots 0→1, 0→1, 2→0, 1→3, 2→3 in index order.

Equations

• AtanasovRanganathan.GenusFiveTwoPoleData.row01LeftCore = { tail := ![0, 0, 2, 1, 2], head := ![1, 1, 0, 3, 3] }

def AtanasovRanganathan.GenusFiveTwoPoleData.row01RightCore : Utilities.Certificate.ExplicitPotential.Core 4 5

The right four-vertex, five-slot component of the row-01 two-pole decomposition, with oriented slots 1→3, 0→2, 0→1, 2→3, 2→3 in index order.

Equations

• AtanasovRanganathan.GenusFiveTwoPoleData.row01RightCore = { tail := ![1, 0, 0, 2, 2], head := ![3, 2, 1, 3, 3] }

def AtanasovRanganathan.GenusFiveTwoPoleData.row02LeftCore : Utilities.Certificate.ExplicitPotential.Core 4 5

The left four-vertex, five-slot component of the row-02 two-pole decomposition, with oriented slots 0→1, 0→2, 1→3, 2→3, 2→3 in index order.

Equations

• AtanasovRanganathan.GenusFiveTwoPoleData.row02LeftCore = { tail := ![0, 0, 1, 2, 2], head := ![1, 2, 3, 3, 3] }

def AtanasovRanganathan.GenusFiveTwoPoleData.row02RightCore : Utilities.Certificate.ExplicitPotential.Core 4 5

The right four-vertex, five-slot component of the row-02 two-pole decomposition, with oriented slots 1→2, 1→2, 2→3, 3→0, 3→0 in index order.

Equations

• AtanasovRanganathan.GenusFiveTwoPoleData.row02RightCore = { tail := ![1, 1, 2, 3, 3], head := ![2, 2, 3, 0, 0] }

def AtanasovRanganathan.GenusFiveTwoPoleData.row03LeftCore : Utilities.Certificate.ExplicitPotential.Core 4 5

The left four-vertex, five-slot component of the row-03 two-pole decomposition, with oriented slots 0→2, 2→1, 0→3, 3→1, 0→1 in index order.

Equations

• AtanasovRanganathan.GenusFiveTwoPoleData.row03LeftCore = { tail := ![0, 2, 0, 3, 0], head := ![2, 1, 3, 1, 1] }

def AtanasovRanganathan.GenusFiveTwoPoleData.row03RightCore : Utilities.Certificate.ExplicitPotential.Core 4 5

The right four-vertex, five-slot component of the row-03 two-pole decomposition, with oriented slots 2→0, 3→1, 0→1, 0→1, 2→3 in index order.

Equations

• AtanasovRanganathan.GenusFiveTwoPoleData.row03RightCore = { tail := ![2, 3, 0, 0, 2], head := ![0, 1, 1, 1, 3] }

def AtanasovRanganathan.GenusFiveTwoPoleData.row04LeftCore : Utilities.Certificate.ExplicitPotential.Core 4 5

The left four-vertex, five-slot component of the row-04 two-pole decomposition, with oriented slots 0→1, 0→1, 3→2, 3→2, 2→0 in index order.

Equations

• AtanasovRanganathan.GenusFiveTwoPoleData.row04LeftCore = { tail := ![0, 0, 3, 3, 2], head := ![1, 1, 2, 2, 0] }

def AtanasovRanganathan.GenusFiveTwoPoleData.row04RightCore : Utilities.Certificate.ExplicitPotential.Core 4 5

The right four-vertex, five-slot component of the row-04 two-pole decomposition, with oriented slots 0→1, 0→1, 1→2, 2→3, 2→3 in index order.

Equations

• AtanasovRanganathan.GenusFiveTwoPoleData.row04RightCore = { tail := ![0, 0, 1, 2, 2], head := ![1, 1, 2, 3, 3] }

def AtanasovRanganathan.GenusFiveTwoPoleData.row07LeftCore : Utilities.Certificate.ExplicitPotential.Core 4 5

The left four-vertex, five-slot component of the row-07 two-pole decomposition, with oriented slots 0→2, 2→1, 0→3, 3→1, 2→3 in index order.

Equations

• AtanasovRanganathan.GenusFiveTwoPoleData.row07LeftCore = { tail := ![0, 2, 0, 3, 2], head := ![2, 1, 3, 1, 3] }

def AtanasovRanganathan.GenusFiveTwoPoleData.row07RightCore : Utilities.Certificate.ExplicitPotential.Core 4 5

The right four-vertex, five-slot component of the row-07 two-pole decomposition, with oriented slots 2→3, 0→2, 0→2, 1→3, 1→3 in index order.

Equations

• AtanasovRanganathan.GenusFiveTwoPoleData.row07RightCore = { tail := ![2, 0, 0, 1, 1], head := ![3, 2, 2, 3, 3] }

def AtanasovRanganathan.GenusFiveTwoPoleData.row13LeftCore : Utilities.Certificate.ExplicitPotential.Core 4 5

The left four-vertex, five-slot core in the row-13 two-pole decomposition; its incidence data are the same as row07LeftCore.

Equations

• AtanasovRanganathan.GenusFiveTwoPoleData.row13LeftCore = AtanasovRanganathan.GenusFiveTwoPoleData.row07LeftCore

def AtanasovRanganathan.GenusFiveTwoPoleData.row13RightCore : Utilities.Certificate.ExplicitPotential.Core 4 5

The right four-vertex, five-slot core in the row-13 two-pole decomposition, again using row07LeftCore with the row-13 attachment data.

Equations

• AtanasovRanganathan.GenusFiveTwoPoleData.row13RightCore = AtanasovRanganathan.GenusFiveTwoPoleData.row07LeftCore

The two choices of first connector

def AtanasovRanganathan.GenusFiveTwoPoleData.row01Focus0 : Utilities.Certificate.TwoPoleSubdivision.Data GenusFiveCoreAtlas.row01Core 4 5 4 5

The explicit two-pole decomposition for row 01 with connector slot 0 first.

Equations

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

def AtanasovRanganathan.GenusFiveTwoPoleData.row01Focus1 : Utilities.Certificate.TwoPoleSubdivision.Data GenusFiveCoreAtlas.row01Core 4 5 4 5

The explicit two-pole decomposition for row 01 with connector slot 1 first.

Equations

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

def AtanasovRanganathan.GenusFiveTwoPoleData.row01 (focus : Fin 2) : Utilities.Certificate.TwoPoleSubdivision.Data GenusFiveCoreAtlas.row01Core 4 5 4 5

Row 01, with either of its two connector slots chosen first.

Equations

• AtanasovRanganathan.GenusFiveTwoPoleData.row01 focus = if focus = 0 then AtanasovRanganathan.GenusFiveTwoPoleData.row01Focus0 else AtanasovRanganathan.GenusFiveTwoPoleData.row01Focus1

def AtanasovRanganathan.GenusFiveTwoPoleData.row02Focus0 : Utilities.Certificate.TwoPoleSubdivision.Data GenusFiveCoreAtlas.row02Core 4 5 4 5

The explicit two-pole decomposition for row 02 with connector slot 0 first.

Equations

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

def AtanasovRanganathan.GenusFiveTwoPoleData.row02Focus1 : Utilities.Certificate.TwoPoleSubdivision.Data GenusFiveCoreAtlas.row02Core 4 5 4 5

The explicit two-pole decomposition for row 02 with connector slot 1 first.

Equations

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

def AtanasovRanganathan.GenusFiveTwoPoleData.row02 (focus : Fin 2) : Utilities.Certificate.TwoPoleSubdivision.Data GenusFiveCoreAtlas.row02Core 4 5 4 5

Row 02, with either of its two connector slots chosen first.

Equations

• AtanasovRanganathan.GenusFiveTwoPoleData.row02 focus = if focus = 0 then AtanasovRanganathan.GenusFiveTwoPoleData.row02Focus0 else AtanasovRanganathan.GenusFiveTwoPoleData.row02Focus1

def AtanasovRanganathan.GenusFiveTwoPoleData.row03Focus0 : Utilities.Certificate.TwoPoleSubdivision.Data GenusFiveCoreAtlas.row03Core 4 5 4 5

The explicit two-pole decomposition for row 03 with connector slot 0 first.

Equations

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

def AtanasovRanganathan.GenusFiveTwoPoleData.row03Focus1 : Utilities.Certificate.TwoPoleSubdivision.Data GenusFiveCoreAtlas.row03Core 4 5 4 5

The explicit two-pole decomposition for row 03 with connector slot 1 first.

Equations

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

def AtanasovRanganathan.GenusFiveTwoPoleData.row03 (focus : Fin 2) : Utilities.Certificate.TwoPoleSubdivision.Data GenusFiveCoreAtlas.row03Core 4 5 4 5

Row 03, with either of its two connector slots chosen first.

Equations

• AtanasovRanganathan.GenusFiveTwoPoleData.row03 focus = if focus = 0 then AtanasovRanganathan.GenusFiveTwoPoleData.row03Focus0 else AtanasovRanganathan.GenusFiveTwoPoleData.row03Focus1

def AtanasovRanganathan.GenusFiveTwoPoleData.row04Focus0 : Utilities.Certificate.TwoPoleSubdivision.Data GenusFiveCoreAtlas.row04Core 4 5 4 5

The explicit two-pole decomposition for row 04 with connector slot 0 first.

Equations

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

def AtanasovRanganathan.GenusFiveTwoPoleData.row04Focus1 : Utilities.Certificate.TwoPoleSubdivision.Data GenusFiveCoreAtlas.row04Core 4 5 4 5

The explicit two-pole decomposition for row 04 with connector slot 1 first.

Equations

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

def AtanasovRanganathan.GenusFiveTwoPoleData.row04 (focus : Fin 2) : Utilities.Certificate.TwoPoleSubdivision.Data GenusFiveCoreAtlas.row04Core 4 5 4 5

Row 04, with either of its two connector slots chosen first.

Equations

• AtanasovRanganathan.GenusFiveTwoPoleData.row04 focus = if focus = 0 then AtanasovRanganathan.GenusFiveTwoPoleData.row04Focus0 else AtanasovRanganathan.GenusFiveTwoPoleData.row04Focus1

def AtanasovRanganathan.GenusFiveTwoPoleData.row07Focus0 : Utilities.Certificate.TwoPoleSubdivision.Data GenusFiveCoreAtlas.row07Core 4 5 4 5

The explicit two-pole decomposition for row 07 with connector slot 0 first.

Equations

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

def AtanasovRanganathan.GenusFiveTwoPoleData.row07Focus1 : Utilities.Certificate.TwoPoleSubdivision.Data GenusFiveCoreAtlas.row07Core 4 5 4 5

The explicit two-pole decomposition for row 07 with connector slot 1 first.

Equations

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

def AtanasovRanganathan.GenusFiveTwoPoleData.row07 (focus : Fin 2) : Utilities.Certificate.TwoPoleSubdivision.Data GenusFiveCoreAtlas.row07Core 4 5 4 5

Row 07, with either of its two connector slots chosen first.

Equations

• AtanasovRanganathan.GenusFiveTwoPoleData.row07 focus = if focus = 0 then AtanasovRanganathan.GenusFiveTwoPoleData.row07Focus0 else AtanasovRanganathan.GenusFiveTwoPoleData.row07Focus1

def AtanasovRanganathan.GenusFiveTwoPoleData.row13Focus0 : Utilities.Certificate.TwoPoleSubdivision.Data GenusFiveCoreAtlas.row13Core 4 5 4 5

The explicit two-pole decomposition for row 13 with connector slot 0 first.

Equations

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

def AtanasovRanganathan.GenusFiveTwoPoleData.row13Focus1 : Utilities.Certificate.TwoPoleSubdivision.Data GenusFiveCoreAtlas.row13Core 4 5 4 5

The explicit two-pole decomposition for row 13 with connector slot 1 first.

Equations

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

def AtanasovRanganathan.GenusFiveTwoPoleData.row13 (focus : Fin 2) : Utilities.Certificate.TwoPoleSubdivision.Data GenusFiveCoreAtlas.row13Core 4 5 4 5

Row 13, with either of its two connector slots chosen first.

Equations

• AtanasovRanganathan.GenusFiveTwoPoleData.row13 focus = if focus = 0 then AtanasovRanganathan.GenusFiveTwoPoleData.row13Focus0 else AtanasovRanganathan.GenusFiveTwoPoleData.row13Focus1

Factor hypotheses for the canonical construction

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row01_left_connected (focus : Fin 2) : (row01 focus).leftCore.Connected

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row01_left_degree_ge_two (focus : Fin 2) (v : Fin 4) : 2 ≤ (row01 focus).leftCore.incidenceDegree v

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row01_right_connected (focus : Fin 2) : (row01 focus).rightCore.Connected

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row01_right_degree_ge_two (focus : Fin 2) (v : Fin 4) : 2 ≤ (row01 focus).rightCore.incidenceDegree v

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row02_left_connected (focus : Fin 2) : (row02 focus).leftCore.Connected

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row02_left_degree_ge_two (focus : Fin 2) (v : Fin 4) : 2 ≤ (row02 focus).leftCore.incidenceDegree v

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row02_right_connected (focus : Fin 2) : (row02 focus).rightCore.Connected

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row02_right_degree_ge_two (focus : Fin 2) (v : Fin 4) : 2 ≤ (row02 focus).rightCore.incidenceDegree v

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row03_left_connected (focus : Fin 2) : (row03 focus).leftCore.Connected

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row03_left_degree_ge_two (focus : Fin 2) (v : Fin 4) : 2 ≤ (row03 focus).leftCore.incidenceDegree v

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row03_right_connected (focus : Fin 2) : (row03 focus).rightCore.Connected

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row03_right_degree_ge_two (focus : Fin 2) (v : Fin 4) : 2 ≤ (row03 focus).rightCore.incidenceDegree v

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row04_left_connected (focus : Fin 2) : (row04 focus).leftCore.Connected

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row04_left_degree_ge_two (focus : Fin 2) (v : Fin 4) : 2 ≤ (row04 focus).leftCore.incidenceDegree v

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row04_right_connected (focus : Fin 2) : (row04 focus).rightCore.Connected

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row04_right_degree_ge_two (focus : Fin 2) (v : Fin 4) : 2 ≤ (row04 focus).rightCore.incidenceDegree v

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row07_left_connected (focus : Fin 2) : (row07 focus).leftCore.Connected

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row07_left_degree_ge_two (focus : Fin 2) (v : Fin 4) : 2 ≤ (row07 focus).leftCore.incidenceDegree v

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row07_right_connected (focus : Fin 2) : (row07 focus).rightCore.Connected

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row07_right_degree_ge_two (focus : Fin 2) (v : Fin 4) : 2 ≤ (row07 focus).rightCore.incidenceDegree v

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row13_left_connected (focus : Fin 2) : (row13 focus).leftCore.Connected

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row13_left_degree_ge_two (focus : Fin 2) (v : Fin 4) : 2 ≤ (row13 focus).leftCore.incidenceDegree v

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row13_right_connected (focus : Fin 2) : (row13 focus).rightCore.Connected

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row13_right_degree_ge_two (focus : Fin 2) (v : Fin 4) : 2 ≤ (row13 focus).rightCore.incidenceDegree v

Canonical weights and the finite coverage check

def AtanasovRanganathan.GenusFiveTwoPoleData.row13Weight : Fin 8 → ℤ

The sum of the two factor canonical divisors, supported on core vertices.

Equations

• AtanasovRanganathan.GenusFiveTwoPoleData.row13Weight = ![0, 0, 1, 1, 0, 0, 1, 1]

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row13_weight_nonneg (v : Fin 8) : 0 ≤ row13Weight v

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row13_weight_sum : ∑ v : Fin 8, row13Weight v = 4

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row13_weight_left (focus : Fin 2) (a : Fin 4) : row13Weight ((row13 focus).vertices (Sum.inl a)) = ↑((row13 focus).leftCore.incidenceDegree a) - 2

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row13_weight_right (focus : Fin 2) (b : Fin 4) : row13Weight ((row13 focus).vertices (Sum.inr b)) = ↑((row13 focus).rightCore.incidenceDegree b) - 2

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row13_coverage (v : Fin 8) : 1 ≤ row13Weight v ∨ ∃ (focus : Fin 2), v = (row13 focus).vertices (Sum.inl ((row13 focus).leftPole 0)) ∨ v = (row13 focus).vertices (Sum.inr ((row13 focus).rightPole 0))

def AtanasovRanganathan.GenusFiveTwoPoleData.row01Weight : Fin 8 → ℤ

The sum of the two factor canonical divisors, supported on core vertices.

Equations

• AtanasovRanganathan.GenusFiveTwoPoleData.row01Weight = ![1, 1, 0, 0, 0, 0, 1, 1]

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row01_weight_nonneg (v : Fin 8) : 0 ≤ row01Weight v

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row01_weight_sum : ∑ v : Fin 8, row01Weight v = 4

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row01_weight_left (focus : Fin 2) (a : Fin 4) : row01Weight ((row01 focus).vertices (Sum.inl a)) = ↑((row01 focus).leftCore.incidenceDegree a) - 2

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row01_weight_right (focus : Fin 2) (b : Fin 4) : row01Weight ((row01 focus).vertices (Sum.inr b)) = ↑((row01 focus).rightCore.incidenceDegree b) - 2

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row01_coverage (v : Fin 8) : 1 ≤ row01Weight v ∨ ∃ (focus : Fin 2), v = (row01 focus).vertices (Sum.inl ((row01 focus).leftPole 0)) ∨ v = (row01 focus).vertices (Sum.inr ((row01 focus).rightPole 0))

def AtanasovRanganathan.GenusFiveTwoPoleData.row02Weight : Fin 8 → ℤ

The sum of the two factor canonical divisors, supported on core vertices.

Equations

• AtanasovRanganathan.GenusFiveTwoPoleData.row02Weight = ![0, 0, 0, 1, 1, 0, 1, 1]

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row02_weight_nonneg (v : Fin 8) : 0 ≤ row02Weight v

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row02_weight_sum : ∑ v : Fin 8, row02Weight v = 4

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row02_weight_left (focus : Fin 2) (a : Fin 4) : row02Weight ((row02 focus).vertices (Sum.inl a)) = ↑((row02 focus).leftCore.incidenceDegree a) - 2

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row02_weight_right (focus : Fin 2) (b : Fin 4) : row02Weight ((row02 focus).vertices (Sum.inr b)) = ↑((row02 focus).rightCore.incidenceDegree b) - 2

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row02_coverage (v : Fin 8) : 1 ≤ row02Weight v ∨ ∃ (focus : Fin 2), v = (row02 focus).vertices (Sum.inl ((row02 focus).leftPole 0)) ∨ v = (row02 focus).vertices (Sum.inr ((row02 focus).rightPole 0))

def AtanasovRanganathan.GenusFiveTwoPoleData.row03Weight : Fin 8 → ℤ

The sum of the two factor canonical divisors, supported on core vertices.

Equations

• AtanasovRanganathan.GenusFiveTwoPoleData.row03Weight = ![1, 1, 0, 0, 1, 1, 0, 0]

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row03_weight_nonneg (v : Fin 8) : 0 ≤ row03Weight v

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row03_weight_sum : ∑ v : Fin 8, row03Weight v = 4

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row03_weight_left (focus : Fin 2) (a : Fin 4) : row03Weight ((row03 focus).vertices (Sum.inl a)) = ↑((row03 focus).leftCore.incidenceDegree a) - 2

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row03_weight_right (focus : Fin 2) (b : Fin 4) : row03Weight ((row03 focus).vertices (Sum.inr b)) = ↑((row03 focus).rightCore.incidenceDegree b) - 2

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row03_coverage (v : Fin 8) : 1 ≤ row03Weight v ∨ ∃ (focus : Fin 2), v = (row03 focus).vertices (Sum.inl ((row03 focus).leftPole 0)) ∨ v = (row03 focus).vertices (Sum.inr ((row03 focus).rightPole 0))

def AtanasovRanganathan.GenusFiveTwoPoleData.row04Weight : Fin 8 → ℤ

The sum of the two factor canonical divisors, supported on core vertices.

Equations

• AtanasovRanganathan.GenusFiveTwoPoleData.row04Weight = ![1, 0, 1, 0, 0, 1, 1, 0]

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row04_weight_nonneg (v : Fin 8) : 0 ≤ row04Weight v

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row04_weight_sum : ∑ v : Fin 8, row04Weight v = 4

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row04_weight_left (focus : Fin 2) (a : Fin 4) : row04Weight ((row04 focus).vertices (Sum.inl a)) = ↑((row04 focus).leftCore.incidenceDegree a) - 2

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row04_weight_right (focus : Fin 2) (b : Fin 4) : row04Weight ((row04 focus).vertices (Sum.inr b)) = ↑((row04 focus).rightCore.incidenceDegree b) - 2

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row04_coverage (v : Fin 8) : 1 ≤ row04Weight v ∨ ∃ (focus : Fin 2), v = (row04 focus).vertices (Sum.inl ((row04 focus).leftPole 0)) ∨ v = (row04 focus).vertices (Sum.inr ((row04 focus).rightPole 0))

def AtanasovRanganathan.GenusFiveTwoPoleData.row07Weight : Fin 8 → ℤ

The sum of the two factor canonical divisors, supported on core vertices.

Equations

• AtanasovRanganathan.GenusFiveTwoPoleData.row07Weight = ![0, 0, 1, 1, 0, 0, 1, 1]

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row07_weight_nonneg (v : Fin 8) : 0 ≤ row07Weight v

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row07_weight_sum : ∑ v : Fin 8, row07Weight v = 4

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row07_weight_left (focus : Fin 2) (a : Fin 4) : row07Weight ((row07 focus).vertices (Sum.inl a)) = ↑((row07 focus).leftCore.incidenceDegree a) - 2

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row07_weight_right (focus : Fin 2) (b : Fin 4) : row07Weight ((row07 focus).vertices (Sum.inr b)) = ↑((row07 focus).rightCore.incidenceDegree b) - 2

theorem AtanasovRanganathan.GenusFiveTwoPoleData.row07_coverage (v : Fin 8) : 1 ≤ row07Weight v ∨ ∃ (focus : Fin 2), v = (row07 focus).vertices (Sum.inl ((row07 focus).leftPole 0)) ∨ v = (row07 focus).vertices (Sum.inr ((row07 focus).rightPole 0))