OMEGA NAUGHT — Lean 4 geometric-provenance formalization (hosted inventory)

This directory is not an eighth source paper, not a joining theorem, and not
peer review. Independent third-party reproduction of Papers I–VII remains none.
Frozen G6 bytes are unchanged.

Status on this archive (12 September 2026):
  Lake package omega_provenance v0.1 is hosted, including Omega.lean,
  twelve Omega/*.lean modules plus Omega/Metrics.lean, lakefile.lean,
  lean-toolchain, evidence logs, and SHA256SUMS.
  Hosted source bytes match the package SHA256SUMS exactly.
  scripts/check_axioms.py PASS on the author axioms.log: 147 theorem reports;
  axioms {Classical.choice, Quot.sound, propext}. That checker is not a
  proof oracle.
  lake build has not been run here. Lean 4 is not installed on this archive.
  Author evidence/build.log reports a prior successful lake build; that is
  not a kernel-check performed on this site.

ZIP SHA-256 stated in the Word transcription (ZIP itself not hosted):
  f77f83d0edd127b5377f7c796963ec9d0cb5610bae14116361b9c6aec8437178
  29 files, 98,418 UTF-8 bytes. Sources recovered from
  LEAN_Proof_Complete_Final.docx and verified against SHA256SUMS.

Author-stated main result:
  Omega.central_provenance_theorem in Omega/Main.lean
  Lean 4.19.0 (leanprover/lean4:v4.19.0); Mathlib commit c44e0c8
  Selected measurement, not uniqueness among all measurements of an unmarked outline.

Claim boundary:
  The construction and its selected measurement rule are explicit inputs.
  The stated conclusion is that this rule yields G = a phi, C = a pi, and
  the finite floor table on D = {0,...,32767}.
  It does not assert uniqueness of the measurement among all possible
  measurements of an unmarked outline.
  Outline length a(2 pi - epsilon) + 2 a phi^2 is strictly larger than
  W = a(phi + pi); the two quantities are never identified.
  Frozen SRSD v1.0 is used only as the scalar quotient-residual interface.
  Cubature, codec, workbook, and Machin-series proof routes are outside
  this formalization.

See SHA256SUMS for package file digests.
See check_axioms.runtime.txt for the named Python inventory run.

Status on this archive (13 September 2026):
  lake build PASS on a byte copy of the hosted sources.
  Lean 4.19.0 (commit 6caaee842e94), Lake 5.0.0-6caaee8, Mathlib v4.19.0
  (commit c44e0c8ee63ca166450922a373c7409c5d26b00b).
  Fresh transcript: evidence/current/build.log
    1,960 bytes, SHA-256 ddc10580b76d0dd4ec8d9012bf91a78338fc43c003c4f7dbab2421f3c2b760b9
    Ends with "Build completed successfully." Modules were Built, not Replayed.
  Fresh axiom audit: evidence/current/axioms.log
    11,804 bytes, SHA-256 82dae0644b5ce591c3e4af7bf9fdbfa6aeec11591560cb785ab0727a65d8eda1
    Byte-identical to the author evidence/axioms.log.
    147 theorem reports; axioms {propext, Classical.choice, Quot.sound}.
    Four theorems depend on no axioms.
  scripts/check_axioms.py PASS on the current log.
  Hosted Omega.lean and Omega/*.lean: zero sorry, admit, or native_decide.
  Toolchain and .lake cache are not hosted.
  That kernel-check is machine-checking of the selected maps in this package.
  It is not peer review of Papers I–VII and not independent reproduction of
  those papers. Cubature 10–21 remains unpackaged. The 117 exact f=23,24
  coefficient pairs are not hosted. Frozen G6 bytes are unchanged.

See evidence/current/ENVIRONMENT.json for the run record.
See evidence/current/SHA256SUMS for current-transcript digests.