Open Problem TR-01 in the Open Problems in Numerical Linear Algebra repository asks whether a rerandomized SRHT (two sign diagonals and two Walsh transforms) with uniform coordinate sampling gives subspace embeddings of dimension proportional to r/ε² at a prescribed sample size, avoiding the logarithmic obstruction of one-round constructions.

Two normalized real Walsh transforms, two independent Rademacher sign diagonals, and uniform coordinate sampling without replacement define the embedding. The proof controls joint entry cumulants of the transformed projection via connected graph contractions and Walsh character identities, bounding the expected trace of even powers of a product of centered projections. A two-projection decomposition converts trace estimates into control of both spectral edges, and coupling of Bernoulli densities transfers the result to a fixed sample size. A Lean 4 formalization of the prescribed-width theorem and supporting lemmas accompanies the manuscript.

The sample size k=min{n,⌈Cr/ε²⌉} for a universal constant C suffices to preserve all squared norms on each fixed r-dimensional subspace within 1±ε with probability at least 0.99, for every ambient Walsh dimension and all ranks, affirmatively resolving TR-01.