Expanding a small subdivision core to a larger one along a contraction

This module supplies the inverse of the usual reduction move. Given a subdivision specification small over an ordered loopless core, a piece of passive combinatorial data called an ExpansionData describes a larger ordered loopless core bigCore together with

• a fibre map fib sending each big core vertex to the small core vertex its fibre collapses onto, and
• a slot classification kind, saying for each big slot whether it is contracted into a fibre, carries exactly one small slot, or carries two small slots in series through a bivalent marker of the small core.

The double case is what makes the datum usable for loop-aware small cores. A semantic loop of a topological core is displayed in a loopless split core as two slots meeting at a bivalent marker; on the big side it is one slot whose two endpoints lie in a single fibre, and the marker is an interior vertex of that slot.

The output is a topological contraction certificate bigSpec.graph → small.graph: quotient multiplicities match exactly and every fibre is connected. Nothing here is specific to genus four.

Small helpers about path vertices

theorem Utilities.Subdivision.CoreExpansion.PathHelpers.pathVertex_of_zero {n p : ℕ} (spec : Certificate.SubdivisionGraph.Spec n p) (j : Fin p) (q : spec.PathPosition j) (h : ↑q = 0) : spec.pathVertex j q = spec.coreVertex (spec.core.tail j)

theorem Utilities.Subdivision.CoreExpansion.PathHelpers.pathVertex_of_last {n p : ℕ} (spec : Certificate.SubdivisionGraph.Spec n p) (j : Fin p) (q : spec.PathPosition j) (h0 : ↑q ≠ 0) (h : ↑q = spec.length j) : spec.pathVertex j q = spec.coreVertex (spec.core.head j)

theorem Utilities.Subdivision.CoreExpansion.PathHelpers.pathVertex_of_interior {n p : ℕ} (spec : Certificate.SubdivisionGraph.Spec n p) (j : Fin p) (q : spec.PathPosition j) (h0 : ↑q ≠ 0) (h : ↑q ≠ spec.length j) : spec.pathVertex j q = spec.interiorVertex j ⟨↑q - 1, ⋯⟩

theorem Utilities.Subdivision.CoreExpansion.PathHelpers.pathVertex_congr {n p : ℕ} (spec : Certificate.SubdivisionGraph.Spec n p) (j : Fin p) (q q' : spec.PathPosition j) (h : ↑q = ↑q') : spec.pathVertex j q = spec.pathVertex j q'

Slot kinds

inductive Utilities.Subdivision.CoreExpansion.SlotKind (p : ℕ) : Type

The role of one big slot in the contraction.

• contracted {p : ℕ} : SlotKind p

  The slot is contracted; both endpoints lie in one fibre.

• single {p : ℕ} : Fin p → SlotKind p

  The slot maps onto a single small slot.

• double {p : ℕ} : Fin p → Fin p → SlotKind p

  The slot maps onto two small slots in series through a marker.

def Utilities.Subdivision.CoreExpansion.instDecidableEqSlotKind.decEq {p✝ : ℕ} (x✝ x✝¹ : SlotKind p✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Utilities.Subdivision.CoreExpansion.instDecidableEqSlotKind.decEq Utilities.Subdivision.CoreExpansion.SlotKind.contracted Utilities.Subdivision.CoreExpansion.SlotKind.contracted = isTrue ⋯
• Utilities.Subdivision.CoreExpansion.instDecidableEqSlotKind.decEq Utilities.Subdivision.CoreExpansion.SlotKind.contracted (Utilities.Subdivision.CoreExpansion.SlotKind.single a) = isFalse ⋯
• Utilities.Subdivision.CoreExpansion.instDecidableEqSlotKind.decEq (Utilities.Subdivision.CoreExpansion.SlotKind.single a) Utilities.Subdivision.CoreExpansion.SlotKind.contracted = isFalse ⋯

@[instance_reducible]

instance Utilities.Subdivision.CoreExpansion.instDecidableEqSlotKind {p✝ : ℕ} : DecidableEq (SlotKind p✝)

Equations

• Utilities.Subdivision.CoreExpansion.instDecidableEqSlotKind = Utilities.Subdivision.CoreExpansion.instDecidableEqSlotKind.decEq

def Utilities.Subdivision.CoreExpansion.kindLength {n p : ℕ} (small : Certificate.SubdivisionGraph.Spec n p) : SlotKind p → ℕ

Length of a big slot forced by its role.

Equations

• Utilities.Subdivision.CoreExpansion.kindLength small Utilities.Subdivision.CoreExpansion.SlotKind.contracted = 1
• Utilities.Subdivision.CoreExpansion.kindLength small (Utilities.Subdivision.CoreExpansion.SlotKind.single j) = small.length j
• Utilities.Subdivision.CoreExpansion.kindLength small (Utilities.Subdivision.CoreExpansion.SlotKind.double j₁ j₂) = small.length j₁ + small.length j₂

theorem Utilities.Subdivision.CoreExpansion.kindLength_pos {n p : ℕ} (small : Certificate.SubdivisionGraph.Spec n p) (k : SlotKind p) : 0 < kindLength small k

def Utilities.Subdivision.CoreExpansion.kindVertex {n p : ℕ} (small : Certificate.SubdivisionGraph.Spec n p) (fallback : Fin n) : SlotKind p → ℕ → small.Vertex

The vertex of the small subdivision sitting at path position q of a big slot with the given role. Positions beyond the slot are clamped, which keeps the definition total and free of transported bound proofs.

Equations

• One or more equations did not get rendered due to their size.
• Utilities.Subdivision.CoreExpansion.kindVertex small fallback Utilities.Subdivision.CoreExpansion.SlotKind.contracted x✝ = small.coreVertex fallback
• Utilities.Subdivision.CoreExpansion.kindVertex small fallback (Utilities.Subdivision.CoreExpansion.SlotKind.single j) x✝ = small.pathVertex j ⟨min x✝ (small.length j), ⋯⟩

theorem Utilities.Subdivision.CoreExpansion.kindVertex_double_le {n p : ℕ} {small : Certificate.SubdivisionGraph.Spec n p} (j₁ j₂ : Fin p) (fallback : Fin n) {q : ℕ} (hq : q ≤ small.length j₁) : kindVertex small fallback (SlotKind.double j₁ j₂) q = small.pathVertex j₁ ⟨min q (small.length j₁), ⋯⟩

theorem Utilities.Subdivision.CoreExpansion.kindVertex_double_gt {n p : ℕ} {small : Certificate.SubdivisionGraph.Spec n p} (j₁ j₂ : Fin p) (fallback : Fin n) {q : ℕ} (hq : ¬q ≤ small.length j₁) : kindVertex small fallback (SlotKind.double j₁ j₂) q = small.pathVertex j₂ ⟨min (q - small.length j₁) (small.length j₂), ⋯⟩

The passive datum

structure Utilities.Subdivision.CoreExpansion.ExpansionData (n p N Q : ℕ) : Type

Passive expansion data. bigCore is the expanded ordered core, fib the fibre map on big core vertices, kind the slot classification, and owner/side the explicit inverse of kind on small slots.

• bigCore : Certificate.ExplicitPotential.Core N Q

  The expanded ordered core.

• fib : Fin N → Fin n

  Which small core vertex a big core vertex collapses onto.

• kind : Fin Q → SlotKind p

  The role of each big slot.

• owner : Fin p → Fin Q

  The big slot carrying a given small slot.

• side : Fin p → Bool

  Whether a small slot is the second half of a double.

def Utilities.Subdivision.CoreExpansion.ExpansionData.SlotCompatible {n p N Q : ℕ} (D : ExpansionData n p N Q) (C : Certificate.ExplicitPotential.Core n p) (e : Fin Q) : Prop

Endpoint compatibility of one big slot with its role.

Equations

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

def Utilities.Subdivision.CoreExpansion.ExpansionData.SlotIndexed {n p N Q : ℕ} (D : ExpansionData n p N Q) (e : Fin Q) : Prop

owner/side really invert kind.

Equations

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

def Utilities.Subdivision.CoreExpansion.ExpansionData.SlotClaimed {n p N Q : ℕ} (D : ExpansionData n p N Q) (j : Fin p) : Prop

Every small slot really is claimed by its recorded owner.

Equations

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

def Utilities.Subdivision.CoreExpansion.ExpansionData.MarkerIsolated {n p N Q : ℕ} (D : ExpansionData n p N Q) (C : Certificate.ExplicitPotential.Core n p) (e : Fin Q) : Prop

The middle vertex of a double is a genuine bivalent marker: it is outside the image of the fibre map, and no other small slot ends there.

Equations

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

def Utilities.Subdivision.CoreExpansion.ExpansionData.Conditions {n p N Q : ℕ} (D : ExpansionData n p N Q) (C : Certificate.ExplicitPotential.Core n p) : Prop

All conditions a usable expansion datum has to satisfy. Every clause ranges over finite types, so the whole conjunction is decidable.

Equations

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

@[instance_reducible]

instance Utilities.Subdivision.CoreExpansion.ExpansionData.decidableSlotCompatible {n p N Q : ℕ} (D : ExpansionData n p N Q) (C : Certificate.ExplicitPotential.Core n p) (e : Fin Q) : Decidable (D.SlotCompatible C e)

Equations

• D.decidableSlotCompatible C e = id inferInstance

@[instance_reducible]

instance Utilities.Subdivision.CoreExpansion.ExpansionData.decidableSlotIndexed {n p N Q : ℕ} (D : ExpansionData n p N Q) (e : Fin Q) : Decidable (D.SlotIndexed e)

Equations

• D.decidableSlotIndexed e = id inferInstance

@[instance_reducible]

instance Utilities.Subdivision.CoreExpansion.ExpansionData.decidableSlotClaimed {n p N Q : ℕ} (D : ExpansionData n p N Q) (j : Fin p) : Decidable (D.SlotClaimed j)

Equations

• D.decidableSlotClaimed j = id inferInstance

@[instance_reducible]

instance Utilities.Subdivision.CoreExpansion.ExpansionData.decidableMarkerIsolated {n p N Q : ℕ} (D : ExpansionData n p N Q) (C : Certificate.ExplicitPotential.Core n p) (e : Fin Q) : Decidable (D.MarkerIsolated C e)

Equations

• D.decidableMarkerIsolated C e = id inferInstance

@[instance_reducible]

instance Utilities.Subdivision.CoreExpansion.ExpansionData.decidableConditions {n p N Q : ℕ} (D : ExpansionData n p N Q) (C : Certificate.ExplicitPotential.Core n p) : Decidable (D.Conditions C)

Equations

• D.decidableConditions C = id inferInstance

theorem Utilities.Subdivision.CoreExpansion.ExpansionData.loopless_of_conditions {n p N Q : ℕ} {D : ExpansionData n p N Q} {C : Certificate.ExplicitPotential.Core n p} (h : D.Conditions C) (e : Fin Q) : D.bigCore.tail e ≠ D.bigCore.head e

theorem Utilities.Subdivision.CoreExpansion.ExpansionData.compatible_of_conditions {n p N Q : ℕ} {D : ExpansionData n p N Q} {C : Certificate.ExplicitPotential.Core n p} (h : D.Conditions C) (e : Fin Q) : D.SlotCompatible C e

theorem Utilities.Subdivision.CoreExpansion.ExpansionData.indexed_of_conditions {n p N Q : ℕ} {D : ExpansionData n p N Q} {C : Certificate.ExplicitPotential.Core n p} (h : D.Conditions C) (e : Fin Q) : D.SlotIndexed e

theorem Utilities.Subdivision.CoreExpansion.ExpansionData.claimed_of_conditions {n p N Q : ℕ} {D : ExpansionData n p N Q} {C : Certificate.ExplicitPotential.Core n p} (h : D.Conditions C) (j : Fin p) : D.SlotClaimed j

theorem Utilities.Subdivision.CoreExpansion.ExpansionData.marker_of_conditions {n p N Q : ℕ} {D : ExpansionData n p N Q} {C : Certificate.ExplicitPotential.Core n p} (h : D.Conditions C) (e : Fin Q) : D.MarkerIsolated C e

theorem Utilities.Subdivision.CoreExpansion.ExpansionData.incident_of_conditions {n p N Q : ℕ} {D : ExpansionData n p N Q} {C : Certificate.ExplicitPotential.Core n p} (h : D.Conditions C) (w : Fin n) : ∃ (j : Fin p), C.tail j = w ∨ C.head j = w

theorem Utilities.Subdivision.CoreExpansion.ExpansionData.fibre_of_conditions {n p N Q : ℕ} {D : ExpansionData n p N Q} {C : Certificate.ExplicitPotential.Core n p} (h : D.Conditions C) (w : Fin n) (T : Finset (Fin N)) (hIn : ∃ a ∈ T, D.fib a = w) (hOut : ∃ b ∉ T, D.fib b = w) : ∃ (e : Fin Q), D.kind e = SlotKind.contracted ∧ D.fib (D.bigCore.tail e) = w ∧ (D.bigCore.tail e ∈ T ∧ D.bigCore.head e ∉ T ∨ D.bigCore.head e ∈ T ∧ D.bigCore.tail e ∉ T)

theorem Utilities.Subdivision.CoreExpansion.ExpansionData.owner_eq_of_single {n p N Q : ℕ} {D : ExpansionData n p N Q} {C : Certificate.ExplicitPotential.Core n p} (h : D.Conditions C) {e : Fin Q} {j : Fin p} (hk : D.kind e = SlotKind.single j) : D.owner j = e ∧ D.side j = false

The owner of a small slot determines the big slot it lives in.

theorem Utilities.Subdivision.CoreExpansion.ExpansionData.owner_eq_of_double {n p N Q : ℕ} {D : ExpansionData n p N Q} {C : Certificate.ExplicitPotential.Core n p} (h : D.Conditions C) {e : Fin Q} {j₁ j₂ : Fin p} (hk : D.kind e = SlotKind.double j₁ j₂) : D.owner j₁ = e ∧ D.side j₁ = false ∧ D.owner j₂ = e ∧ D.side j₂ = true

theorem Utilities.Subdivision.CoreExpansion.ExpansionData.exists_carrier {n p N Q : ℕ} {D : ExpansionData n p N Q} {C : Certificate.ExplicitPotential.Core n p} (h : D.Conditions C) (j : Fin p) : D.kind (D.owner j) = SlotKind.single j ∧ D.side j = false ∨ (∃ (j₂ : Fin p), D.kind (D.owner j) = SlotKind.double j j₂ ∧ D.side j = false) ∨ ∃ (j₁ : Fin p), D.kind (D.owner j) = SlotKind.double j₁ j ∧ D.side j = true

The big slot owning a small slot really carries it, and side records which half.

The expanded specification

def Utilities.Subdivision.CoreExpansion.ExpansionData.bigLength {n p N Q : ℕ} (D : ExpansionData n p N Q) (small : Certificate.SubdivisionGraph.Spec n p) (e : Fin Q) : ℕ

The length assignment on the expanded core forced by the datum.

Equations

• D.bigLength small e = Utilities.Subdivision.CoreExpansion.kindLength small (D.kind e)

theorem Utilities.Subdivision.CoreExpansion.ExpansionData.bigLength_pos {n p N Q : ℕ} (D : ExpansionData n p N Q) (small : Certificate.SubdivisionGraph.Spec n p) (e : Fin Q) : 0 < D.bigLength small e

def Utilities.Subdivision.CoreExpansion.ExpansionData.bigSpec {n p N Q : ℕ} (D : ExpansionData n p N Q) (small : Certificate.SubdivisionGraph.Spec n p) (hN : 0 < N) (hLoopless : ∀ (e : Fin Q), D.bigCore.tail e ≠ D.bigCore.head e) : Certificate.SubdivisionGraph.Spec N Q

The expanded subdivision specification.

Equations

• D.bigSpec small hN hLoopless = Utilities.Certificate.SubdivisionGraph.Spec.ofCore D.bigCore hN hLoopless (D.bigLength small) ⋯

Path terms

def Utilities.Subdivision.CoreExpansion.smallStepTerm {n p : ℕ} (small : Certificate.SubdivisionGraph.Spec n p) (j : Fin p) (a b : small.Vertex) (i : ℕ) : ℕ

The two ordered-endpoint indicators of one unit step of a small slot, written through clamped path positions.

Equations

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

def Utilities.Subdivision.CoreExpansion.kindStepTerm {n p : ℕ} (small : Certificate.SubdivisionGraph.Spec n p) (fallback : Fin n) (k : SlotKind p) (a b : small.Vertex) (i : ℕ) : ℕ

The two ordered-endpoint indicators of one unit step of a big slot, after applying the contraction.

Equations

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

def Utilities.Subdivision.CoreExpansion.slotSum {n p : ℕ} (small : Certificate.SubdivisionGraph.Spec n p) (j : Fin p) (a b : small.Vertex) : ℕ

Total contribution of one small slot.

Equations

• Utilities.Subdivision.CoreExpansion.slotSum small j a b = ∑ i : Fin (small.length j), Utilities.Subdivision.CoreExpansion.smallStepTerm small j a b ↑i

def Utilities.Subdivision.CoreExpansion.kindSlotSum {n p : ℕ} (small : Certificate.SubdivisionGraph.Spec n p) (a b : small.Vertex) : SlotKind p → ℕ

Total contribution of the small slots carried by one big slot.

Equations

• One or more equations did not get rendered due to their size.
• Utilities.Subdivision.CoreExpansion.kindSlotSum small a b Utilities.Subdivision.CoreExpansion.SlotKind.contracted = 0
• Utilities.Subdivision.CoreExpansion.kindSlotSum small a b (Utilities.Subdivision.CoreExpansion.SlotKind.single j) = Utilities.Subdivision.CoreExpansion.slotSum small j a b

Per-slot evaluation

theorem Utilities.Subdivision.CoreExpansion.kindStepTerm_contracted {n p : ℕ} {small : Certificate.SubdivisionGraph.Spec n p} (fallback : Fin n) {a b : small.Vertex} (hab : a ≠ b) (i : ℕ) : kindStepTerm small fallback SlotKind.contracted a b i = 0

theorem Utilities.Subdivision.CoreExpansion.kindStepTerm_single {n p : ℕ} {small : Certificate.SubdivisionGraph.Spec n p} (j : Fin p) (fallback : Fin n) (a b : small.Vertex) (i : ℕ) : kindStepTerm small fallback (SlotKind.single j) a b i = smallStepTerm small j a b i

theorem Utilities.Subdivision.CoreExpansion.kindVertex_double_shift {n p : ℕ} {small : Certificate.SubdivisionGraph.Spec n p} {j₁ j₂ : Fin p} (fallback : Fin n) (hMid : small.core.head j₁ = small.core.tail j₂) (i : ℕ) : kindVertex small fallback (SlotKind.double j₁ j₂) (small.length j₁ + i) = small.pathVertex j₂ ⟨min i (small.length j₂), ⋯⟩

Positions of the second half of a double, shifted past the first half.

theorem Utilities.Subdivision.CoreExpansion.kindSum_eq {n p : ℕ} {small : Certificate.SubdivisionGraph.Spec n p} (fallback : Fin n) (k : SlotKind p) {a b : small.Vertex} (hab : a ≠ b) (hMid : ∀ (j₁ j₂ : Fin p), k = SlotKind.double j₁ j₂ → small.core.head j₁ = small.core.tail j₂) : ∑ i : Fin (kindLength small k), kindStepTerm small fallback k a b ↑i = kindSlotSum small a b k

Sum of the contracted step terms over one big slot, in terms of the small slots it carries.

A two-point indicator sum

Small-side edge count

theorem Utilities.Subdivision.CoreExpansion.numEdges_small_eq {n p : ℕ} (small : Certificate.SubdivisionGraph.Spec n p) (a b : small.Vertex) (hab : a ≠ b) : numEdges small.graph a b = ∑ j : Fin p, slotSum small j a b

Endpoints of a big slot

theorem Utilities.Subdivision.CoreExpansion.kindVertex_zero_single {n p : ℕ} {small : Certificate.SubdivisionGraph.Spec n p} (fallback : Fin n) (j : Fin p) : kindVertex small fallback (SlotKind.single j) 0 = small.coreVertex (small.core.tail j)

theorem Utilities.Subdivision.CoreExpansion.kindVertex_zero_double {n p : ℕ} {small : Certificate.SubdivisionGraph.Spec n p} (fallback : Fin n) (j₁ j₂ : Fin p) : kindVertex small fallback (SlotKind.double j₁ j₂) 0 = small.coreVertex (small.core.tail j₁)

theorem Utilities.Subdivision.CoreExpansion.kindVertex_last_single {n p : ℕ} {small : Certificate.SubdivisionGraph.Spec n p} (fallback : Fin n) (j : Fin p) : kindVertex small fallback (SlotKind.single j) (small.length j) = small.coreVertex (small.core.head j)

theorem Utilities.Subdivision.CoreExpansion.kindVertex_last_double {n p : ℕ} {small : Certificate.SubdivisionGraph.Spec n p} (fallback : Fin n) (j₁ j₂ : Fin p) : kindVertex small fallback (SlotKind.double j₁ j₂) (small.length j₁ + small.length j₂) = small.coreVertex (small.core.head j₂)

The contraction certificate

def Utilities.Subdivision.CoreExpansion.ExpansionData.vertexMap {n p N Q : ℕ} (D : ExpansionData n p N Q) (small : Certificate.SubdivisionGraph.Spec n p) (hN : 0 < N) (hL : ∀ (e : Fin Q), D.bigCore.tail e ≠ D.bigCore.head e) : (D.bigSpec small hN hL).Vertex → small.Vertex

The contraction on subdivision vertices.

Equations

• D.vertexMap small hN hL (Sum.inl v) = small.coreVertex (D.fib v)
• D.vertexMap small hN hL (Sum.inr y) = Utilities.Subdivision.CoreExpansion.kindVertex small (D.fib (D.bigCore.tail y.fst)) (D.kind y.fst) (↑y.snd + 1)

theorem Utilities.Subdivision.CoreExpansion.ExpansionData.vertexMap_coreVertex {n p N Q : ℕ} (D : ExpansionData n p N Q) (small : Certificate.SubdivisionGraph.Spec n p) (hN : 0 < N) (hL : ∀ (e : Fin Q), D.bigCore.tail e ≠ D.bigCore.head e) (v : Fin N) : D.vertexMap small hN hL ((D.bigSpec small hN hL).coreVertex v) = small.coreVertex (D.fib v)

theorem Utilities.Subdivision.CoreExpansion.ExpansionData.vertexMap_interiorVertex {n p N Q : ℕ} (D : ExpansionData n p N Q) (small : Certificate.SubdivisionGraph.Spec n p) (hN : 0 < N) (hL : ∀ (e : Fin Q), D.bigCore.tail e ≠ D.bigCore.head e) (e : Fin Q) (o : Fin ((D.bigSpec small hN hL).length e - 1)) : D.vertexMap small hN hL ((D.bigSpec small hN hL).interiorVertex e o) = kindVertex small (D.fib (D.bigCore.tail e)) (D.kind e) (↑o + 1)

theorem Utilities.Subdivision.CoreExpansion.ExpansionData.vertexMap_pathVertex {n p N Q : ℕ} {D : ExpansionData n p N Q} {small : Certificate.SubdivisionGraph.Spec n p} {hN : 0 < N} {hL : ∀ (e : Fin Q), D.bigCore.tail e ≠ D.bigCore.head e} (hCond : D.Conditions small.core) (e : Fin Q) (q : (D.bigSpec small hN hL).PathPosition e) : D.vertexMap small hN hL ((D.bigSpec small hN hL).pathVertex e q) = kindVertex small (D.fib (D.bigCore.tail e)) (D.kind e) ↑q

The contraction reads off the small path vertex at the same position.

theorem Utilities.Subdivision.CoreExpansion.ExpansionData.vertexMap_stepLeft {n p N Q : ℕ} {D : ExpansionData n p N Q} {small : Certificate.SubdivisionGraph.Spec n p} {hN : 0 < N} {hL : ∀ (e : Fin Q), D.bigCore.tail e ≠ D.bigCore.head e} (hCond : D.Conditions small.core) (e : Fin Q) (i : Fin ((D.bigSpec small hN hL).length e)) : D.vertexMap small hN hL ((D.bigSpec small hN hL).stepLeft e i) = kindVertex small (D.fib (D.bigCore.tail e)) (D.kind e) ↑i

theorem Utilities.Subdivision.CoreExpansion.ExpansionData.vertexMap_stepRight {n p N Q : ℕ} {D : ExpansionData n p N Q} {small : Certificate.SubdivisionGraph.Spec n p} {hN : 0 < N} {hL : ∀ (e : Fin Q), D.bigCore.tail e ≠ D.bigCore.head e} (hCond : D.Conditions small.core) (e : Fin Q) (i : Fin ((D.bigSpec small hN hL).length e)) : D.vertexMap small hN hL ((D.bigSpec small hN hL).stepRight e i) = kindVertex small (D.fib (D.bigCore.tail e)) (D.kind e) (↑i + 1)

The quotient multiplicity equation

theorem Utilities.Subdivision.CoreExpansion.ExpansionData.owner_aggregate {n p N Q : ℕ} {D : ExpansionData n p N Q} {small : Certificate.SubdivisionGraph.Spec n p} (hCond : D.Conditions small.core) (a b : small.Vertex) (e : Fin Q) : kindSlotSum small a b (D.kind e) = ∑ j : Fin p, if D.owner j = e then slotSum small j a b else 0

Regroup the small slots carried by a big slot by their recorded owner.

theorem Utilities.Subdivision.CoreExpansion.ExpansionData.valid_multiplicity {n p N Q : ℕ} {D : ExpansionData n p N Q} {small : Certificate.SubdivisionGraph.Spec n p} {hN : 0 < N} {hL : ∀ (e : Fin Q), D.bigCore.tail e ≠ D.bigCore.head e} (hCond : D.Conditions small.core) (a b : small.Vertex) (hab : a ≠ b) : numEdges small.graph a b = ∑ x : (D.bigSpec small hN hL).Vertex, ∑ y : (D.bigSpec small hN hL).Vertex, if D.vertexMap small hN hL x = a ∧ D.vertexMap small hN hL y = b then numEdges (D.bigSpec small hN hL).graph x y else 0

Quotient multiplicities match exactly.

Shape of the image of an interior position

def Utilities.Subdivision.CoreExpansion.SlotUses {p : ℕ} (k : SlotKind p) (j : Fin p) : Prop

The small slots a big slot carries.

Equations

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

theorem Utilities.Subdivision.CoreExpansion.kindVertex_interior_cases {n p : ℕ} {small : Certificate.SubdivisionGraph.Spec n p} (fallback : Fin n) (k : SlotKind p) {q : ℕ} (h0 : 0 < q) (hq : q < kindLength small k) : (∃ (j : Fin p), SlotUses k j ∧ ∃ (o : Fin (small.length j - 1)), kindVertex small fallback k q = small.interiorVertex j o) ∨ ∃ (j₁ : Fin p) (j₂ : Fin p), k = SlotKind.double j₁ j₂ ∧ kindVertex small fallback k q = small.coreVertex (small.core.head j₁)

theorem Utilities.Subdivision.CoreExpansion.kindVertex_interior_injective {n p : ℕ} {small : Certificate.SubdivisionGraph.Spec n p} (fallback : Fin n) (k : SlotKind p) (hne : ∀ (j₁ j₂ : Fin p), k = SlotKind.double j₁ j₂ → j₁ ≠ j₂) {q q' : ℕ} (h0 : 0 < q) (hq : q < kindLength small k) (h0' : 0 < q') (hq' : q' < kindLength small k) (h : kindVertex small fallback k q = kindVertex small fallback k q') : q = q'

Fibres

theorem Utilities.Subdivision.CoreExpansion.ExpansionData.owner_of_slotUses {n p N Q : ℕ} {D : ExpansionData n p N Q} {small : Certificate.SubdivisionGraph.Spec n p} (hCond : D.Conditions small.core) {e : Fin Q} {j : Fin p} (h : SlotUses (D.kind e) j) : D.owner j = e

theorem Utilities.Subdivision.CoreExpansion.ExpansionData.kind_double_ne {n p N Q : ℕ} {D : ExpansionData n p N Q} {small : Certificate.SubdivisionGraph.Spec n p} (hCond : D.Conditions small.core) (e : Fin Q) (j₁ j₂ : Fin p) : D.kind e = SlotKind.double j₁ j₂ → j₁ ≠ j₂

theorem Utilities.Subdivision.CoreExpansion.ExpansionData.interior_fibre {n p N Q : ℕ} {D : ExpansionData n p N Q} {small : Certificate.SubdivisionGraph.Spec n p} {hN : 0 < N} {hL : ∀ (e : Fin Q), D.bigCore.tail e ≠ D.bigCore.head e} (hCond : D.Conditions small.core) (e : Fin Q) (o : Fin ((D.bigSpec small hN hL).length e - 1)) (y : (D.bigSpec small hN hL).Vertex) (h : D.vertexMap small hN hL y = D.vertexMap small hN hL ((D.bigSpec small hN hL).interiorVertex e o)) : y = (D.bigSpec small hN hL).interiorVertex e o

Fibres over the image of an interior big vertex are singletons.

theorem Utilities.Subdivision.CoreExpansion.ExpansionData.vertexMap_surjective {n p N Q : ℕ} {D : ExpansionData n p N Q} {small : Certificate.SubdivisionGraph.Spec n p} {hN : 0 < N} {hL : ∀ (e : Fin Q), D.bigCore.tail e ≠ D.bigCore.head e} (hCond : D.Conditions small.core) : Function.Surjective (D.vertexMap small hN hL)

The contraction hits every small vertex.

The topological contraction certificate

def Utilities.Subdivision.CoreExpansion.ExpansionData.certificate {n p N Q : ℕ} (D : ExpansionData n p N Q) (small : Certificate.SubdivisionGraph.Spec n p) (hN : 0 < N) (hL : ∀ (e : Fin Q), D.bigCore.tail e ≠ D.bigCore.head e) : Certificate.GraphContractionCertificate (D.bigSpec small hN hL).graph small.graph

The contraction certificate attached to an expansion datum.

Equations

• D.certificate small hN hL = { vertexMap := D.vertexMap small hN hL }

theorem Utilities.Subdivision.CoreExpansion.ExpansionData.certificate_valid {n p N Q : ℕ} {D : ExpansionData n p N Q} {small : Certificate.SubdivisionGraph.Spec n p} {hN : 0 < N} {hL : ∀ (e : Fin Q), D.bigCore.tail e ≠ D.bigCore.head e} (hCond : D.Conditions small.core) : (D.certificate small hN hL).Valid

theorem Utilities.Subdivision.CoreExpansion.ExpansionData.certificate_connectedFibres {n p N Q : ℕ} {D : ExpansionData n p N Q} {small : Certificate.SubdivisionGraph.Spec n p} {hN : 0 < N} {hL : ∀ (e : Fin Q), D.bigCore.tail e ≠ D.bigCore.head e} (hCond : D.Conditions small.core) : (D.certificate small hN hL).ConnectedFibres

theorem Utilities.Subdivision.CoreExpansion.ExpansionData.certificate_topologicalValid {n p N Q : ℕ} {D : ExpansionData n p N Q} {small : Certificate.SubdivisionGraph.Spec n p} {hN : 0 < N} {hL : ∀ (e : Fin Q), D.bigCore.tail e ≠ D.bigCore.head e} (hCond : D.Conditions small.core) : (D.certificate small hN hL).TopologicalValid