Legged cores: marked points as legs

The marked-moduli organization (PHILOSOPHY.md §1): a marked point is a leg attached at its own vertex of the core, contributing one incidence to valence. The leg construction on the ordered-slot core is a one-slot split — the same combinatorial move as OneEdgeSplitRefinement.splitCore, restated here at the Core level so it can be iterated (the second leg of a two-marked row lands on the once-legged core) and consumed by the closed-orthant machinery, which never sees a Spec.

MarkedCore packages a core with distinguished marked vertices, and LegStable is the maximal-cone condition of M_{g,n}^trop: marked vertices are exactly bivalent in the edge graph (their leg supplies the third incidence) and every other vertex is exactly trivalent.

def Utilities.Certificate.ExplicitPotential.Core.legSplit {n p : ℕ} (core : Core n p) (slot : Fin p) : Core (n + 1) (p + 1)

The leg construction: split slot through a fresh last vertex. The old slot keeps the tail and is redirected into the fresh vertex; the fresh last slot runs from the fresh vertex to the old head. Definitionally the core of OneEdgeSplitRefinement.splitCore (see legSplit_eq_splitCore).

Equations

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

def Utilities.Certificate.ExplicitPotential.Core.legVertexOf {n p : ℕ} (_core : Core n p) : Fin (n + 1)

The fresh vertex carrying the leg.

Equations

• _core.legVertexOf = Fin.last n

@[simp]

theorem Utilities.Certificate.ExplicitPotential.Core.legSplit_tail_old {n p : ℕ} (core : Core n p) (slot edge : Fin p) : (core.legSplit slot).tail edge.castSucc = (core.tail edge).castSucc

@[simp]

theorem Utilities.Certificate.ExplicitPotential.Core.legSplit_tail_last {n p : ℕ} (core : Core n p) (slot : Fin p) : (core.legSplit slot).tail (Fin.last p) = Fin.last n

@[simp]

theorem Utilities.Certificate.ExplicitPotential.Core.legSplit_head_old {n p : ℕ} (core : Core n p) (slot edge : Fin p) : (core.legSplit slot).head edge.castSucc = if edge = slot then Fin.last n else (core.head edge).castSucc

@[simp]

theorem Utilities.Certificate.ExplicitPotential.Core.legSplit_head_last {n p : ℕ} (core : Core n p) (slot : Fin p) : (core.legSplit slot).head (Fin.last p) = (core.head slot).castSucc

theorem Utilities.Certificate.ExplicitPotential.Core.legSplit_eq_splitCore {n p : ℕ} (source : SubdivisionGraph.Spec n p) (slot : Fin p) : OneEdgeSplitRefinement.splitCore source slot = source.core.legSplit slot

The leg construction agrees with the one-slot split refinement's core.

theorem Utilities.Certificate.ExplicitPotential.Core.legSplit_loopless {n p : ℕ} (core : Core n p) (slot : Fin p) (hLoopless : ∀ (edge : Fin p), core.tail edge ≠ core.head edge) (edge : Fin (p + 1)) : (core.legSplit slot).tail edge ≠ (core.legSplit slot).head edge

Splitting preserves looplessness.

theorem Utilities.Certificate.ExplicitPotential.Core.legSplit_connected {n p : ℕ} (core : Core n p) (slot : Fin p) (hConnected : core.Connected) : (core.legSplit slot).Connected

Splitting preserves cut connectedness.

structure Utilities.Certificate.ExplicitPotential.MarkedCore (n p k : ℕ) : Type

A core with distinguished marked vertices — the combinatorial datum of a marked tropical curve. k is the number of marked points; each mark is a leg attached at marks i.

• core : Core n p

  The finite edge core to which the marked legs are attached.

• marks : Fin k → Fin n

  The core vertex carrying each marked leg; injectivity and valence conditions are imposed by LegStable.

def Utilities.Certificate.ExplicitPotential.MarkedCore.LegStable {n p k : ℕ} (C : MarkedCore n p k) : Prop

Maximal-cone stability: marks are pairwise distinct, marked vertices are exactly bivalent in the edge graph (the leg is the third incidence), and every unmarked vertex is exactly trivalent.

Equations

• C.LegStable = (Function.Injective C.marks ∧ (∀ (i : Fin k), C.core.incidenceDegree (C.marks i) = 2) ∧ ∀ (v : Fin n), (∀ (i : Fin k), C.marks i ≠ v) → C.core.incidenceDegree v = 3)

def Utilities.Certificate.ExplicitPotential.MarkedCore.legStableCheck {n p k : ℕ} (C : MarkedCore n p k) : Bool

Exact Boolean check for LegStable.

Equations

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

@[simp]

theorem Utilities.Certificate.ExplicitPotential.MarkedCore.legStableCheck_eq_true_iff {n p k : ℕ} (C : MarkedCore n p k) : C.legStableCheck = true ↔ C.LegStable