Bitopological Spaces from Directed Graphs: Extending the Nada Construction to Capture Temporal Irreversibility — Reproducibility and Formalization Bundle

v1.1.1 — Archive pointers made self-consistent. A maintenance release. No mathematical, algorithmic, formalization, or empirical content differs from v1.1.0. The Data and Code Availability section of the manuscript pinned v1.0.0 as “the specific version used in this paper”, and the bibliography entry likewise named version 1.0.0. Both predated the releases that followed, so a reader following either pointer arrived at a snapshot that does not contain the text they were reading. Both now name this release and its version DOI, 10.5281/zenodo.22018146. The DOI was reserved on the Zenodo draft before the manuscript was compiled, so the reference is self-referential rather than merely current: the archived document names the archive that holds it, and no future release can make the statement stale by existing. The concept DOI 10.5281/zenodo.19488414 is unchanged wherever it appears, since it resolves to the latest version by construction. Substantive content, unchanged from v1.1.0 and repeated here for readers arriving at this version directly. Two facts about the construction that earlier versions reported as empirical findings are theorems, and are stated and proved: Theorem 3.11 (base-size duality). For every finite directed graph, |B+| = |B−|, by the Galois duality of formal concept analysis. Corollary: the base-size irreversibility index IB is identically zero, so base-size asymmetry is not a channel of irreversibility, and the two IB rows of the GDP results table are consistency checks rather than measurements. Proposition 3.6 (Alexandrov chain). On a visibility graph the specialization preorder R* is the natural total order, so the Alexandrov base has cardinality exactly n and a single component. The reachability layer is a constant of the construction, not a property of any particular series. Remark on mirror-forced zeros of IC. Mirror invariance holds for the horizontal visibility graph of any monotone series and for any palindromic series under either criterion. It does not hold for the natural visibility graph of every monotone series: (0, 1, 1.5, 10) carries the edge {2,4} without its mirror {1,3}. The formalization status is likewise corrected: the Lean 4 development contains no sorry and declares one explicit axiom, specialization_chain_of_sameComponent, corresponding to the classical McCord–Stong equivalence not yet available in Mathlib. No empirical figure changed at any point in this line: the quantities in the GDP results table are identical to v1.0.1. Files. The complete research compendium — manuscript (PDF and LaTeX source), Lean 4 formalization against Mathlib, R Markdown reproducibility notebook and its rendered output, and the empirical dataset (GDPC1_snapshot.csv) — is bundled as bitopology-nada-v1.1.1.tar.gz, byte-identical to tag v1.1.1 of the source repository. The manuscript PDF is also provided loose for direct reading. Compiled with pdflatex: 30 pages, no overfull or underfull boxes, no missing characters, no unresolved references.