Session 010 — 2026-08-19 — Phase 5: paper completion + honesty audit + Lean

Plan (user-approved)

Phase 5 order: 5.3 (complete paper draft) → 5.4 (honesty audit) → 5.1/5.2 (Lean skeletons + axiom audit).

5.3 — paper draft completed

• Abstract refreshed: three contributions, each with an explicit correctness tag (was: stale "session 008 state" draft).
• Introduction written (state of the art, Weil/Li/Voros framing, three contribution summaries, paper map).
• Background §2 written (Weil-form certificate method: G̃ = P + Q, rank–trace, window ratio R(ψ) with the D-004 definition, ceiling 0.682, D-H/Epstein sanity gate).
• Appendix B (formal verification) written: zeta-23-lean audit status
• four-tier formalization target list.
• References pass: all 12 \cite keys resolve (references.bib).
• Compiles clean with MiKTeX (11 → 12 pp after audit corrections), no warnings, no undefined refs.
• Caught during writing: my first draft invented an R(ψ) formula; replaced with the archived definition (D-004:69). Lesson: paper text must be built from the archive, not memory.

5.4 — full honesty audit (D-060)

Method: claim lists extracted from draft.tex; four independent read-only audit instances, each verifying against the archive with file:line evidence; adjudicated by hand. ~55 claims: 0 unsupported, 10 draft misstatements (all corrected), 7 archive-side defects (errata filed in place).

Draft corrections (all applied, recompiled clean)

1. (1.12)⟺spec(D)⊂ℝ was presented as PROVED; the converse is a SKELETON (L3/L4, D-051). Split in §3.2 + abstract tag. Most serious finding.
2. "triangle window" → flat window ψ₀ = 1_[−½,½] (factual error I introduced in 5.3b; D-002:91).
3. B(n) "+ o(1)" → "+ I_I + 1" (archive bound has explicit remainders, D-037:99).
4. "60 digits" symbolic verification → "verified against 60-digit reference values (E-001)" (json records dps 50).
5. Sanity-gate scope: "every new criterion" → "each of the three main theorems (D-053)".
6. §3.2 Finding 1 depth fit: "Δ ≈ log a + 0.64" was the log-plateau fit; now states Δ(a) = log(2a) + o(1) (theorem) + Δ ≈ 3.33 − 4.76/a (direct fit, D-040) + plateau ratios 0.973–0.997.
7. λ_a "<3×10⁻¹² at a=2" clarified as the D-046 floor-corrected bound on the true λ_a (raw Galerkin values are upper bounds).
8. Detector "measured to 0.9%" → "within 0.02%–2.3% (three of four within 0.5%)"; scope clarified (E-027 at a ∈ {4,8}; a = 12 from E-022/E-024).
9. Appendix floors "≈ 1.04" → measured 0.90–1.26 (E-022b raw).
10. θ-spread "≤ 2.2%" → "at most 2.23%" (E-024 exact); λ₁ "102 digits" → "agrees with closed form to better than 10⁻²⁸ relative".

Archive errata filed (in place, dated, referencing D-060)

• R-004: updated to post-repair state (A = 10.5/B₀ = 48; N₀ = 8×10⁴, margin 16 020; convexity PROVED D-057; overlap 6.25×; H2 digamma now PROVED via D-056).
• D-036 §6: sign erratum — S_∞ correction is −1/(24n) (file's own residual list proves it).
• D-056 title: stale "A = 6.0, B₀ = 40" → 10.5/48 (db row also fixed).
• D-055 F-C + D-058 (L3): "≤ 0.9%" → 0.02%–2.3% (worst case a=4, γ≈51.4).
• D-042 §2: linear-K "1.9a to 0.3%" fit superseded by D-045 (K/(2a) → 1, measured 0.973–0.997; the 0.3% claim fails against the file's own raw values K/a = 1.95–1.99); residual asymptotic Z/(2π), not Z/6.
• D-043 §D: residual "→ Z/6" erratum → Z/(2π) (D-045); qualitative conclusion unchanged.

Audit-side notes

• Suspected envelope/floor contradiction REFUTED: sinc(0) = 1, so the profile envelope at z = γ is ≈ 1 − 1/(2a), matching the floor. Clarifying parenthetical added to draft.
• Residual known limitations now listed in D-060 §4 (M₀ grid-verified; ‖G⁻¹‖‖k‖² ≤ a condition; Mathlib-RKHS claim plausible-unverified; E-027 heights rounded).

5.1/5.2 — Lean (COMPLETE at skeleton stage; D-061)

• No local toolchain → installed elan 4.2.3 (user-approved), pinned leanprover/lean4:v4.33.0-rc2 auto-installed.
• lake exe cache get: Mathlib cache for the pinned rev fetched (8681 files, ~7 GB) — the D-007 deferred-rebuild prerequisite.
• lake build (Zeta23): green, 9010 jobs — D-007's deferred rebuild DONE. Solution/Multiplicity/XiPrime/Challenge all build; sorries only in the trusted comparator challenge files.
• 5.2 verified LIVE: all four comparator PrintAxioms scripts run against the fresh build — every statement (27 comparator + PairCeiling rows) shows exactly [propext, Classical.choice, Quot.sound], matching AUDIT.md verbatim.
• New package research/lean/NguyenRH1/ (tracked; vendored zeta-23-lean untouched, path requires reuse its checkout + Mathlib build):
• LiSkeleton.lean: liCoeff (tsum over IsNontrivialZero with zeroMult), RHUpTo / LiVerifiedUpTo hypotheses (Zeta23 literature-hypothesis style), lambda_pos_finite_height, SInfty + sInfty_lower_bound, C0hat/Hhat/IIMaj/marginTilde (explicit D-056/D-057 constants), marginTilde_convex (parameterized by the smooth N-majorant F with its ψ-block sign hypothesis — the 11-block-table mechanism), chain_rule_sqrt_shift.
• SuzukiSkeleton.lean: xiFun from completedRiemannZeta, Ffactor, suzukiW (deficiency vectors as parameters), sineSkeleton, R003_exact_factorization. The (1.12) reduction is deliberately NOT stated (vacuous-statement trap documented in-file).
• ValleySkeleton.lean: WeilFormData structure, IsKernelDiagonal (nonnegativity only — variational identity is the documented gap), valley_plateau_upper / valley_floor_upper / valley_floor_lower_isolated / valley_profile (sinc(0)=1 let-bound), all conditional on Mathlib's RiemannHypothesis.
• PrintAxioms.lean: task-5.2 audit script; expected at skeleton stage = the three standard axioms + sorryAx per declaration.
• Design decision recorded: NO axiom/opaque declarations anywhere (would violate §5.2); unformalized objects enter as parameters with hypotheses, and unstatable statements are deferred rather than stubbed vacuously.
• Build outcome: lake build green (8706 jobs) — exactly the 9 designed sorry warnings, no errors (two compile iterations: end-ordering; Unicode subscript identifiers; Complex.sin).
• NguyenRH1 PrintAxioms: all 9 declarations show [propext, Classical.choice, Quot.sound, sorryAx] — nothing else. sorryAx = the skeleton marker; 5.2's completion criterion for NguyenRH1 is its disappearance as proofs land.
• Housekeeping: detached cmd /c chains with && died silently once (empty log); single-command detached builds fine, short PrintAxioms runs in foreground. Lean 4 gotchas logged in D-061 §6.

Commits

• 9567ba4: 5.3 paper draft completed.
• c595dfc: 5.4 honesty audit complete (D-060 + corrections + errata).
• (final commit at session end: Lean package + D-061 + STATE/NGUYEN)

Next actions

• Phase 5 continuation options: (i) prove sInfty_lower_bound + marginTilde_convex in Lean (the elementary tier); (ii) E-023b (acb box cover for M₀); (iii) E-021 n = 10⁴ rerun; (iv) paper polish (figures/tables from CSVs).