Principal divisors on the factors of a two-pole subdivision

The global script restricts to the prescribed factor scripts. At a factor vertex its principal divisor differs from the factor principal divisor only by the outgoing slope of the first connector at its attachment pole. The second connector is constant, so its stored orientation has no effect.

theorem Utilities.Certificate.TwoPoleSubdivision.Data.prin_script_left {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)) (a : (leftSpec s d).Vertex) : (prin s.graph) (script s d f g h) (left s d a) = (prin (leftSpec s d).graph) f a + if a = (leftSpec s d).coreVertex (d.leftPole 0) then h 1 - h 0 else 0

The left principal divisor acquires precisely the outgoing slope of the first connector at the first left pole.

theorem Utilities.Certificate.TwoPoleSubdivision.Data.prin_script_right {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)) (b : (rightSpec s d).Vertex) : (prin s.graph) (script s d f g h) (right s d b) = (prin (rightSpec s d).graph) g b + if b = (rightSpec s d).coreVertex (d.rightPole 0) then h (s.length (d.slots (Sum.inr 0)) - 1) - h (s.length (d.slots (Sum.inr 0))) else 0

The right principal divisor acquires precisely the outgoing slope of the first connector at the first right pole.

The two-pole transfer interface on an actual subdivision

The finite incidence decomposition supplies genuine factor embeddings and a global script. Only the connector interiors lie outside the two factors; their Laplacians are the second differences of the supplied path values.

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

The left subdivision's ordered attachment poles, obtained from the two designated left core vertices.

Equations

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

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

The right subdivision's ordered attachment poles, obtained from the two designated right core vertices.

Equations

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

theorem Utilities.Certificate.TwoPoleSubdivision.Data.prin_script_nonneg_outside {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)) (hConvex : ∀ (j : ℕ), 0 < j → j < s.length (d.slots (Sum.inr 0)) → 0 ≤ h (j - 1) - 2 * h j + h (j + 1)) (z : s.Vertex) (hLeft : ∀ (a : (leftSpec s d).Vertex), z ≠ left s d a) (hRight : ∀ (b : (rightSpec s d).Vertex), z ≠ right s d b) : 0 ≤ (prin s.graph) (script s d f g h) z

def Utilities.Certificate.TwoPoleSubdivision.Data.scriptGluing {n p nA pA nB pB : ℕ} (s : SubdivisionGraph.Spec n p) (d : Data s.core nA pA nB pB) : TwoPole.ScriptGluing (leftSpec s d).graph (rightSpec s d).graph s.graph (leftPoles s d) (rightPoles s d) (s.length (d.slots (Sum.inr 0)))

Finite incidence data realize the abstract path-gluing interface. The interface hypotheses are discharged by actual global firing scripts.

Equations

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