Sampling and numerical methods

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

ORCID

Research notev2.0.0

Abstract

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.

Read manuscript PDF ↗Cite this paperDownload BibTeX

Contribution

Records a reproducible 345-window census at 65,536 points and states the boundary between checked predicates and digital-net interpretation.

Formalization scope

partial

What Lean checks

The registered development kernel-checks packed finite predicates for the 345 pair-aligned windows of a pinned OneTwo table at m = 16, the 9/336 distribution, and the worked dimensions 25–28 certificate. Version 2 retains the same registered Lean source while clarifying its interpretation boundary.

What it does not check

The semantic bridge from packed row-reduction predicates to mathematical matrix rank, the digital-net rank criterion and discrepancy consequences, and authentication of the released source table remain outside Lean. The ancillary depth-15 census and protected-pair audit are not compared. Version 2 does not claim a fresh completed Lean build. This narrower statement from the current manuscript takes precedence over older repository wording.

This scope is reconciled with the hosted manuscript and pinned project README. The mathematical statements and assumptions in the source determine what the formalization establishes; manuscript revisions may clarify the interpretation of the same proof artifact.

Toolchain
leanprover/lean4:v4.32.0
Reproduce the formalization
git clone https://github.com/lennrt/palomar-formalizations.git
cd palomar-formalizations
git checkout 9437c5e5ba09d6ba95285eaac4532414a84923e1
cd zenodo-21925582/palomar
lake exe cache get
lake build

See the project README for the complete setup, dependencies, and selected declarations.

Citation & version

Lennart Rudolph. (2026). A Lean-Checked Rank Census for Pair-Aligned OneTwo Sobol' Projections at m=16. v2.0.0. Zenodo. https://doi.org/10.5281/zenodo.22760649.

View and copy BibTeX
Download .bib

Hosted manuscript
v2.0.0 ·
All versions DOI
10.5281/zenodo.21925581

The repository and linked OpenAlex record reference 10.5281/zenodo.21925582. The local PDF and citation here describe v2.0.0, identified by its version DOI above.

Version history

  • v1.0.0 · · available from Zenodo

    Earlier title: Exact Projection Quality of OneTwo Sobol' Sequences at 65,536 Points

  • v2.0.0 · · hosted here
Manuscript file integrity

SHA-256 of this exact hosted PDF:

468144d247fd0015104c8d60bab5824705ea88d97c2ff438359b0a6c56db4c74