The converse statement, assembled

The converse of the Regts–Sevenster theorem: every mixed partition function has exponentially bounded edge-connection rank, with base the total dimension k + 2ℓ. This file defines the statement and assembles it from the Eulerian independence of the Definition 5 value (a theorem, eulerianIndependence) and the connection-rank bound, which the super-Gram identity supplies downstream (RS/TheoremConverse.lean). The normalization on the empty graph is proved here: the Definition 5 value of any flagless fragment is (k − 2ℓ) ^ circles.

The value on flagless fragments

theorem RS.mixedPartition_of_flagless {α : Type} (W : Fragment α) [IsEmpty W.Flag] [IsEmpty W.Vertex] {k ℓ : ℕ} (h : MixedFunctional k ℓ) : mixedPartition h W = (↑k - 2 * ↑ℓ) ^ W.circles

The Definition 5 value of a flagless fragment is the circle factor alone.

theorem RS.mixedPartition_empty {k ℓ : ℕ} (h : MixedFunctional k ℓ) : mixedPartition h emptyClosedFragment = 1

The empty-graph normalization: the Definition 5 value of the empty closed fragment is 1.

The converse statement

theorem RS.converseStatement_of_rank_bounded (hInd : EulerianIndependence) (Hrank : ∀ (k ℓ : ℕ) (hf : MixedFunctional k ℓ), EdgeRankBounded (fun (W : ClosedFragment) => mixedPartition hf W) (k + 2 * ℓ)) : RegtsSevensterConverseStatement

Assembly of the converse from the Eulerian-independence input and the connection-rank bound.