From Source-Bound Proofs to Reproducible Research Artifacts: An NSRW Case Study

How can a research repository connect a mathematical construction to an inspectable, reproducible result? This case study examines the Navier–Stokes Research Workbench through its investigation of mass and angular histories, culminating in a same-point mass-zero/angular-positive theorem. It explains exact source binding, fresh external-module compilation, binary failure preservation and fixed-checkpoint replay, using concrete invocation, elaboration and archive-loss incidents. Version 0.6 adds a bounded exact-rational numerical experiment: rigorously rounded exponential and expm1 enclosures for normalized core scalars at 128, 256 and 512 fractional bits. The historical Lean replay, focused software checks and new numerical outputs retain distinct identities. The local full suite reports 645 passed, 3 skipped and 90.53% coverage; this is software validation, not independent mathematical reproduction. No explicit source Profile or numerical mass-zero/J certificate is claimed. Yun Kwansub. Version 0.6, 31 October 2026. Paper/source CC BY 4.0; supporting software MIT. Software archive: https://doi.org/10.5281/zenodo.23381778. Companion mathematical paper: https://doi.org/10.5281/zenodo.23835054. Repository: https://github.com/flamehaven01/NavierStokes-Research-Workbench.