Cubic ordered cores

Occurrence-sensitive incidence degree for an ordered explicit core. Parallel slots are counted separately, and a loop contributes twice. Looplessness is an independent property.

def Utilities.Certificate.ExplicitPotential.Core.incidenceDegree {n p : ℕ} (core : Core n p) (vertex : Fin n) : ℕ

Incidence degree, counting every ordered slot endpoint.

Equations

• core.incidenceDegree vertex = ∑ edge : Fin p, ((if core.tail edge = vertex then 1 else 0) + if core.head edge = vertex then 1 else 0)

def Utilities.Certificate.ExplicitPotential.Core.Cubic {n p : ℕ} (core : Core n p) : Prop

Every vertex has exactly three incident slot endpoints.

Equations

• core.Cubic = ∀ (vertex : Fin n), core.incidenceDegree vertex = 3