E.11. Reproduction and boundaries

The portable runtime is the pinned Linux x86-64 Lean 4.34.0-rc2 kit. It is not duplicated inside this source archive. From the extracted release, run

Permalink · Source line 148

The launcher checks file hashes, runs 25 extension-infrastructure tests and the new exact-arithmetic regressions, then builds every module in a new output directory and audits every registered declaration. It also compiles an explicit statement contract and negative controls. The final check verifies the released snapshot again.

The source-policy scan excludes proof placeholders and additional project axioms. Compiler errors, timeouts, missing imports and invalid negative-control preludes are not accepted as successful theorem verification. Failed development snapshots are retained separately from active proof sources.

Permalink · Source line 152

The pinned Mathlib compiled cache is reused, not rebuilt from source. No independent third-party checker or peer review was run. The original numerical experiment suite and Papers I–VIII were not rerun. Prior verification evidence is retained as historical evidence and is not relabeled as fresh testing. The original Paper IX manuscript still requires cumulative supplements and amendments; this extension is not a rewritten primary manuscript.

The external Conjecture 3.9 is distinct from Paper IX's native Conjectures 13.2 and 13.3. Those two remain unproved. The present result does not assert least periods, earliest thresholds, or an optimal exponent for every individual parameter tuple. It makes no historical-priority claim relative to other unpublished work.

Permalink · Source line 157

Yuta Nishibuchi. \(p\)-adic Congruences of Generalized Euler Numbers and Relations to Even Zeta Values. arXiv:2605.10677v2, revised 1 June 2026. Definition 2.1, Conjecture 3.9 and Proposition 3.10. The version identifier is fixed for the statement comparison.

Permalink · Source line 162