# Verification record

Verified on 7 September 2026.

- **Lean:** 4.33.1, commit `819816b2e0a3bf405af45ae5c7af2491d8f5bee6`, Windows x86-64.
- **Mathlib:** v4.33.1, commit `0df444a360eaa60ab8c11dca51a86af692955474`.
- **Complete project build:** `lake --no-cache build` exited with code 0: “Build completed successfully (3426 jobs).” Style-only linter suggestions were emitted; there were no compiler errors.
- **Dependency audit:** `Audit.lean` compiled and exited with code 0.
- **Source scan:** no `sorry`, `admit`, `native_decide`, custom `axiom` declarations, or `unsafe` declarations in the delivered Lean source.
- **Copy integrity:** every delivered source and configuration file was checked byte-for-byte against the built project. `SOURCE-SHA256.txt` records the delivered file hashes.

## Checked final statements

```lean
binaryDisjunctive_E
  (hAGP : AGP) (hSupply : PrimeIntervalSupply) :
  BinaryDisjunctive E

binaryDisjunctive_lambertE
  (hAGP : AGP) (hSupply : PrimeIntervalSupply) :
  BinaryDisjunctive lambertE

every_binary_block
  (hAGP : AGP) (hSupply : PrimeIntervalSupply)
  (length value N : ℕ)
  (hlength : 0 < length) (hvalue : value < 2^length) :
  ∃ shift, N ≤ shift ∧ binaryBlock lambertE length shift = value
```

## Observed transitive axiom audit

```text
'ErdosBorwein.binaryDisjunctive_E' depends on axioms: [propext, Classical.choice, Quot.sound]
'ErdosBorwein.binaryDisjunctive_lambertE' depends on axioms: [propext, Classical.choice, Quot.sound]
'ErdosBorwein.every_binary_block' depends on axioms: [propext, Classical.choice, Quot.sound]
'ErdosBorwein.E_eq_lambertE' depends on axioms: [propext, Classical.choice, Quot.sound]
'ErdosBorwein.binaryBlock_eq_of_wordVisit' depends on axioms: [propext, Classical.choice, Quot.sound]
```

The two external mathematical inputs are explicit theorem arguments, so they appear in the theorem types rather than as custom axioms. Their definitions are printed by `Audit.lean` and explained in the README. The result verified here is the full conditional implication from those estimates to qualitative disjunctivity and arbitrarily late occurrences.

The package contains 18 mathematical modules, the public import module, and the audit file. It does not include compiled dependencies or runtime binaries; Lake retrieves the pinned dependencies.