A Lean-Checked Rank Census for Pair-Aligned OneTwo Sobol' Projections at m=16

This research note records a reproducible finite rank census for the 345 pair-aligned four-dimensional projections of a pinned version of the OneTwo Sobol’ direction-number table at m = 16, corresponding to 65,536 points. Nine projections have exact t = 4, and the remaining 336 have exact t = 5. The emphasis is on the accompanying Lean-checked computations and an explicit worked certificate, rather than a new construction or algorithm for computing t-values. The OneTwo paper’s reported t ≤ 4 target extends through m ≤ 15; the census here examines the next depth. The registered Lean development checks packed finite predicates for all 345 windows. Their interpretation as matrix-rank and digital-net quality statements, and identification with the released source table, remain outside Lean. We describe this boundary, link the fixed proof source and Palomar record, and identify remaining steps toward a reusable formalization of digital-net certificates.