{
  "abstract": "This paper deposits the formal closure of the Riemann Hypothesis as one standalone Lean 4 file compiled against Mathlib: 2,189 lines, 123 theorems, 127 compiler-pinned axiom cones, no sorry, no user-declared axiom, and no physical definition or premise. Its 187 declarations are carried, statement and proof byte-identical, from the master file of the author's twin-binder paper, of which it is the formal side. The file binds Mathlib's RiemannHypothesis, by proved biconditionals, to the fixed points of the orthogonal retraction reg(s) = 1/2 + i Im s of ℂ onto the critical line: the hypothesis holds exactly when every nontrivial zero is fixed by reg, exactly when the zero set coincides with its retracted image, exactly when it is contained in that image, exactly when reg is injective on it, and exactly when least erasure transports from the record of the zeros to the zeros, the normal form of the hypothesis. With no premise the file proves the forward pass: the nontrivial zeros are closed under s ↦ 1 − s̄ by the functional equation and Schwarz reflection, lie in 0 ≤ Re s ≤ 1, and are each registered at reg(s) in their lossless, self-verifying record. One bit remains, the look back from the record to the zeros, which the file proves equivalent to reg(s) = s at every nontrivial zero, to the hypothesis, and to the absence of nontrivial zeros from the right half-strip Re s > 1/2 and from the band 1/2 < Re s < 1, and from which RiemannHypothesis follows in one step. The file proves as well that no derivation valid at every reflection-closed configuration, from what those configurations share, yields the value, and that every route to the hypothesis, from any premise, delivers the bit; one theorem with nothing before the colon binds the whole arc. Everything except the bit is proved with no posit, and the hypothesis holds on the look back, at premise grade.\n\nRelease note (the arc of this paper and its twin, 10.5281/zenodo.23357512). A complete formal closure of the Riemann Hypothesis on one bit: comprehensive over every step, universal over every route, and conditional at exactly one place, the look back, where the hypothesis holds at premise grade. The bit is irreducible: nothing the interface shares decides it, and every route delivers it. The formal cargo loop carries everything up to the bit and closes the look back at the record with no premise. At the zeros the bit is posited, and the physical closure supplies it as a witness, from premises printed in its signatures, sealing the hypothesis on the same line.\n\nVersion 1.0.0, 16 October 2026, Math Journal edition, 64 pages. The deposited file RH_Formal_Closure_v1_0_0_CC.lean (2,189 lines, 108,405 bytes, SHA-256 4af02e3365b374623279498b164d3a35d27e0609404c66689f0ff889e147aab3) is attached beside the paper and reproduced verbatim in Appendix D; it compiles under Lean 4.19.0 with Mathlib v4.19.0 with an empty message stream. Appendix E states the closure as the file's theorems. The audit digest and the LaTeX source stand beside the paper in the repository.\n\nThis record carried, until 16 October 2026, A Formal Proof of the Riemann Hypothesis: The Formal Domain as a Self-Verifying Fixed Point (13 October 2026) with the master file RH_Both_Sides_Formal_Master_v3_0_9.lean. The present paper takes its place; both earlier files are kept, byte-identical, in the git repository at FINAL_BINDING/RH Binding/.",
  "abstract_shown": true,
  "affiliations": [],
  "article_type": null,
  "arxiv": null,
  "author_total": 1,
  "authors": [
    {
      "name": "Mohammad F Islam",
      "orcid": "0009-0003-1671-0664"
    }
  ],
  "bibtex": "https://research.draconitic.com/paper/ek4trh2621g83.bib",
  "cited_by": 0,
  "doi": "10.5281/zenodo.23334982",
  "fulltext_url": null,
  "id": "ek4trh2621g83",
  "issns": [],
  "landing_url": "https://zenodo.org/records/23334982",
  "language": null,
  "licence": "CC-BY-4.0",
  "licence_label": "CC BY 4.0",
  "licence_source": "article",
  "licence_url": "https://creativecommons.org/licenses/by/4.0/",
  "metadata_licence": null,
  "native_subjects": [],
  "openalex": null,
  "pdf_url": "https://zenodo.org/api/records/23334982/files/RH_Completed_Formal_Closure_v1_0_0.pdf/content",
  "pmcid": null,
  "pmid": null,
  "published": "2026-10-16",
  "publisher": null,
  "ris": "https://research.draconitic.com/paper/ek4trh2621g83.ris",
  "sources": [
    {
      "first_seen": "2026-10-30T12:17:23Z",
      "native_id": "23334982",
      "source": "zenodo",
      "url": "https://zenodo.org/records/23334982"
    }
  ],
  "subjects": [],
  "title": "The Completed Formal Closure of the Riemann Hypothesis: A Formal Proof in Lean 4 from Its One Bit, Every Other Step Proved, Zero Physics",
  "title_text": "The Completed Formal Closure of the Riemann Hypothesis: A Formal Proof in Lean 4 from Its One Bit, Every Other Step Proved, Zero Physics",
  "type": "preprint",
  "updated_at": "2026-10-30T12:33:21Z",
  "url": "https://research.draconitic.com/paper/ek4trh2621g83",
  "venue": "Zenodo",
  "versions": []
}