The circle value

Closing the standard copairing against the standard form yields the superdimension k − 2ℓ, which is the value Definition 5 gives a free circle.

theorem RS.stdForm_comp_stdCopair (k ℓ : ℕ) : ((stdForm k ℓ).comp (stdCopair k ℓ)).evenMap 1 = ↑k - 2 * ↑ℓ

The circle value (accompanying paper §5.2): the standard form closes the standard copairing to the superdimension k − 2ℓ.