The scalar functional

The descended trace at arity zero evaluates a closed fragment's class to its parameter value: closing against the empty strand bundle is the identity, so the arity-zero trace is evaluation of f itself. This is the numerical endpoint of the extraction: every identity of Hom-classes at arity zero becomes an identity of parameter values through this functional.

noncomputable def RS.pairCloseStrandBundleZero (W : Fragment (Fin (0 + 0))) : Fragment.Equiv (pairClose W (strandBundle 0)) W

Closing a closed fragment against the empty bundle is the fragment.

Equations

• One or more equations did not get rendered due to their size.

theorem RS.traceMap_zero_ofFragment {R : ℕ} (f : EdgeRankParameter R) (W : Fragment (Fin (0 + 0))) : (HomSpace.traceMap f.val 0) (HomSpace.ofFragment f.val W) = f.val W

The scalar functional: the arity-zero descended trace of a closed fragment's class is its parameter value.