D-063 — Pre-submission audit of the NguyenRH1 Lean package
Date: 2026-08-20 | Session: 013 | Task: 5.2 (pre-submission re-audit, user directive) Status: ALL CHECKS PASS. Verdict: package is submission-ready.
Full independent re-audit of the whole package before Paper A circulation. Six stages; every stage passed.
A. Source sweep (all .lean files)
sorrytactics: exactly 5 —SuzukiSkeleton.lean:55(R003_exact_factorization) andValleySkeleton.lean:58,68,83,99(valley_plateau_upper, valley_floor_upper, valley_floor_lower_isolated, valley_profile). All intended skeletons; all other hits are comments.- Forbidden constructs: none — no
admit, noaxiomdeclarations, nonative_decide, nounsafe, no@[implemented_by]. set_option: exactly one —maxHeartbeats 800000oniimaj_bracket_bound(elaborator budget only; kernel checking is unaffected).
B. Clean-room rebuild
.lake/build deleted; lake build NguyenRH1 from empty: 8707 jobs,
build successful (LiSkeleton 46 s, LiBasePoints 22 s, root 15 s).
Warnings: only the 5 intended declaration uses 'sorry' (4 valley +
1 Suzuki).
C. Exhaustive axiom audit (every declaration, not just headline ones)
Mechanically generated PrintAxiomsAll.lean: one #print axioms per
public declaration (139 declarations; private helpers are covered
transitively through the public proof terms).
Result (audit-session013-axioms.txt, archived in the package):
- 134 declarations:
[propext, Classical.choice, Quot.sound]— the three standard axioms only. This includeslambda_pos_finite_height_verified,lambda_pos_finite_height,marginTilde_FAlt_80000_pos,marginTilde_FAlt_80000_lt_100000, all of tier (i), and every numeric bound lemma. - 5 declarations (exactly the intended skeletons): the standard
three +
sorryAx. - Nothing else — no hidden axiom anywhere in the package.
D. Statement-to-paper correspondence (paperA.tex)
| Paper A claim | Lean statement | Match |
|---|---|---|
| Thm R-004: λ_n > 0 for 1 ≤ n ≤ (T₀−1)², T₀ = 3×10¹² | ∀ n : ℕ, 1 ≤ n → (n:ℝ) ≤ (3*10^12-1)^2 → 0 < (liCoeff n).re with liCoeff n = ∑' ρ, (zeroMult ρ)·(1-(1-1/ρ)ⁿ) |
✓ (the paper's λ_n; positivity of the real part per the documented conjugate-symmetry convention) |
| Hypothesis 1: RH verified to T₀ (Platt–Trudgian) | RHUpTo (3*10^12): every nontrivial zero with |Im ρ| ≤ T₀ has Re ρ = 1/2 |
✓ |
| Hypothesis 2: finite Li verification to 5×10⁵ | LiVerifiedUpTo (5*10^5) |
✓ |
| Hypothesis 3 (the one named analytic bound): |S_f(n)| ≤ B(n) on 10⁵ ≤ n ≤ (T₀−1)² | SfBoundProp: ∀ n, 100000 ≤ n → (n:ℝ) ≤ (3·10¹²−1)² → |Sf n| ≤ Bn FAlt n, with Sf n := SInfty n + 1 − (liCoeff n).re (BL Thm 2 by construction, documented) |
✓ |
| Margin evaluations discharged in-development | marginTilde_FAlt_80000_pos (≥ 8001 certified), marginTilde_FAlt_80000_lt_100000 |
✓ |
| Axiom profile / no sorry in the Li chain | per stage C | ✓ |
Note (documented since session 010): the summability of liCoeff's |
||
| zero-side family is part of the contour-identity layer inside | ||
SfBoundProp's eventual proof (the tsum honesty note on the |
||
| definition); the paper's Appendix B is consistent with this reading. |
E. Inherited library (zeta-23-lean, tag v1.0) — re-verified LIVE
All comparator scripts re-run against the existing build:
- 27 main comparator statements: verbatim match with AUDIT.md.
- 16 amendment comparators (ξ′/PairCeiling): verbatim match with the AUDIT.md amendment section.
- 43/43 lines show only the standard axioms (one def-level check shows
[propext]alone); nosorryAxanywhere in the comparators.
F. Artifacts filed
research/lean/NguyenRH1/PrintAxiomsAll.lean(generator script)research/lean/NguyenRH1/audit-session013-axioms.txt(139-line output)
Verdict
The NguyenRH1 package checks out completely: clean-room build green; no sorries outside the 5 declared skeletons; no hidden axioms; the headline theorem's statement is exactly the paper's Theorem R-004 with exactly the three named hypotheses the paper declares. Submission-ready.