Session 011 (2026-08-19) — Task (a): Lean proof tier (i) COMPLETE

User choice at session start: option (a) from STATE.md NEXT ACTION — prove the elementary Lean tier (sInfty_lower_bound, marginTilde_convex, chain_rule_sqrt_shift; D-061 §5 tier (i)).

NOTE: the user's system crashed during the session; a parallel pre-crash instance had already committed chain_rule_sqrt_shift (53cc122) and the Bernoulli term lemmas bern_term_nonneg/bern_term_upper (caf0cb2). This session built on those without duplication; no work was lost.

What was done

sInfty_lower_bound — PROVED (commit 9e2616f)

D-037 §3 archimedean bound S_∞(n) ≥ ½n log n + (C₁−γ/2)n − 4 for n ≥ 20, formalized end-to-end:

bern_term_nonneg/lower/upper (Bernoulli + geometric factorization; upper via 1−(1−x)ⁿ = x·Σ(1−x)ʲ termwise).
sInf_series_summable: O(n²/m²) comparison vs p-series p=2 (honesty note on SInfty's tsum DISCHARGED — summability now proved).
harmonic_lower/upper: the two γ-shifted bounds log M + γ ≤ H_M ≤ log(M+1) + γ, from Mathlib's eulerMascheroniSeq/Seq' strict mono/antitone (NumberTheory/Harmonic/EulerMascheroni.lean).
oddHarm_eq: Σ_{k=1}^K 1/(2k+1) = H_{2K+1} − ½H_K − 1 (induction).
sInf_partial_lower: truncation via Summable.sum_le_tsum with an explicit subtype embedding (oddEmb, junk value at 0).
Assembly: parity cases (n = 2q / 2q+1). The γ/log 2/log π pieces cancel EXACTLY (pure algebra, no decimal estimates); residual log defect n(log(n−1)−log n) ≥ −n/(n−1) (even) / ≥ −1/2 (odd) absorbed by the −4.

marginTilde_convex — PROVED (commit 40c4265)

D-057 margin convexity, formalized end-to-end (~700 new lines):

Chain-rule infrastructure: chain_rule_sqrt_shift_on (localized to Ioi(−1) — the log-blocks' singularity line), chain_rule_sqrt (unshifted, for IIMaj), deriv2_of_hasDerivAt_nhds package.
psiOf functional + the full D-057 11-block table: id, L1, L2, L1², L1·L2, L2², T·L1, T·L2 — ψ-formula + sign proof for each (block_range_bounds: T ≥ 5.4721, L1 ≥ 2 via e² ≤ 7.4721, L2 ≥ 0.6931; #6's sign via L1 ≤ T+1 ≤ T(T−1)/(T−4) reduction).
IIMaj (B̃₄): rewritten as ψ̃(s) = 4.56(s+1)(e^{−as}+e^{−bs}), s = √n, a = 2log2−1/2, b = 2log2 (IIMaj_eq_psiTilde_sqrt); closed-form D1/D2 (hasDerivAt_psiTilde, deriv2_psiTilde); iim_u2_antitone (derivative-negative); iimaj_bracket_bound — factor-monotone split 4.56·[(s+1)/s]·[(b²s+b)e^{−as}]·[1+e^{−s/2}] ≤ 4.56·1.2237·0.2124·1.1099 ≤ 1.316 < 2 (exp bounds via Real.sum_le_exp_of_nonneg, 6–7 terms); IIMaj_deriv2_lt: IIMaj″(n) < 1/(2n) for n ≥ 20.
Assembly: marginTilde_eq_expanded (ring-verified constant/weight bookkeeping, 12 pieces); full ContDiffOn regularity on Ioi 20 + ContinuousOn on Ici 20 (endpoint 20 handled separately); deriv2_add/deriv2_const_mul/deriv2_const_val combinators; final: margiñ″(n) = 1/(2n) − 2ψ_F/(4n) − Σ wᵢψᵢ/(4n) − IIMaj″(n) ≥ 1/(2n) − IIMaj″(n) > 0 via convexOn_of_deriv2_nonneg.
iimaj_bracket_bound needs set_option maxHeartbeats 800000 (the set-variable chains are whnf-heavy).

DESIGN NOTE (user-requested documentation): the Lean proof diverges from D-057's 11-row table: 11 conditions → 8-block ψ-table + separate IIMaj″ bound. Reason: D-057's rows #1–#4 expand the Trudgian F/S_b majorants (the Lean theorem is parameterized over F with hψ as hypothesis, so those rows vanish), and B̃₄ (I_I) is non-concave, so it is excluded from the ψ-machinery and bounded directly by the analytic factor-monotone argument (≤ 1.316 < 2), superseding E-029's grid measurement (0.189). Recorded in D-057 §6 and the paper's Formal verification appendix.

Axiom audit (task 5.2 criterion)

PrintAxioms on ALL new declarations: [propext, Classical.choice, Quot.sound] — NO sorryAx, no new axioms. sorryAx now remains only on lambda_pos_finite_height (tier ii) and the Suzuki/Valley skeletons (tiers iii/iv) — exactly as designed in D-061 §5.

Sorry inventory (NguyenRH1)

LiSkeleton: lambda_pos_finite_height (tier ii — traced contour bound).
SuzukiSkeleton: R003_exact_factorization (tier iv).
ValleySkeleton: 4 statements (tier iii). Tier (i) fully eliminated: chain_rule_sqrt_shift, sInfty_lower_bound, marginTilde_convex all PROVED.

Commits this session

53cc122 chain_rule_sqrt_shift (pre-crash instance) caf0cb2 bern_term_nonneg/upper (pre-crash instance) 9e2616f sInfty_lower_bound PROVED d340188 chain-rule infrastructure (shift_on/sqrt) cef7cf2 block table batches 1–2 6bbbbf7 block table batch 3 eb88ff7 IIMaj machinery (psiTilde rewrite, D1/D2) 3dc3dc7 IIMaj bound (antitone + bracket + IIMaj_deriv2_lt) 1e5cced assembly infrastructure (combinators, marginS) a075b2b marginTilde_eq_expanded + marginExpanded regularity 40c4265 marginTilde_convex PROVED — tier (i) COMPLETE

Lean 4 gotchas encountered (for future sessions)

HasDerivAt.add_const c h adds to the VALUE (f x + c); for precomposition use .comp with ((hasDerivAt_id' x).add_const c) and massage mul_one.
HasDerivAt.mul/add/sub leave Pi.mul_apply/Pi.add_apply forms — simp only [Pi.mul_apply, Pi.add_apply, Pi.sub_apply] at h before convert/exact.
convert h using 2 <;> first | rfl | ring — instance-equality side goals closed by rfl, value goals by ring.
field_simp often CLOSES goals; a trailing ring then errors "no goals" — keep as separate iterations when unsure.
Finset.sum_image hypothesis is Set.InjOn; map named g, summand f.
deriv^[2] (iterate) ≠ deriv (deriv ·) syntactically — show bridges (defeq via iterate unfolding).
(m : ℝ) vs (m.1 : ℝ) on subtypes can explode isDefEq — pin the families explicitly (g :=, f :=) in Summable.of_nonneg_of_le.
one_div x vs x⁻¹ and -a * b vs -(a * b) parse mismatches break rw [Real.exp_neg]/one_div lemmas — insert show rewrites.
Numeric digit-bounds: check products before norm_num (two tight constants had to be loosened: 9.9809→9.9807, 3.9636→3.9635).
set_option maxHeartbeats 800000 in must precede the doc comment, not follow it.

Next actions (session 012 candidates)

(a) tier (ii): the traced contour bound inside lambda_pos_finite_height (big — explicit N(T)/S(T)/ζ′/ζ bounds). (b) E-023b acb box cover for M₀ (removes last grid-verified constant). (c) Paper figures/tables from numerics CSVs. (d) (★) symbol-space opening (D-046 revival condition ii).