# Reproduction report

## Actual environment

* Ubuntu 24.04.3 LTS, x86_64, glibc 2.39; reported kernel 6.18.35.
* Official Lean 4.19.0 Linux release, commit `6caaee842e94`, Release build.
* Lake 5.0.0-6caaee8, using Lean 4.19.0.
* Mathlib v4.19.0, commit `c44e0c8ee63ca166450922a373c7409c5d26b00b`.
* Python 3.12.14 was used for packaging and report inspection, not as a proof oracle.

Lean was initially absent. Its official release archive and the pinned Mathlib source were downloaded. Mathlib dependencies and compiled library files came from its cache; the project proofs were elaborated and checked locally. This report does not claim that the entire Mathlib source tree was rebuilt locally.

## Container accommodation

This container exposes the running executable through `/proc/self/exe` but did not resolve Lean's `/proc/<getpid()>/exe` lookup. The unmodified official executable initially reported `failed to locate application`. The supplied `scripts/self_exe.c` changes just that `readlink` path to `/proc/self/exe`. It was compiled as a shared library and loaded with `LD_PRELOAD`. It changes executable discovery, not arithmetic, theorem elaboration, the kernel or imported proof terms. Ordinary environments should use the normal commands in README without this shim.

The local wrapper used during this session was:

```bash
export LD_PRELOAD=/tmp/omega-lean-toolchain/self_exe.so
export PATH=/tmp/omega-lean-toolchain/lean-4.19.0-linux/bin:$PATH
exec lake "$@"
```

Mathlib cache extraction also used `TAR_OPTIONS=--no-same-owner`. The initial project `lake update` failed at a ProofWidgets release download. Explicit cache downloads completed successfully, after which the project built. The original setup log is included as `evidence/setup_lake_update.log`; this failed setup command is not presented as a successful proof check.

## Final checks actually performed

| Command in the project directory | Exit status | Result |
|---|---:|---|
| `./scripts/lean_local.sh build` | 0 | Default project target, including all central proof modules, built successfully |
| `./scripts/lean_local.sh env lean Omega/AxiomAudit.lean` | 0 | All 147 project theorem axiom dependencies reported |

The wrapper applies the environment accommodation above. The final reports are `evidence/build.log` and `evidence/axioms.log`. Stylistic linter suggestions about tactic sequencing are present in the build log; there are no build errors or unfinished-proof warnings in that final log.

The 147 reported theorem dependencies contain only `propext`, `Classical.choice` and `Quot.sound`, or subsets of them; some theorems depend on no axioms. No `sorryAx`, external native-evaluation axiom, or project-specific axiom occurs. `scripts/check_axioms.py` verifies the coverage count against the theorem declarations and rejects any other reported axiom.

## Evidence classes

* Analytic, algebraic and inductive proofs: Lean proof terms, checked during local compilation.
* Exact finite certificate: ordinary Lean `decide` computes a Boolean certificate covering all 32,768 states. `certified_gap` proves its interpretation. This is not `native_decide` and is not an imported Python PASS message.
* Concrete exact arithmetic: GCD, inverse, threshold values and witnesses are proved by kernel-reduced decision or proof-producing arithmetic tactics.
* Mathematical-library dependencies: pinned Mathlib, including its proved real π bounds, calculus and linear-algebra results.
* Empirical execution histories: outside this Lean formalization. No codec, timing, workbook or network measurement is certified merely by compiling these files.

The archive supplies the reproducible source, dependency lock, proof guide, axiom audit and successful logs. It does not bundle the compiler or downloaded Mathlib cache. A clean installation on another machine has not been executed in this session; the reproduction commands are supplied for that check. SHA256SUMS identifies the packaged files at release time.