Connection ranks and minimum colour dimension

The natural-valued connection rank is the dimension of the actual connection-map range. Under an edge-rank bound this range is finite, so its natural dimension agrees with its module rank. The minimum colour dimension is the least total colour bound of a representing mixed model; it is zero when no representing model exists.

noncomputable def RS.circlesClosed (c : ℕ) : ClosedFragment

The closed fragment of c free circles.

Equations

• RS.circlesClosed c = (RS.Fragment.circlesOnly c).relabel (Equiv.equivOfIsEmpty Empty (Fin 0))

noncomputable def RS.connectionRank (f : ClosedFragment → ℂ) (t : ℕ) : ℕ

The natural dimension of the connection-map range. It agrees with connection rank whenever the range is finite-dimensional.

Equations

• RS.connectionRank f t = Module.finrank ℂ ↥(RS.connectionMap f t).range

def RS.MixedFunctional.Represents {k ℓ : ℕ} (h : MixedFunctional k ℓ) (f : ClosedFragment → ℂ) : Prop

A mixed functional represents the parameter on every closed fragment, including those with free circles.

Equations

• h.Represents f = ∀ (W : RS.ClosedFragment), f W = RS.mixedPartition h W

noncomputable def RS.minimumColourDimension (f : ClosedFragment → ℂ) : ℕ

The least total colour bound among representing mixed models, with value zero when the set of such bounds is empty.

Equations

• RS.minimumColourDimension f = sInf {d : ℕ | RS.IsMixedPartitionFunctionTotalBounded f d}

structure RS.PrescribedColourBounds (f : ClosedFragment → ℂ) (k ℓ : ℕ) : Prop

The rank and free-circle conditions for prescribed even and odd colour dimensions.

• circle_eq : f (circlesClosed 1) = ↑k - 2 * ↑ℓ

  The free-circle value is the prescribed superdimension.

• rank_bounded : EdgeRankBounded f (k + 2 * ℓ)

  Every connection rank is bounded by the total colour count.