A genus-generic trivalent expansion

Every connected ordered loopless core all of whose vertices carry at least three slot ends is the image of a cubic ordered loopless core under an equal-genus topological contraction.

The construction is the centipede: a core vertex w of valence d is replaced by a path of d - 2 trivalent vertices, each carrying one or two free legs, and the d slot ends at w are distributed along those legs. The fibre over w is a tree (a path), so contracting all fibres preserves b₁.

Counting is uniform: writing g = p - n + 1 for the genus of the core, the expanded core has 2 (g - 1) vertices and 3 (g - 1) slots, which is exactly what trivalence forces (2E = 3V and E - V + 1 = g).

The output is packaged as Utilities.Subdivision.CoreExpansion.ExpansionData, so Utilities.Subdivision.CoreExpansion.ExpansionData.certificate_topologicalValid turns it into an actual topological contraction certificate from a positive subdivision of the expanded cubic core onto any positive subdivision of the given core.

An adjacent-flip lemma

theorem Utilities.Subdivision.TrivalentExpansion.exists_flip_down (P : ℕ → Prop) {a : ℕ} (ha : P a) (b : ℕ) : a ≤ b → ¬P b → ∃ (k : ℕ), k + 1 ≤ b ∧ P k ∧ ¬P (k + 1)

Walking down from a point where P holds to a point where it fails crosses an adjacent flip.

theorem Utilities.Subdivision.TrivalentExpansion.exists_adjacent_flip {m : ℕ} (P : ℕ → Prop) {a b : ℕ} (ham : a < m) (hbm : b < m) (ha : P a) (hb : ¬P b) : ∃ (k : ℕ), k + 1 < m ∧ (P k ∧ ¬P (k + 1) ∨ ¬P k ∧ P (k + 1))

Two points of Fin m on opposite sides of a predicate are separated by an adjacent flip inside Fin m.

The centipede leg map

def Utilities.Subdivision.TrivalentExpansion.legIndex (D k : ℕ) : ℕ

Position along the centipede of the k-th slot end at a vertex of valence D. Ends 0 and 1 sit on the first centipede vertex, ends D - 2 and D - 1 on the last, and each remaining end has a centipede vertex to itself.

Equations

• Utilities.Subdivision.TrivalentExpansion.legIndex D k = if k = 0 then 0 else min (k - 1) (D - 3)

theorem Utilities.Subdivision.TrivalentExpansion.legIndex_lt {D : ℕ} (hD : 3 ≤ D) (k : ℕ) : legIndex D k < D - 2

The expanded core, before it is indexed by Fin

@[reducible, inline]

abbrev Utilities.Subdivision.TrivalentExpansion.BigV {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) : Type

Vertices of the expansion: for each core vertex w, a centipede of slotValence C w - 2 vertices.

Equations

• Utilities.Subdivision.TrivalentExpansion.BigV C = ((w : Fin n) × Fin (Utilities.Certificate.PseudocorePresentation.slotValence C w - 2))

@[reducible, inline]

abbrev Utilities.Subdivision.TrivalentExpansion.BigE {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) : Type

Slots of the expansion: the slotValence C w - 3 centipede edges at each core vertex, plus one carrier for each core slot.

Equations

• Utilities.Subdivision.TrivalentExpansion.BigE C = ((w : Fin n) × Fin (Utilities.Certificate.PseudocorePresentation.slotValence C w - 3) ⊕ Fin p)

noncomputable def Utilities.Subdivision.TrivalentExpansion.endEquiv {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (w : Fin n) : ↥(Certificate.PseudocorePresentation.slotEnds C w) ≃ Fin (Certificate.PseudocorePresentation.slotValence C w)

An arbitrary enumeration of the slot ends at a core vertex.

Equations

• Utilities.Subdivision.TrivalentExpansion.endEquiv C w = (Utilities.Certificate.PseudocorePresentation.slotEnds C w).equivFin

noncomputable def Utilities.Subdivision.TrivalentExpansion.legOf {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (w : Fin n) (x : ↥(Certificate.PseudocorePresentation.slotEnds C w)) : Fin (Certificate.PseudocorePresentation.slotValence C w - 2)

The centipede vertex carrying a given slot end.

Equations

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

def Utilities.Subdivision.TrivalentExpansion.tailEnd {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (j : Fin p) : ↥(Certificate.PseudocorePresentation.slotEnds C (C.tail j))

The tail end of a core slot, as an element of the slot-end set.

Equations

• Utilities.Subdivision.TrivalentExpansion.tailEnd C j = ⟨(j, false), ⋯⟩

def Utilities.Subdivision.TrivalentExpansion.headEnd {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (j : Fin p) : ↥(Certificate.PseudocorePresentation.slotEnds C (C.head j))

The head end of a core slot, as an element of the slot-end set.

Equations

• Utilities.Subdivision.TrivalentExpansion.headEnd C j = ⟨(j, true), ⋯⟩

noncomputable def Utilities.Subdivision.TrivalentExpansion.bigTail {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) : BigE C → BigV C

Tail endpoint of an expansion slot.

Equations

• One or more equations did not get rendered due to their size.
• Utilities.Subdivision.TrivalentExpansion.bigTail C hDeg (Sum.inl x_1) = ⟨x_1.fst, ⟨↑x_1.snd, ⋯⟩⟩

noncomputable def Utilities.Subdivision.TrivalentExpansion.bigHead {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) : BigE C → BigV C

Head endpoint of an expansion slot.

Equations

• One or more equations did not get rendered due to their size.
• Utilities.Subdivision.TrivalentExpansion.bigHead C hDeg (Sum.inl x_1) = ⟨x_1.fst, ⟨↑x_1.snd + 1, ⋯⟩⟩

Counting

theorem Utilities.Subdivision.TrivalentExpansion.sum_valence_sub_two {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) : ∑ w : Fin n, (Certificate.PseudocorePresentation.slotValence C w - 2) + 2 * n = 2 * p

theorem Utilities.Subdivision.TrivalentExpansion.sum_valence_sub_three {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) : ∑ w : Fin n, (Certificate.PseudocorePresentation.slotValence C w - 3) + 3 * n = 2 * p

theorem Utilities.Subdivision.TrivalentExpansion.card_bigV {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) : Fintype.card (BigV C) = 2 * (p - n)

theorem Utilities.Subdivision.TrivalentExpansion.card_bigE {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) : Fintype.card (BigE C) = 3 * (p - n)

Indexing the expansion by Fin

noncomputable def Utilities.Subdivision.TrivalentExpansion.vEquiv {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) : BigV C ≃ Fin (2 * (p - n))

An indexing of the expansion vertices.

Equations

• Utilities.Subdivision.TrivalentExpansion.vEquiv C hDeg = Fintype.equivFinOfCardEq ⋯

noncomputable def Utilities.Subdivision.TrivalentExpansion.eEquiv {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) : BigE C ≃ Fin (3 * (p - n))

An indexing of the expansion slots.

Equations

• Utilities.Subdivision.TrivalentExpansion.eEquiv C hDeg = Fintype.equivFinOfCardEq ⋯

noncomputable def Utilities.Subdivision.TrivalentExpansion.data {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) : CoreExpansion.ExpansionData n p (2 * (p - n)) (3 * (p - n))

The centipede expansion datum.

Equations

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

@[simp]

theorem Utilities.Subdivision.TrivalentExpansion.data_tail {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (a : BigE C) : (data C hDeg).bigCore.tail ((eEquiv C hDeg) a) = (vEquiv C hDeg) (bigTail C hDeg a)

@[simp]

theorem Utilities.Subdivision.TrivalentExpansion.data_head {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (a : BigE C) : (data C hDeg).bigCore.head ((eEquiv C hDeg) a) = (vEquiv C hDeg) (bigHead C hDeg a)

@[simp]

theorem Utilities.Subdivision.TrivalentExpansion.data_fib {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (x : BigV C) : (data C hDeg).fib ((vEquiv C hDeg) x) = x.fst

@[simp]

theorem Utilities.Subdivision.TrivalentExpansion.data_kind_inl {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (x : (w : Fin n) × Fin (Certificate.PseudocorePresentation.slotValence C w - 3)) : (data C hDeg).kind ((eEquiv C hDeg) (Sum.inl x)) = CoreExpansion.SlotKind.contracted

@[simp]

theorem Utilities.Subdivision.TrivalentExpansion.data_kind_inr {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (j : Fin p) : (data C hDeg).kind ((eEquiv C hDeg) (Sum.inr j)) = CoreExpansion.SlotKind.single j

@[simp]

theorem Utilities.Subdivision.TrivalentExpansion.data_owner {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (j : Fin p) : (data C hDeg).owner j = (eEquiv C hDeg) (Sum.inr j)

@[simp]

theorem Utilities.Subdivision.TrivalentExpansion.data_side {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (j : Fin p) : (data C hDeg).side j = false

theorem Utilities.Subdivision.TrivalentExpansion.exists_slot {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (e : Fin (3 * (p - n))) : ∃ (a : BigE C), (eEquiv C hDeg) a = e

Every expansion slot index comes from an abstract expansion slot.

theorem Utilities.Subdivision.TrivalentExpansion.exists_vertex {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (v : Fin (2 * (p - n))) : ∃ (x : BigV C), (vEquiv C hDeg) x = v

Every expansion vertex index comes from an abstract expansion vertex.

theorem Utilities.Subdivision.TrivalentExpansion.bigV_ne_of_fst {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) {u v : BigV C} (h : u.fst ≠ v.fst) : u ≠ v

theorem Utilities.Subdivision.TrivalentExpansion.bigV_ne_of_snd {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) {u v : BigV C} (h : ↑u.snd ≠ ↑v.snd) : u ≠ v

The expansion conditions

theorem Utilities.Subdivision.TrivalentExpansion.bigCore_loopless {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (hLoop : ∀ (j : Fin p), C.tail j ≠ C.head j) (e : Fin (3 * (p - n))) : (data C hDeg).bigCore.tail e ≠ (data C hDeg).bigCore.head e

theorem Utilities.Subdivision.TrivalentExpansion.slotCompatible {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (e : Fin (3 * (p - n))) : (data C hDeg).SlotCompatible C e

theorem Utilities.Subdivision.TrivalentExpansion.slotIndexed {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (e : Fin (3 * (p - n))) : (data C hDeg).SlotIndexed e

theorem Utilities.Subdivision.TrivalentExpansion.slotClaimed {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (j : Fin p) : (data C hDeg).SlotClaimed j

theorem Utilities.Subdivision.TrivalentExpansion.markerIsolated {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (e : Fin (3 * (p - n))) : (data C hDeg).MarkerIsolated C e

theorem Utilities.Subdivision.TrivalentExpansion.exists_incident {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (w : Fin n) : ∃ (j : Fin p), C.tail j = w ∨ C.head j = w

Fibre connectivity

theorem Utilities.Subdivision.TrivalentExpansion.fibre_crossing {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (T : Finset (Fin (2 * (p - n)))) (w : Fin n) (ia ib : Fin (Certificate.PseudocorePresentation.slotValence C w - 2)) (ha : (vEquiv C hDeg) ⟨w, ia⟩ ∈ T) (hb : (vEquiv C hDeg) ⟨w, ib⟩ ∉ T) : ∃ (e : Fin (3 * (p - n))), (data C hDeg).kind e = CoreExpansion.SlotKind.contracted ∧ (data C hDeg).fib ((data C hDeg).bigCore.tail e) = w ∧ ((data C hDeg).bigCore.tail e ∈ T ∧ (data C hDeg).bigCore.head e ∉ T ∨ (data C hDeg).bigCore.head e ∈ T ∧ (data C hDeg).bigCore.tail e ∉ T)

Two centipede vertices over the same core vertex on opposite sides of a subset are separated by a contracted slot of that centipede.

theorem Utilities.Subdivision.TrivalentExpansion.conditions {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (hLoop : ∀ (j : Fin p), C.tail j ≠ C.head j) : (data C hDeg).Conditions C

The expansion conditions hold.

The expanded core is cubic

theorem Utilities.Subdivision.TrivalentExpansion.mem_slotEnds_tail {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (a : BigE C) (x : BigV C) (h : bigTail C hDeg a = x) : ((eEquiv C hDeg) a, false) ∈ Certificate.PseudocorePresentation.slotEnds (data C hDeg).bigCore ((vEquiv C hDeg) x)

theorem Utilities.Subdivision.TrivalentExpansion.mem_slotEnds_head {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (a : BigE C) (x : BigV C) (h : bigHead C hDeg a = x) : ((eEquiv C hDeg) a, true) ∈ Certificate.PseudocorePresentation.slotEnds (data C hDeg).bigCore ((vEquiv C hDeg) x)

noncomputable def Utilities.Subdivision.TrivalentExpansion.bigEndOfEnd {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (w : Fin n) (x : ↥(Certificate.PseudocorePresentation.slotEnds C w)) : Fin (3 * (p - n)) × Bool

The expansion slot end attached to a core slot end.

Equations

• Utilities.Subdivision.TrivalentExpansion.bigEndOfEnd C hDeg w x = ((Utilities.Subdivision.TrivalentExpansion.eEquiv C hDeg) (Sum.inr (↑x).1), (↑x).2)

theorem Utilities.Subdivision.TrivalentExpansion.bigEndOfEnd_injective {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (w : Fin n) : Function.Injective (bigEndOfEnd C hDeg w)

theorem Utilities.Subdivision.TrivalentExpansion.bigEndOfEnd_mem {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (w : Fin n) (x : ↥(Certificate.PseudocorePresentation.slotEnds C w)) (i : Fin (Certificate.PseudocorePresentation.slotValence C w - 2)) (hleg : legOf C hDeg w x = i) : bigEndOfEnd C hDeg w x ∈ Certificate.PseudocorePresentation.slotEnds (data C hDeg).bigCore ((vEquiv C hDeg) ⟨w, i⟩)

theorem Utilities.Subdivision.TrivalentExpansion.legEnd_mem {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (w : Fin n) (i : Fin (Certificate.PseudocorePresentation.slotValence C w - 2)) (k : ℕ) (hkD : k < Certificate.PseudocorePresentation.slotValence C w) (hk : legIndex (Certificate.PseudocorePresentation.slotValence C w) k = ↑i) : bigEndOfEnd C hDeg w ((endEquiv C w).symm ⟨k, hkD⟩) ∈ Certificate.PseudocorePresentation.slotEnds (data C hDeg).bigCore ((vEquiv C hDeg) ⟨w, i⟩)

The expansion slot end attached to the k-th slot end at w lies over the centipede vertex its leg index names.

theorem Utilities.Subdivision.TrivalentExpansion.legEnd_ne {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (w : Fin n) {k k' : ℕ} (hk : k < Certificate.PseudocorePresentation.slotValence C w) (hk' : k' < Certificate.PseudocorePresentation.slotValence C w) (hne : k ≠ k') : bigEndOfEnd C hDeg w ((endEquiv C w).symm ⟨k, hk⟩) ≠ bigEndOfEnd C hDeg w ((endEquiv C w).symm ⟨k', hk'⟩)

theorem Utilities.Subdivision.TrivalentExpansion.legEnd_ne_contracted {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (w : Fin n) {k : ℕ} (hk : k < Certificate.PseudocorePresentation.slotValence C w) (x : (w : Fin n) × Fin (Certificate.PseudocorePresentation.slotValence C w - 3)) (s : Bool) : bigEndOfEnd C hDeg w ((endEquiv C w).symm ⟨k, hk⟩) ≠ ((eEquiv C hDeg) (Sum.inl x), s)

theorem Utilities.Subdivision.TrivalentExpansion.bigV_eq {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) {w : Fin n} {a b : Fin (Certificate.PseudocorePresentation.slotValence C w - 2)} (h : ↑a = ↑b) : ⟨w, a⟩ = ⟨w, b⟩

theorem Utilities.Subdivision.TrivalentExpansion.three_le_card_of_three_mem {α : Type} {s : Finset α} {a b c : α} (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (ha : a ∈ s) (hb : b ∈ s) (hc : c ∈ s) : 3 ≤ s.card

theorem Utilities.Subdivision.TrivalentExpansion.three_le_valence {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (v : Fin (2 * (p - n))) : 3 ≤ Certificate.PseudocorePresentation.slotValence (data C hDeg).bigCore v

theorem Utilities.Subdivision.TrivalentExpansion.bigCore_cubic {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) : (data C hDeg).bigCore.Cubic

The expanded core is connected

theorem Utilities.Subdivision.TrivalentExpansion.bigCore_connected {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (hConn : C.Connected) : (data C hDeg).bigCore.Connected

The genus-generic trivalent expansion theorem

theorem Utilities.Subdivision.TrivalentExpansion.exists_expansion {n p : ℕ} (C : Certificate.ExplicitPotential.Core n p) (hLoop : ∀ (j : Fin p), C.tail j ≠ C.head j) (hDeg : ∀ (w : Fin n), 3 ≤ Certificate.PseudocorePresentation.slotValence C w) (hConn : C.Connected) : ∃ (D : CoreExpansion.ExpansionData n p (2 * (p - n)) (3 * (p - n))), D.Conditions C ∧ D.bigCore.Cubic ∧ D.bigCore.Connected

Trivalent expansion. Every connected ordered loopless core of minimum slot valence three is the target of an equal-genus topological contraction from a cubic connected ordered loopless core, whose size is forced by trivalence: 2 (g - 1) vertices and 3 (g - 1) slots, where g = p - n + 1 is the genus.