A subdivision split into two factors and two connector slots

The data are finite incidence tables. They contain no divisors or rank hypotheses. The first connector is oriented from the left factor to the right; the second may be stored in either orientation.

Values of an arbitrary script along a slot, extended constantly past its last endpoint. This lets us reuse the existing slot-value Laplacian API.

def Utilities.Certificate.TwoPoleSubdivision.pathValue {n p : ℕ} (s : SubdivisionGraph.Spec n p) (f : firingScript s.graph) (e : Fin p) (k : ℕ) : ℤ

Evaluate a firing script along a slot: coordinate zero is the tail, interior coordinates select subdivision vertices, and coordinates at or beyond the length use the head.

Equations

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

@[simp]

theorem Utilities.Certificate.TwoPoleSubdivision.pathValue_zero {n p : ℕ} (s : SubdivisionGraph.Spec n p) (f : firingScript s.graph) (e : Fin p) : pathValue s f e 0 = f (s.coreVertex (s.core.tail e))

@[simp]

theorem Utilities.Certificate.TwoPoleSubdivision.pathValue_length {n p : ℕ} (s : SubdivisionGraph.Spec n p) (f : firingScript s.graph) (e : Fin p) : pathValue s f e (s.length e) = f (s.coreVertex (s.core.head e))

@[simp]

theorem Utilities.Certificate.TwoPoleSubdivision.pathValue_interior {n p : ℕ} (s : SubdivisionGraph.Spec n p) (f : firingScript s.graph) (e : Fin p) (k : Fin (s.length e - 1)) : pathValue s f e (↑k + 1) = f (s.interiorVertex e k)

theorem Utilities.Certificate.TwoPoleSubdivision.pathValue_compatible {n p : ℕ} (s : SubdivisionGraph.Spec n p) (f : firingScript s.graph) : s.SlotValueCompatible (fun (v : Fin n) => f (s.coreVertex v)) (pathValue s f)

theorem Utilities.Certificate.TwoPoleSubdivision.pathValue_script {n p : ℕ} (s : SubdivisionGraph.Spec n p) (f : firingScript s.graph) : s.slotValueScript (fun (v : Fin n) => f (s.coreVertex v)) (pathValue s f) = f

theorem Utilities.Certificate.TwoPoleSubdivision.pathValue_slope {n p : ℕ} (s : SubdivisionGraph.Spec n p) (f : firingScript s.graph) : s.IsStepSlope f fun (e : Fin p) (k : ℕ) => pathValue s f e (k + 1) - pathValue s f e k

structure Utilities.Certificate.TwoPoleSubdivision.Data {n p : ℕ} (core : ExplicitPotential.Core n p) (nA pA nB pB : ℕ) : Type

An orientation-aware partition of a core into two factors and two slots.

• leftCore : ExplicitPotential.Core nA pA

  The core incidence data of the left factor in the two-pole decomposition.

• rightCore : ExplicitPotential.Core nB pB

  The core incidence data of the right factor in the two-pole decomposition.

• vertices : Fin nA ⊕ Fin nB ≃ Fin n

  The bijection partitioning the original core vertices between the left and right factors.

• slots : (Fin pA ⊕ Fin pB) ⊕ Fin 2 ≃ Fin p

  The bijection partitioning core slots into the two factors' internal slots and the two connector slots.

• leftPole : Fin 2 → Fin nA

  The two left-factor vertices incident to the corresponding connector slots.

• rightPole : Fin 2 → Fin nB

  The two right-factor vertices incident to the corresponding connector slots.

• left_nonempty : 0 < nA
• right_nonempty : 0 < nB
• tail_left (e : Fin pA) : core.tail (self.slots (Sum.inl (Sum.inl e))) = self.vertices (Sum.inl (self.leftCore.tail e))
• head_left (e : Fin pA) : core.head (self.slots (Sum.inl (Sum.inl e))) = self.vertices (Sum.inl (self.leftCore.head e))
• tail_right (e : Fin pB) : core.tail (self.slots (Sum.inl (Sum.inr e))) = self.vertices (Sum.inr (self.rightCore.tail e))
• head_right (e : Fin pB) : core.head (self.slots (Sum.inl (Sum.inr e))) = self.vertices (Sum.inr (self.rightCore.head e))
• tail_first : core.tail (self.slots (Sum.inr 0)) = self.vertices (Sum.inl (self.leftPole 0))
• head_first : core.head (self.slots (Sum.inr 0)) = self.vertices (Sum.inr (self.rightPole 0))
• second_ends : core.tail (self.slots (Sum.inr 1)) = self.vertices (Sum.inl (self.leftPole 1)) ∧ core.head (self.slots (Sum.inr 1)) = self.vertices (Sum.inr (self.rightPole 1)) ∨ core.tail (self.slots (Sum.inr 1)) = self.vertices (Sum.inr (self.rightPole 1)) ∧ core.head (self.slots (Sum.inr 1)) = self.vertices (Sum.inl (self.leftPole 1))

def Utilities.Certificate.TwoPoleSubdivision.Data.leftSpec {n p nA pA nB pB : ℕ} (s : SubdivisionGraph.Spec n p) (d : Data s.core nA pA nB pB) : SubdivisionGraph.Spec nA pA

The left factor retains its own vertices and its five (in the application) internal slots, with the original subdivision lengths.

Equations

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

def Utilities.Certificate.TwoPoleSubdivision.Data.rightSpec {n p nA pA nB pB : ℕ} (s : SubdivisionGraph.Spec n p) (d : Data s.core nA pA nB pB) : SubdivisionGraph.Spec nB pB

The corresponding right factor.

Equations

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

@[simp]

theorem Utilities.Certificate.TwoPoleSubdivision.Data.leftSpec_core {n p nA pA nB pB : ℕ} (s : SubdivisionGraph.Spec n p) (d : Data s.core nA pA nB pB) : (leftSpec s d).core = d.leftCore

@[simp]

theorem Utilities.Certificate.TwoPoleSubdivision.Data.rightSpec_core {n p nA pA nB pB : ℕ} (s : SubdivisionGraph.Spec n p) (d : Data s.core nA pA nB pB) : (rightSpec s d).core = d.rightCore

@[simp]

theorem Utilities.Certificate.TwoPoleSubdivision.Data.leftSpec_length {n p nA pA nB pB : ℕ} (s : SubdivisionGraph.Spec n p) (d : Data s.core nA pA nB pB) (e : Fin pA) : (leftSpec s d).length e = s.length (d.slots (Sum.inl (Sum.inl e)))

@[simp]

theorem Utilities.Certificate.TwoPoleSubdivision.Data.rightSpec_length {n p nA pA nB pB : ℕ} (s : SubdivisionGraph.Spec n p) (d : Data s.core nA pA nB pB) (e : Fin pB) : (rightSpec s d).length e = s.length (d.slots (Sum.inl (Sum.inr e)))

def Utilities.Certificate.TwoPoleSubdivision.Data.left {n p nA pA nB pB : ℕ} (s : SubdivisionGraph.Spec n p) (d : Data s.core nA pA nB pB) : (leftSpec s d).Vertex → s.Vertex

Embed the left factor's subdivision vertices into the full subdivision, preserving core vertices and interior slot coordinates.

Equations

• Utilities.Certificate.TwoPoleSubdivision.Data.left s d (Sum.inl a) = s.coreVertex (d.vertices (Sum.inl a))
• Utilities.Certificate.TwoPoleSubdivision.Data.left s d (Sum.inr ⟨e, k⟩) = s.interiorVertex (d.slots (Sum.inl (Sum.inl e))) k

def Utilities.Certificate.TwoPoleSubdivision.Data.right {n p nA pA nB pB : ℕ} (s : SubdivisionGraph.Spec n p) (d : Data s.core nA pA nB pB) : (rightSpec s d).Vertex → s.Vertex

Embed the right factor's subdivision vertices into the full subdivision, preserving core vertices and interior slot coordinates.

Equations

• Utilities.Certificate.TwoPoleSubdivision.Data.right s d (Sum.inl b) = s.coreVertex (d.vertices (Sum.inr b))
• Utilities.Certificate.TwoPoleSubdivision.Data.right s d (Sum.inr ⟨e, k⟩) = s.interiorVertex (d.slots (Sum.inl (Sum.inr e))) k

@[simp]

theorem Utilities.Certificate.TwoPoleSubdivision.Data.left_core {n p nA pA nB pB : ℕ} (s : SubdivisionGraph.Spec n p) (d : Data s.core nA pA nB pB) (a : Fin nA) : left s d ((leftSpec s d).coreVertex a) = s.coreVertex (d.vertices (Sum.inl a))

@[simp]

theorem Utilities.Certificate.TwoPoleSubdivision.Data.right_core {n p nA pA nB pB : ℕ} (s : SubdivisionGraph.Spec n p) (d : Data s.core nA pA nB pB) (b : Fin nB) : right s d ((rightSpec s d).coreVertex b) = s.coreVertex (d.vertices (Sum.inr b))

@[simp]

theorem Utilities.Certificate.TwoPoleSubdivision.Data.left_interior {n p nA pA nB pB : ℕ} (s : SubdivisionGraph.Spec n p) (d : Data s.core nA pA nB pB) (e : Fin pA) (k : Fin ((leftSpec s d).length e - 1)) : left s d ((leftSpec s d).interiorVertex e k) = s.interiorVertex (d.slots (Sum.inl (Sum.inl e))) k

@[simp]

theorem Utilities.Certificate.TwoPoleSubdivision.Data.right_interior {n p nA pA nB pB : ℕ} (s : SubdivisionGraph.Spec n p) (d : Data s.core nA pA nB pB) (e : Fin pB) (k : Fin ((rightSpec s d).length e - 1)) : right s d ((rightSpec s d).interiorVertex e k) = s.interiorVertex (d.slots (Sum.inl (Sum.inr e))) k

theorem Utilities.Certificate.TwoPoleSubdivision.Data.left_injective {n p nA pA nB pB : ℕ} (s : SubdivisionGraph.Spec n p) (d : Data s.core nA pA nB pB) : Function.Injective (left s d)

theorem Utilities.Certificate.TwoPoleSubdivision.Data.right_injective {n p nA pA nB pB : ℕ} (s : SubdivisionGraph.Spec n p) (d : Data s.core nA pA nB pB) : Function.Injective (right s d)

theorem Utilities.Certificate.TwoPoleSubdivision.Data.disjoint {n p nA pA nB pB : ℕ} (s : SubdivisionGraph.Spec n p) (d : Data s.core nA pA nB pB) (a : (leftSpec s d).Vertex) (b : (rightSpec s d).Vertex) : left s d a ≠ right s d b

def Utilities.Certificate.TwoPoleSubdivision.Data.potential {n p nA pA nB pB : ℕ} (s : SubdivisionGraph.Spec n p) (d : Data s.core nA pA nB pB) (f : firingScript (leftSpec s d).graph) (g : firingScript (rightSpec s d).graph) (v : Fin n) : ℤ

The core potential obtained by reading the left or right firing script according to the vertex partition.

Equations

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

def Utilities.Certificate.TwoPoleSubdivision.Data.values {n p nA pA nB pB : ℕ} (s : SubdivisionGraph.Spec n p) (d : Data s.core nA pA nB pB) (f : firingScript (leftSpec s d).graph) (g : firingScript (rightSpec s d).graph) (h : ℕ → ℤ) (e : Fin p) (k : ℕ) : ℤ

Slot values assembled from the two factor scripts, the supplied first-connector profile, and a constant value at the second left pole on the other connector.

Equations

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

def Utilities.Certificate.TwoPoleSubdivision.Data.script {n p nA pA nB pB : ℕ} (s : SubdivisionGraph.Spec n p) (d : Data s.core nA pA nB pB) (f : firingScript (leftSpec s d).graph) (g : firingScript (rightSpec s d).graph) (h : ℕ → ℤ) : firingScript s.graph

The firing script on the full subdivision assembled from the factor core potentials and connector slot profiles.

Equations

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

theorem Utilities.Certificate.TwoPoleSubdivision.Data.compatible {n p nA pA nB pB : ℕ} (s : SubdivisionGraph.Spec n p) (d : Data s.core nA pA nB pB) (f : firingScript (leftSpec s d).graph) (g : firingScript (rightSpec s d).graph) (h : ℕ → ℤ) (h0 : h 0 = f ((leftSpec s d).coreVertex (d.leftPole 0))) (hL : h (s.length (d.slots (Sum.inr 0))) = g ((rightSpec s d).coreVertex (d.rightPole 0))) (hsecond : f ((leftSpec s d).coreVertex (d.leftPole 1)) = g ((rightSpec s d).coreVertex (d.rightPole 1))) : s.SlotValueCompatible (potential s d f g) (values s d f g h)

theorem Utilities.Certificate.TwoPoleSubdivision.Data.slope {n p nA pA nB pB : ℕ} (s : SubdivisionGraph.Spec n p) (d : Data s.core nA pA nB pB) (f : firingScript (leftSpec s d).graph) (g : firingScript (rightSpec s d).graph) (h : ℕ → ℤ) (hCompat : s.SlotValueCompatible (potential s d f g) (values s d f g h)) : s.IsStepSlope (script s d f g h) fun (e : Fin p) (k : ℕ) => values s d f g h e (k + 1) - values s d f g h e k