PREPRINT · VERSION 0.6 · 31 OCTOBER 2026
From Source-Bound Proofs to Reproducible Research Artifacts: An NSRW Case Study
Yun Kwansub · 10 pages · CC BY 4.0
Abstract
Formal research depends on more than the availability of a proof file: the file must refer to the intended source definitions, compile against an identified environment, and remain connected to the execution described in a publication. We present the implementation and research use of the NavierStokes Research Workbench (NSRW), organized around a construction-specific investigation of mass and angular histories. The investigation progresses from moment comparisons to actual repair-coefficient positivity and a same-point mass-zero/angular-positive theorem. Its software separates development compilation, fixed-checkpoint replay, archive checking and mathematical interpretation. We describe input identity, fresh external-module generation, binary log preservation and explicit failure boundaries, and analyze actual packaging errors, proof elaboration errors and an archive-preservation loss. A retained replay compiled fourteen external modules after one source-target build. In a separate local check for this manuscript, sixty-four focused software tests passed. These observations establish concrete implementation behavior and a reproducible-input contract, rather than comparative performance or independently reproduced mathematics. The case illustrates how research software can support the discovery and composition of formal consequences while keeping failed experiments and incomplete evidence distinguishable.
Actual failures, specific repairs
Section 6 analyzes documented incidents from the research process.
| Observed incident | Resolution |
|---|---|
| Invalid include option, unavailable dependency, or input outside the source root | Correct the logical module root/search path and compile the dependency in the same run. |
| A redundant tactic and unresolved types in two weighted inequalities | Remove the tactic and provide explicit types; keep the conditional theorem’s premises and conclusion. |
| An earlier replay archive absent from inspected preservation locations | Run a new clean replay with a new identity and preserve its archive; retain the older preservation gap. |
Why exact-rational bounds?
At λ = 10−12, the positive support-weight gap is about 3.84 × 10−18, obtained from a difference of nearby exponentials. Direct positive-series expm1 evaluation avoids that subtraction; exact rational arithmetic and outward dyadic rounding produce explicit, inspectable error bounds.
Already in v0.6: §7.2 reports the 128/256/512 fractional-bit scalar records, error-bound method and software tests. This is the principal addition to the preceding manuscript version.
Subsequent software result: the separate mpmath interval checker checks the same records through a different arithmetic implementation. That later experiment is described on the site, rather than attributed to the published v0.6 manuscript.
Inspect scalar values and exact interval widths · Reproduce the artifacts
Cite this work
Yun, Kwansub (2026). From Source-Bound Proofs to Reproducible Research Artifacts: An NSRW Case Study. Version 0.6. Zenodo. https://doi.org/10.5281/zenodo.23835112
Cite P02 v0.6 · BibTeX
@misc{yun_2026_23835112,
author = {Yun, Kwansub},
title = {From Source-Bound Proofs to Reproducible Research
Artifacts: An NSRW Case Study
},
month = oct,
year = 2026,
publisher = {Zenodo},
version = {0.6},
doi = {10.5281/zenodo.23835112},
url = {https://doi.org/10.5281/zenodo.23835112},
}Official Zenodo export · version-specific DOI. Use the all-versions link to discover later editions.