Prescribed parity dimensions

The free-circle value fixes the difference of the parity dimensions. The total-dimension theorem therefore bounds both dimensions by any prescribed compatible pair. Extension by zero then gives a model on exactly that pair of colour spaces.

theorem RS.mixedPartition_circlesClosed {k ℓ : ℕ} (h : MixedFunctional k ℓ) (c : ℕ) : mixedPartition h (circlesClosed c) = (↑k - 2 * ↑ℓ) ^ c

A disjoint union of free circles evaluates to the corresponding power of the superdimension.

theorem RS.MixedFunctional.Represents.circle_eq {f : ClosedFragment → ℂ} {k ℓ : ℕ} {h : MixedFunctional k ℓ} (hrep : h.Represents f) : f (circlesClosed 1) = ↑k - 2 * ↑ℓ

Every representing model has superdimension equal to the parameter's free-circle value.

theorem RS.TotalBoundedMixedModel.even_dimension_eq {f : ClosedFragment → ℂ} (M : TotalBoundedMixedModel f (minimumColourDimension f)) : ↑M.k = (↑(minimumColourDimension f) + f (circlesClosed 1)) / 2

The minimum total dimension and free-circle value determine the even dimension of every minimal model.

theorem RS.TotalBoundedMixedModel.half_odd_dimension_eq {f : ClosedFragment → ℂ} (M : TotalBoundedMixedModel f (minimumColourDimension f)) : ↑M.ℓ = (↑(minimumColourDimension f) - f (circlesClosed 1)) / 4

The minimum total dimension and free-circle value determine half the odd dimension of every minimal model.

theorem RS.regts_sevenster_prescribed_deligne_only (hDeligne : DeligneTheoremStatement) (f : ClosedFragment → ℂ) (hempty : f emptyClosedFragment = 1) (hiso : ∀ (W₁ W₂ : ClosedFragment) (a : Fragment.Equiv W₁ W₂), f W₁ = f W₂) (K L : ℕ) : (∃ (h : MixedFunctional K L), h.Represents f) ↔ PrescribedColourBounds f K L

A normalized invariant parameter has a model with prescribed parity dimensions exactly when its ranks and free-circle value satisfy the corresponding bounds, conditional on Deligne alone.