A syntactic linear step bound

The bound counts primitive syntax operations. A unitary is one node regardless of its matrix dimension or synthesis cost. Since $m(t)$ is bounded by the number of written operation nodes, this is a syntactically linear bound, not a physical complexity claim.