The Regts–Sevenster theorem, both directions

The super-Gram identity is a theorem (EdgeSubset.superGramIdentity), so the converse holds with no hypothesis at all: every mixed partition function is an edge-rank-bounded parameter. With it the characterization and the quantitative round trip rest on Deligne alone.

theorem RS.mixedPartition_edgeRankBounded {k ℓ : ℕ} (h : MixedFunctional k ℓ) : EdgeRankBounded (fun (W : ClosedFragment) => mixedPartition h W) (k + 2 * ℓ)

The converse rank bound with the exact total dimension as its base, including the zero-dimensional model.

theorem RS.regts_sevenster_converse : RegtsSevensterConverseStatement

THE CONVERSE (Regts–Sevenster, arXiv:1807.04494, Theorem 6): every mixed partition function is an edge-rank-bounded parameter, with base max 1 (k + 2ℓ).

theorem RS.edgeRankBounded_of_mixedBounded {f : ClosedFragment → ℂ} {B : ℕ} (hf : IsMixedPartitionFunctionBounded f B) : EdgeRankBounded f (max 1 (2 * B))

The rank bound from a bounded mixed partition function.

theorem RS.regts_sevenster_iff (hDeligne : DeligneTheoremStatement) (f : ClosedFragment → ℂ) (hempty : f emptyClosedFragment = 1) (hiso : ∀ (W₁ W₂ : ClosedFragment) (a : Fragment.Equiv W₁ W₂), f W₁ = f W₂) : (∃ (R : ℕ), EdgeRankBounded f R) ↔ IsMixedPartitionFunction f

THE CHARACTERIZATION, conditional on Deligne alone: a fragment parameter has bounded edge rank exactly when it is a mixed partition function.

theorem RS.regts_sevenster_quant_roundtrip (hDeligne : DeligneTheoremStatement) (f : ClosedFragment → ℂ) (hempty : f emptyClosedFragment = 1) (hiso : ∀ (W₁ W₂ : ClosedFragment) (a : Fragment.Equiv W₁ W₂), f W₁ = f W₂) : (∀ (R : ℕ), EdgeRankBounded f R → IsMixedPartitionFunctionBounded f ⌊2 * Real.exp 1 * ↑R⌋₊) ∧ ∀ (B : ℕ), IsMixedPartitionFunctionBounded f B → EdgeRankBounded f (max 1 (2 * B))

THE QUANTITATIVE ROUND TRIP, conditional on Deligne alone: edge rank R gives dimension ⌊2eR⌋, and dimension B gives edge rank base max 1 (2B).