{"id":"palomar/PALOMAR-2026-08-23-000004","url":"https://github.com/DiarHaidary/Nelson-Nguyen-conjecture-upper-bound-palomar/tree/3fdbf2cbb26c10c18bc799fa63fbd3a768f6f0e2","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-23-000004-v1.json","repo":"https://github.com/DiarHaidary/Nelson-Nguyen-conjecture-upper-bound-palomar","tags":["math.NA","math.PR","msc:65F50","msc:60B20","msc:68W20","randomized-linear-algebra","sketching","lean-formalization"],"score":0,"title":"DiarHaidary/Nelson-Nguyen-conjecture-upper-bound-palomar","trust":"high","domain":"math.NA","source":"palomar","authors":["Diar Heidary"],"reviews":0,"subject":"math.NA","summary":"Lean 4 formalization of three sparse oblivious-subspace-embedding results at the Nelson--Nguyen parameter scale: the fully independent signed-hash SparseStack construction, independent uniform signed exact-s columns, and a limited-independence transfer for finite laws whose combined hash-sign selector marginals agree with SparseStack through order 4q. At the stated rounded parameters the selected theorems give failure probability at most delta, with explicit strict bounds s < 1356 q / epsilon and m < 306456 (d + q) / epsilon^2 where those parameter conclusions are packaged. The formalization…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-23","reactions":{},"formalized":true,"formalizes":[{"title":"A Sparse-Fock Proof of the Upper Edge for Fully Independent SparseStack","identifier":"https://github.com/DiarHaidary/nelson-nguyen-sparse-fock/blob/3a8969bfa135b7b5042d7090df992780b8ac567b/paper/nelson_nguyen_sparse_fock_candidate_proof.pdf","relationship":"formalizes"},{"title":"Limited Independence and Uniform Signed Exact-s OSNAP at the Nelson--Nguyen Scale","identifier":"https://github.com/DiarHaidary/nelson-nguyen-sparse-fock/blob/3a8969bfa135b7b5042d7090df992780b8ac567b/extensions/limited-independence-exact-s-osnap/report/limited_independence_uniform_exact_s_osnap.pdf","relationship":"formalizes"}]}