English description and human-generated proof of the liveness/convergence properties for the DB version on secondary nodes. For context, in 8.0, this is guaranteed by linearizable read through the shard primary. In 9.0, we will use ClusterTime of the last DDL critical section entry and prove (in words) that the two are equivalent.