Paper B Reproducibility Evidence Chain for Lifecycle-Aware Isolated-Environment Replay of Proof-Carrying Formal Software

Version 1.2 is an additive publication-state and immutable-tag metadata correction. Raw replay archives and historical verdicts are unchanged. Earlier versions: 10.5281/zenodo.21413981 and 10.5281/zenodo.21416375. Source software: 10.5281/zenodo.21346728. The source tag remains v1.3.0 at commit 13bf095688bcabd5b090f188e9bd28a16237edeb. Replay 1 remains FAIL under K1/v1; Replay 2 remains PASS under K2/v2. No independent reproduction or external validation is claimed. Version 1.2 DOI: 10.5281/zenodo.21420268. Documentation and evidence tables are licensed under CC BY 4.0. New verification scripts are licensed under MIT. Embedded upstream artifacts retain their original licenses. This dataset consolidates the complete evidence chain supporting the methods paper “Lifecycle-Aware Isolated-Environment Replay for Proof-Carrying Formal Software.”It preserves: (1) the first raw replay returning FAIL; (2) canonical evidence normalization without retroactive verdict rewriting; (3) the release-lifecycle temporal oracle and its fixture coverage; (4) exact Lean/Lake and Coq/OCaml environment locks; (5) the second isolated-environment replay returning PASS under contract K2/v2; (6) the versioned contract registry, normalized G00–G20 gate ledger, orthogonal test taxonomy, and threat-to-validity register; and (7) a frozen external AI-mediated replay protocol whose status is NOT YET EXECUTED.The raw G03 failure is preserved separately from the temporal-oracle gate. The first replay remains FAIL, and the second PASS does not overwrite it.Both completed replays were operated by the author in separate fresh environments. Therefore, this record does not claim independent third-party reproduction or external validation.Source software: V0 OSAP Formal Core v1.3.0, commit 13bf095688bcabd5b090f188e9bd28a16237edeb, DOI 10.5281/zenodo.21346728. After downloading the record, run python verify_zenodo_upload.py to validate the archive, evidence checksums, source identity, preserved first-run FAIL, second-run PASS, and external-replay status.