{"id":"palomar/PALOMAR-2026-09-07-000001","url":"https://github.com/yuningyang19/rerandSRHT_prob_5_6_simons_workshop/tree/158a716c07e16ec4fca14e36836b14d8d20ee7c8","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-07-000001-v1.json","repo":"https://github.com/yuningyang19/rerandSRHT_prob_5_6_simons_workshop","tags":["math.NA","math.PR","msc:65F55","msc:60B20","randomized-linear-algebra","subspace-embedding","numerical-analysis"],"score":0,"title":"Subspace embeddings with the rerandomized SRHT","trust":"high","domain":"math.NA","source":"palomar","authors":["Yuning Yang"],"reviews":0,"subject":"math.NA","summary":"A Lean 4 formalization of a rerandomized SRHT subspace embedding theorem. For every ambient Walsh dimension n = 2^m, rank 1 <= r <= n, and 0 < epsilon < 1, one deterministic width k <= min(n, ceil(C r / epsilon^2)) can be chosen independently of the orthonormal frame. For each fixed frame, the transform with two independent uniform sign layers and an independent uniform k-subset has spectral failure probability at most 1/100, and preserves all squared norms in that subspace within 1 +/- epsilon with probability at least 99/100. C is an explicit universal constant, with no sharp numerical…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-07","reactions":{},"formalized":true,"formalizes":[{"title":"Subspace embeddings with the rerandomized SRHT","identifier":"https://github.com/yuningyang19/rerandSRHT_prob_5_6_simons_workshop/blob/d0276b4b5bb85e25a43e6f677356dd625a19c1d6/research/problem_5_6/formalization/v6_certification/revisions/20260907_positive_dimensions/snapshots/research/problem_5_6/paper/v6/main.tex","relationship":"formalizes"}]}