Current task: —

Updated 08-20-2026

D-061 — Phase 5.1/5.2: zeta-23-lean full build + live axiom audit + NguyenRH1 skeleton package

Date: 2026-08-19 | Session: 010 | Tasks: 5.1 (first pass), 5.2 Status: complete (skeleton stage; proofs are sorry by design).

1. Toolchain (this machine, first time)

2. zeta-23-lean build (D-007's deferred rebuild — DONE)

3. Task 5.2 axiom audit — verified LIVE (not just static)

All four comparator PrintAxioms scripts run against the fresh build; every printed line is exactly [propext, Classical.choice, Quot.sound] — matching AUDIT.md verbatim:

4. NguyenRH1 skeleton package (task 5.1, first pass)

Location: research/lean/NguyenRH1/ (tracked; the vendored zeta-23-lean checkout is UNTOUCHED — path requires reuse it and its Mathlib build; nothing downloaded or compiled twice). Toolchain pinned identical (v4.33.0-rc2).

Design rules (honesty):

Inventory (9 statements, all compiling)

LiSkeleton.lean (R-004 / draft §3.1):

Build + audit results

5. What remains for 5.1 (future sessions)

Ordered per draft Appendix B: (i) sInfty_lower_bound + marginTilde_convex (elementary; positivity/interval tactics + the 11-block table); (ii) the traced contour bound inside lambda_pos_finite_height (needs explicit N(T)/S(T)/ζ′/ζ bounds); (iii) valley proofs (need model-space/RKHS infrastructure); (iv) Suzuki factorization proof + the (1.12) statement itself. The finite-height theorem's computational hypotheses (RHUpTo, LiVerifiedUpTo) stay as trusted inputs by design.

UPDATE 2026-08-19 (session 011): tier (i) COMPLETE. chain_rule_sqrt_shift, sInfty_lower_bound, marginTilde_convex all PROVED with PrintAxioms = [propext, Classical.choice, Quot.sound] only (no sorryAx). ~1100 new lines across 10 commits: full support library — bern_term_*, sInf_series_summable, harmonic_lower/upper, oddHarm_eq, sInf_partial_lower (for sInfty); chain-rule package (chain_rule_sqrt_shift_on/sqrt, deriv2_of_hasDerivAt_nhds), psiOf block table (8 blocks with formulas+signs, block_range_bounds), IIMaj as psiTilde with iim_u2_antitone/iimaj_bracket_bound/IIMaj_deriv2_lt, marginTilde_eq_expanded identity, marginExpanded ContDiffOn/ContinuousOn regularity, deriv2 combinators (for marginTilde). Details: research/journal/session-011.md. Remaining: tiers (ii), (iii), (iv). DIVERGENCE FROM D-057 (documented in D-057 §6 and draft.tex Formal verification): the Lean convexity proof uses an 8-block ψ-table plus a separate analytic IIMaj″ bound, not D-057's 11-row table — the F/S_b expansion rows vanish because the Lean theorem is parameterized over F, and B̃₄ is non-concave (bounded directly, ≤ 1.316 < 2, superseding E-029's grid-measured 0.189).

UPDATE 2026-08-20 (session 012): tier (ii) STEP 1 COMPLETE. Per session-012-notes.txt (assembly-first split), lambda_pos_finite_height is now PROVED modulo its named hypotheses — PrintAxioms = 3 standard axioms, no sorryAx anywhere in LiSkeleton.lean. The remaining obligation is isolated as the single named analytic hypothesis SfBoundProp (∀ n ∈ [10⁵, N₁], |Sf n| ≤ Bn FAlt n); the other hypotheses are the computational perimeter (RHUpTo, LiVerifiedUpTo) and two elementary margin evaluations (hbase/hbase2 — discharge plan validated in D-062 §5, execution = tier (ii) step 2). New machinery: FAlt (blockwise ψ-clean Trudgian-shape majorant), Bn, Sf, marginTilde_eq_sub, ψ-blocks #1/#3/#4 with signs, contDiffOn_FAlt, FAlt_psi_neg, pos_of_convex_of_base (MVT) and pos_of_convex_of_two_points (secant; used). Refactor: margin regularity weakened to ContDiffOn (Ioi 1) (FAlt has log-singularities at 0 and 1), chain_rule_sqrt_shift_on generalized to c ≤ 1, unused hmaj dropped from marginTilde_convex. Triage + perimeter decision (Trudgian 2014 N(T)/S(T) inside the trusted perimeter, declared): D-062.

6. Housekeeping notes