PROJECT: NGUYEN-RH-1

The Riemann Hypothesis Challenge — Autonomous Agent Research Blueprint

Created: [08-17-2026] | Status: ACTIVE | Version: 1.0

1. MISSION STATEMENT

Prove (or make maximal rigorous progress toward) the Riemann Hypothesis: all nontrivial zeros of ζ(s) satisfy Re(s) = 1/2. Primary launchpad: the Anthropic paper proving ≥ 2/3 of zeros are simple and on the critical line, unconditionally.

2. RESOURCE MANIFEST

3. KEY KNOWNS (inherited state of the art)

• ≥ 2/3 zeros simple & on line; ≥ 5/6 distinct [R2, unconditional].
• Montgomery–Taylor window: 0.6725 / 0.83625; window-class optimum.
• Bandwidth-one certificate ceiling ≈ 0.682 [R2 §7.2].
• Weil positivity on all of C²_c(ℝ) ⟺ RH [Weil, Bombieri].
• Negative index of truncated Weil form counts off-line pairs [Bom00].
• Obstruction map: X ≫ T needs prime-pair info; higher moments need Rudnick–Sarnak X^k ≤ T^{2−ε}; HL*(∞) ⟹ 100% but not RH itself.
• Any proof must FAIL for Davenport–Heilbronn / Epstein zeta (sanity gate — these violate RH-analogues).

4. ATTACK TRACKS

• A. Certificate extension (moments, windows, SDP, prime pairs)
• B. Spectral / Hilbert–Pólya (quantum formalism from R1; Gabor frame ↔ self-adjoint operator; Berry–Keating; de Branges)
• C. Positivity criteria (Weil growing support, Li coefficients, de Bruijn–Newman Λ = 0)
• D. Formal verification (Lean 4 skeletons for every lemma)

4A. KNOWLEDGE INTEGRATION & EXTERNAL RESEARCH (STANDING ORDER)

Goal reminder: solve RH by COMBINING all knowledge at our disposal.

1. Use the full equation inventory. Every attack must actively consider the complete toolset — quantum formalism (R1), analytic number theory (R2, R4), spectral theory, random matrix theory, physics equations (physics.info) — and seek cross-domain combinations, never stay inside a single track by default.
2. Cross-pollination check. Before abandoning any approach, ask: which OTHER track's machinery could close this gap? Log cross-track ideas in the session journal even when not pursued.
3. Web research before obstruction. When knowledge is missing, research the web (arXiv, surveys, MathOverflow, LMFDB, OEIS) BEFORE declaring a dead end. Record every external source used — URL, what was taken, date — in the derivation/result file; paper-worthy sources go to references.bib.
4. Master tool index. research/derivations/D-001 (built in Phase 0.1) is the living index of all usable equations/tools; every newly discovered tool is added there so no later session rediscovers it.
5. NO-BOUNDARIES RULE (user directive, 2026-08-17). Do not merely follow what has been done. The metric is success on the ultimate goal, not fidelity to any tradition. Actively import ANY domain of human knowledge that could crack a wall in the obstruction map (D-006 §6) — no field is off-limits. Candidate reservoirs to sweep systematically: random matrix theory & free probability; operator theory (de Branges, Krein, canonical systems); harmonic analysis (uncertainty principles, restriction theory, Beurling–Malliavin); mathematical physics (integrable systems, quantum chaos, scattering); probability (Gaussian processes, determinantal point processes); algebraic geometry & finite fields (Weil's proof for curves — the ONE case RH is proven); p-adic and adelic methods; ergodic theory; information theory; optimization (SDP/SOS hierarchies); machine-assisted discovery. At each phase boundary, run a DOMAIN SWEEP: list the current walls, ask which untouched field has machinery shaped like each wall, web-research the top candidates (per §4A.3), and log findings in D-001 Part III — including negative ones (a field that provably does not apply is documented progress).

5. PROJECT PLAN & CHECKLIST

⚠ THE PLAN IS NOT CONCRETE. This is research: the plan and checklist may be updated, extended, reordered, or pruned at ANY time as results demand. Never follow the checklist at the expense of the ultimate goal — solving the Riemann Hypothesis. If a promising direction appears that is not in the plan, the plan changes, not the direction. All plan changes are committed to git with a one-line rationale.

✅ PHASE 0 — Initialization & Ingestion (COMPLETE 2026-08-17)

• [x] 0.1 Parse notes.txt; index all quantum equations for Track B.
  • → research/derivations/D-001 (living master tool index, Part I done)
• [x] 0.2 Deep-read Anthropic paper; reproduce chain (1.2) line by line.
  • → D-002 (statements/notation), D-003 (zero side), D-004 (prime side), D-005 (linear algebra + chain), D-006 (sharpness/ceiling + Lean)
• [x] 0.3 Reproduce Lemma 3.2 (rank–trace) proof independently.
  • → research/derivations/D-005 (all four loss-points mapped; equality case confirmed)
• [x] 0.4 Verify R(ψ₀) = 4/3 and R(ψ_MT) = ½ + (1/√2)cot(1/√2) symbolically.
  • → E-001 (sympy + mpmath, 60-digit): both PASS. Caught a hand-arithmetic slip in D-004 (correct: R(ψ_MT) = 1.32749930, 2−R = 0.67250070).
• [x] 0.5 Clone/inspect zeta-23-lean structure; confirm axiom audit.
  • → D-007 (cloned at v1.0=3635e74; static audit consistent with AUDIT.md: 0 real axioms, sorries only in trusted challenge stubs; full lake rebuild deferred to Track D)
• [x] 0.6 Numerical sandbox: compute first 10⁴ zeros; build finite G̃; confirm tr, ‖·‖²_HS, inertia predictions empirically.
  • → E-002 (10⁴ zeros @ dps 25, all checks pass), E-003 (finite G̃ at T=1000/2000/4000, both windows: tr≈N to 0.1%, HS²/N tracks R(ψ) with O(1/L) decay as Thm 5.7 predicts, PSD confirmed). Summary: D-008.

✅ PHASE 1 — Master the Ceiling (Track A groundwork) (COMPLETE 2026-08-20 — decision gate 1.5/D-013: NO within current data class, Track A → monitoring mode; 1.2 closed as deferred)

• [x] 1.1 Re-derive the bandwidth-one ceiling ≈ 0.682; identify every inequality that is not tight.
  • → D-009 (ceiling re-derived from kernel-checked Lean; inventory: 4 chain losses, 4 ceiling losses, 3 structural gaps; zero-density route RULED OUT with reason; new candidate: multiple-zero bounds as extra chain constraint — not ceiling-constrained)
• [x] 1.2 Test window families beyond C²[−½,½]; SDP over certificates (CGdL20 style) numerically. → CLOSED-DEFERRED by decision (calibration value only; E-005 testbed already provides CMS machinery; D-013 rationale)
• [x] 1.3 Investigate third moment tr G̃³ paths: what fragment of [Hej94, RS96] survives unconditionally?
  • → ANSWER: none usefully. D-011 (wall: availability λ≤2/k vs cap λ)
  • E-005 (model-decisive) → G-002. Moment ladder CLOSED both sides.
• [x] 1.4 Attempt any unconditional support-(1+δ) form-factor result.
  • → D-012: none exists; missing input located EXACTLY (prime pairs at lag h ≲ X/T). Literature logged (D-001 Part III).
• [x] 1.5 DECISION GATE: is > 2/3 achievable in this framework? Document.
  • → D-013: NO within current data class; 6-wall map (W1–W6); necessary conditions for any fix; routes ranked. Track A → monitoring mode; proceed to Tracks B/C.
• [x] 1.6 ξ′-world bandwidth-one ceiling (LawN256 analogue) (NEW, 2026-08-18 regroup).
  • → ANSWER: saturated. E-020b/D-030: window-class optimum for kernel D₁ = 0.86864 to 1e-6 — the paper's quartic window IS optimal (control recovers MT 1.32749930 to 1.7e-7). The perfect-square node buys ~0 headroom beyond the paper's window; nothing transfers to ξ. Adversary-side LP (E-020) documented as machinery limitation (finite pool can't realize the extremal adversary).
• [x] 1.7 T4b scoping (NEW, 2026-08-18 regroup).
  • → CLOSED with rationale (D-031): the mechanism iterates formally (prime polynomial degree k → k nodes; ξ″ leading-order ≈ 0.94), but (i) certificates certify ξ⁽ᵏ⁾ zeros only, (ii) the G-001 substitution symmetry caps every ξ⁽ᵏ⁾ data class below 100%, so the Speiser/Levinson–Montgomery route to RH is closed at every derivative order, (iii) cost per derivative is high. Revival condition noted (ξ-side input route or Suzuki-line need).

🔶 PHASE 2 — Spectral Program (Track B) (MAPPED TO EXHAUSTION at current technology, 2026-08-19 — parked: 2.2/2.3/2.5 unprioritized; live remainder: 2.9 (L1, L3/L4 skeleton) → Paper B / post-publication)

NOTE (2026-08-18 regroup): the Suzuki finite-interval operator program (spawned by 3.4c) IS the live realization of this phase — Suzuki's T_a is a canonical-system / de Branges-type construction (2.4), its Galerkin realization is a validated ⟨ψ|Ĥ|ψ⟩ model (2.1), and Suzuki Cor 1.6 gives an explicit RH-equivalent convergence target (success criterion #3). Items 2.6–2.8 are the active queue; 2.2/2.3 remain open, unprioritized.

• [~] 2.1 Map Weil form W to candidate quadratic forms ⟨ψ|Ĥ|ψ⟩ using R1 operator formalism (self-adjointness ⟺ real spectrum ⟺ RH).
  • → PARTIAL: Suzuki A_a Galerkin = validated Weil-form operator (ledger #1; E-009a/b, D-019). General Ĥ construction: open.
• [ ] 2.2 Analyze Berry–Keating Ĥ = ½(x̂p̂+p̂x̂) with boundary regularizations; compare counting function to N(T). (untouched)
• [ ] 2.3 Exploit paper's Lemma 2.1 (Poisson–Gabor, critical density h = 2π/L, no aliasing) as a frame for an operator model. (untouched)
• [~] 2.4 Examine de Branges space / canonical system reformulation.
  • → ACTIVE via Suzuki line: Q-S2 (ℋ(T_a) as de Branges-type space, D-019); W(a,θ;z) all-real zeros (Thm 1.5) + exact interlacing measured (E-014 H1, E-016 F1).
• [ ] 2.5 DECISION GATE: any genuine self-adjoint realization? Document.
• [x] 2.6 (Q-S3c remainder) Root-cause E-016 V3 Herglotz reconstruction mismatch.
  • → RESOLVED (E-016b/E-016c, D-025): TWO recon-side defects, analytic side exact (V6: direct float64 vs dps-50 ≤ 4.4e-15 to y=40). (i) Galerkin W has a double zero at z≈0 (pair ±iε, ε~2–6e-9 — Galerkin artifact vs Thm 1.5; found by NEW winding-excess diagnostic; explains D-024 F3 "defect at the origin"); (ii) EM tail had a spurious factor y (predicts the y=20 deficit EXACTLY at both a=4 and a=10). Candidates (a)/(c) refuted. V3 REPAIRED: V3R 1.99e-5 (a=4), 1.46e-5 (a=10) vs 0.02 threshold. E-016 F1–F4 stand. Remaining: small-y-weighted θ-metric (folds into 2.8).
• [x] 2.7 (Q-S3a, analytic) Prove/disprove v±(a,·) → A_∞^{−1}e^{±·} in a norm that controls W on compacts.
  • → ANSWERED STRUCTURALLY (D-026, R-003, E-017/D-027): the question is REPLACED by an EXACT factorization W = F·(R₀ + R_τ), F = z²ξ/ξ′, with R₀ = 2e^{a+iθ/2}sin(az−θ/2) + o(eᵃ) closed form. Cor 1.6 ⟺ (★): tail R_τ cancels the sine skeleton up to a zero-free remainder — a finite-interval Wiener–Hopf remainder estimate on the symbol ĝ = z⁻²ξ′/ξ (RH-gated factorization). Explains ALL measured phenomenology incl. the origin double zero. E-017: (★) already ~99.8% complete OFF the real axis at a=4; θ=π preferred quantitatively (4.7% vs 6.8%); transition = cancellation descending to ℝ. Open content isolated: (★) on ℝ.
• [x] 2.8 (Q-S3b, numerics) Prime-sum backend redesign → a ~ 12–14; track θ=π zero flow; test z₁·a ≈ 4.5 stiff law vs limit.
  • → COMPLETE at a=12 (E-018/E-019, D-028/D-029): backend v2 (blockwise Λ, e²⁴, validated 2.2e-7) built; descent profile shows (★) strip-uniform (~5–7e-3); a=12 zero-flow: maximal lattice (1145/1146), stiff law z₁·a = 4.495, lattice STIFFENS (gap CV ↓), origin pair persists (+2.0000 winding excess), no non-real zeros, envelope stationary. NO transition at a ≤ 12 — question answered; a=13+ deprioritized by evidence (revivable in ~30 min via backend cache). Key structural gain (D-028): the open content of Cor 1.6 is the zero set of M, not its envelope. [ERRATUM 2026-08-19, D-043 §C: the "γ-proximity chance-level" claim is RETRACTED — wrong-direction metric; correct metric shows quadratic positional locking ~0.65/a².]
• [~] 2.9 (★) analytic attack (NEW, 2026-08-18; design D-034/D-035 complete). Resolvent-convergence route: prove v±(a)→v±(∞) in the Krein-space ℋ(T)-norm ⟹ D_{a,θ(a)} → D strong resolvent (Krein formalism) ⟹ "Cor 1.6 ⟺ D has real spectrum" (deliverable D1, criterion-3-shaped). Wall mapped: W-1 index unknown, W-2 real-spectrum persistence = RH, W-3 factorization circular for proofs. Sub-tasks 2.10/2.11 support.
  • → D1 COMPLETE (session 008, D-041): Theorem D1 (deficiency convergence ⟺ strong resolvent convergence) stated with proof skeleton; reduction "(1.12) ⟺ spec(D) ⊂ ℝ" assembled (⇒ Suzuki Cor 1.6; ⇐ via L3/L4 WH literature assembly); lemma map L0–L4/W1–W3; limit extension identified as the π/2 one (Suzuki §7.2–7.5); D-040 Δ-constraint formalized as necessary conditions N1–N3 — the θ(a) flow is obligatory, target the π/2-extension. Remaining: L1 (unconditional embedding), L3/L4 (WH class assembly), θ(a) theory (→ 2.12).
• [x] 2.10 (E-022/E-022b, D-040) Spectral-measure convergence numerics (D-035 D2). COMPLETE (session 008): Clark/de Branges spectral measures μ_a = Σ (1/K_a(z_k,z_k))δ_{z_k} computed for a ≤ 12 (V0–V3 pass). Findings: mass conservation (≈184, a-independent); coarse weak metric FLAT; K_a(z,z) has deep valleys exactly at the true γ's (Δ(a) = 2.16→2.94, corr(d,log K) ≈ +0.4) — the γ-information flows through the WEIGHTS, not the positions (within-z-bin + shifted-null controlled); mass within ±0.1 of γ's 63%→72.5%; Δ(a) ≈ 3.33 − 4.76/a SATURATES at fixed θ=π — fixed-θ ceiling; consolidation (Δ→∞) requires the θ(a) flow (new constraint on 2.9-D1). Δ(a) is now the sharp, cheap convergence probe for any candidate θ(a).
• [x] 2.11 (D-038) Transition-scale lower bound from skeleton + E-019 data: quantify the a-scale at which (★)-consistent consolidation must begin (D-035 D3). [NEW 2026-08-18]
  • → COMPLETE (session 008, D-038): consolidation functional R(a) = (aZ/π)e^{−Δ(a)} (validated 15% vs measured residual); onset criterion Δ′(a) > 1/a; margin C(a) = Δ − log a decreasing 0.77 → 0.46 (a = 4→12); a* > 12; fixed-θ consolidation asymptotically IMPOSSIBLE (saturation ceiling vs log a growth).
• [x] 2.12 (E-024, D-042) θ-flow numerics. COMPLETE (session 008):
  • θ-INDEPENDENCE proved numerically (residual spread ≤ 2.2%, valley masses ≈ 1.00 for all θ; only lattice phase responds) — the θ(a) flow CANNOT drive consolidation (de Branges prediction confirmed); channel closed by evidence. Linear-K law found: K_plateau ≈ 1.9a (≈ (6/π)a, 5 points to 0.3%), valley floor ≈ 1 (mass gauge m_γ = 1) ⟹ residual → Z/6 ≠ 0 — the family equilibrates EXACTLY at the consolidation boundary (margin C(a) → 0.4 const). Consolidation channel relocated to Suzuki's own lever: λ → λ_a⁻ (ground-state regime, sister conjecture (1.2)) → task 2.13. [ERRATUM 2026-08-19 (D-060): the 1.9a fit / Z/6 residual are superseded by D-045 — plateau K/(2a) → 1 (measured 0.973–0.997), residual → Z/(2π); the equilibrium conclusion is unchanged.]
• [x] 2.13 (E-025, D-043) λ-flow numerics. COMPLETE (session 008): (A) discretization floor found: pencil bottom crosses 0 at a ≈ 5.2 (h=0.01), O(h) artifact → 0; true λ_a unresolvable for a ≳ 3 — the λ→λ_a⁻ experiment is machinery-limited (D-019 F1's cliff tail = floor, upper bounds stand). (B) λ-flow RESPONSE confirmed qualitatively: near-singular T ⟹ Δ deepens (2.2→7.0 at a=4), residual drops 48→11 — but the approached mode at a ≥ 6 is the artifact mode (sister corr ≈ 0). (C) MAJOR CORRECTION: E-019's "γ-proximity chance-level" was a wrong-direction metric; correct direction shows quadratic positional locking ~0.65/a², improving through a=12 (D-029 erratum). Revised picture: positions lock + weights concentrate; obstruction = excess-zero outflow + residual → Z/6 (linear-K equilibrium).
  • [ERRATUM 2026-08-19 (D-060): residual → Z/(2π) per D-045; the obstruction conclusion is unchanged.]

✅ PHASE 3 — Positivity Criteria (Track C) (COMPLETE 2026-08-19 — 3.1–3.8 all answered/closed, R-004 full tag; 3.1/3.2 closed by evidence, 3.5 fulfilled via 3.6–3.8)

• [x] 3.1 Weil positivity on supports [−a,a], push a beyond Yoshida.
  • → ANSWERED/CLOSED by evidence: landscape mapped (D-014); E-006/D-015: positivity horizon resolution-limited at 1e-10; E-007/E-007b + D-017: floor decays ~e^{−1.65a}; pushing further needs new conditioning machinery.
• [x] 3.2 Li coefficients λ_n: numerics to n ~ 10⁵; asymptotic attack.
  • → E-008: zero-side table certifies λ_n > 0 for n ≤ 116 (explicit tail bound). E-011/R-001: arithmetic side (BL Thm 2, zero-free, flint Stieltjes + Arb ζ, dps 1000) λ_n > 0 ∀ n ≤ 2000, cross-validated vs E-008; refined asymptotic ratio 1.00216 at n = 2000. E-015 (session 005, detached): extended to n ≤ 3000, ALL CHECKS PASS (dps 1450; λ_3000 = 8617.2192; ratio 0.999845). Next: asymptotic attack → task 3.5; further pushes (cost ~n⁴: n=4000 ≈ 9 h) only in support of 3.5 (e.g. ratio trend data). CLOSED 2026-08-20: the n ~ 10⁵ own-table target is superseded — R-004's finite verification uses our table to 3000 + (session-042 correction: Johansson 2015 § 4.2's rigorous ordinary-λ_n table to 10⁵, replacing the retracted Misguich–Voros citation, which concerned a deformed sequence), and 3.5's deliverable was achieved via 3.6–3.8 (R-004).
• [x] 3.3 de Bruijn–Newman: study heat-flow dynamics of zeros; can the paper's 2/3 density constrain Λ?
  • → ANSWER: NO — one-sided information (D-021): theorem lower-bounds on-line fraction, Λ needs an upper bound on the complex fraction; plus extremal-vs-averaged (E-012: collision times span 4.5 orders, two-body accurate to 4.8% vs full ODE) and asymptotic-vs-explicit. Route → G-003 (do not retry with stronger density results).
• [x] 3.4 Cross-pollinate: does 2/3-simplicity feed any criterion?
  • → ANSWER: YES — it fed the Suzuki operator line, now the live spectral program. 3.4a CLOSED (D-016, scale mismatch); 3.4b floor decay (D-017); 3.4c COMPLETE (Suzuki operators: D-018, E-009a/b, D-019 — λ_a cliff; Galerkin Weil form validated 4.5e-6; E-010/ D-020 lattice law). Continuation moved to Phase 2 (2.6–2.8) as of the 2026-08-18 regroup.
• [x] 3.5 Li-coefficient asymptotic attack (NEW, 2026-08-18 regroup).
  • → DESIGN COMPLETE (D-032/D-033, session 006 cont.7). Voros: "λ_n > 0 ∀ n ≥ N₀" ⟺ RH at ANY N₀ — no partial version exists. ACHIEVABLE DELIVERABLE identified: EXPLICIT finite-height theorem (λ_n > 0 ∀ n ≤ N₁ from Lagarias Thm 6.1's bridge + Platt's T₀ ≈ 3e12 + traced constants + finite verification) — nobody has assembled this chain. Wall mapped: arithmetic-side triangle bounds explode ((15/14)ⁿ); the three-way cancellation IS RH. Remaining work → tasks 3.6–3.8. COMPLETE 2026-08-19: 3.6–3.8 all done → R-004 (finite-height theorem, ledger #6, full tag).
• [x] 3.6 (D-036) Explicit |ξ′/ξ| / |L′/L| contour bounds for ζ with constants (Lagarias Lemma 6.1; Davenport Ch. 15) + explicit N(T) bound (Backlund–Rosser/Trudgian). [NEW 2026-08-18]
  • → COMPLETE (session 006 cont.9; D-036). I_III dominant ~4.7√n log n first estimate; constants A = 0.9, B₀ = 1.0 MEASURED by E-021 (D-036 §6 updated).
• [x] 3.7 (E-021) Exact S_∞(n) computation n ≤ 10⁴ (Lagarias T-function closed forms) → explicit O(1) constant; measure true |S_f(n)| curve vs the traced bound. [NEW 2026-08-18]
  • → COMPLETE (session 007, after 6-bug root-cause saga — mpmath zeta ~58-digit ceiling, GAMMA_E float literal, 3× parse-before- dps, σ-omission boundary (15/14)ⁿ, float64 zeros; journal-007). ALL CHECKS PASS: V1 λ_n vs E-015 4.8e-25 (n ≤ 3000); V2 A = 0.9, B₀ = 1.0; V3 c₀ = −1/4 with exact correction 1/(24n). |S_f(n)| max 13.52 at n = 3298 vs traced bound ~2280 (slack ~170×). n = 10⁴ rerun available via cache.
• [x] 3.8 (D-037 + R-004) Assemble the finite-height theorem: N₁ explicit; finite verification table; adversarial review; tag [PROVED-CONDITIONAL(computational RH-to-height-T₀)]. [NEW]
  • → COMPLETE (session 008; D-037, R-004, E-023 ALL CHECKS PASS).
  • λ_n > 0 for all n ≤ N₁ = (T₀−1)² ≈ 9.0×10²⁴ (T₀ = 3×10¹² Platt–Trudgian; conservative window N₁* = 2.73×10²¹). N₀ = 5×10⁴ (margin 67 705, convex chain); finite verification ours to 3000 + Misguich–Voros to 5×10⁵ (10× overlap). D-036 |t|<10 gap found and closed (M₀ = 1.3352). Follow-ups: D-039 (digamma sub-bound proof), E-023b (acb box cover).

✅ PHASE 4 — Synthesis Assault (COMPLETE 2026-08-19, session 009)

• [x] 4.1 Combine strongest partial results from Phases 1–3.
  • → D-052 (session 008): result inventory; T-1/T-2/T-3 final forms.
• [x] 4.2 State best new theorem(s); classify [PROVED]/[CONDITIONAL].
  • → D-052; classifications corrected by D-054 (session 009).
• [x] 4.3 Adversarial gauntlet: Davenport–Heilbronn/Epstein sanity gate; independent-instance review; error-hunting pass.
  • → 4.3a D-053 (session 008): GATE PASSES structurally for T-1/T-2/T-3.
  • → 4.3b D-054 (session 009): four independent review instances; ALL THREE TAGS downgraded after hand-verification — D-039 proof broken (bound true), D-036 §1 far-sum O(|t| log t) hole (reference-point trick missing), D-049 B1/B3 lower bounds broken (Lemma-D 1/g² term dropped; sinc² factor 2), δ_crit one-direction, T-2 ⇐ skeleton, D-052 accounting fixes (C1–C5). Theorem STATEMENTS survive (margins dwarf the gaps). Repair map opened:
• [x] 4.5a D-056 (session 009): reference-point R-bound PROVED (A = 10.5, B₀ = 48, honest C₀ incl. log log term — D-036 §0 erratum) + digamma remainder |r| ≤ 1.2/|w|² PROVED + I_I housekeeping. E-028 ALL CHECKS PASS (26× slack); N₀ = 80 000, overlap 6.25×, margin(N₁) = 2.458e26. R-004 tag RESTORED.
• [x] 4.5b D-057 (session 009): margin convexity PROVED (chain-rule reduction φ(T(n))″ = ψφ/4n + 11-block table with elementary sign arguments + I_I direct bound). E-029 ALL CHECKS PASS.
• [x] 4.5c D-058 (session 009): valley lower bounds repaired — B1′(i) isolated zeros clean rate PROVED; B1′(ii) general via node-killing projection (Gram constant + annulus count E(γ,a)); B3′ sinc²((z−γ)a) fix; m_γ fix (K ≤ 1/m_γ); detector restatement three-level (bare/pencil/carrier).
• [x] 4.5d D-059 (session 009): bookkeeping write-ups — (1.12) punctured-compact reading; R_τ := W/F − R₀ + distributional representation; Lemma FD (form-domain identification, flat bumps admissible); L1 write-up (PWS step named).
• [x] 4.4 Numerical stress test vs known zero data.
  • → E-027 + D-055 (session 009, ALL CHECKS PASS): synthetic off-line pair stress test of the T-3 detector — bare-form negativity IMMEDIATE for any δ > 0 (no threshold; strict Schwarz); tuned-carrier threshold π/(2a) EXACT (≤0.9% at a = 4, 8); T_a-pencil onset magnitude-limited (δ ≈ 0.11 at a = 4, 0.038 at a = 8); negative directions localized at the pair. D-050 erratum sharpened.

🔶 PHASE 5 — Verification & Write-up (Track D)

• [~] 5.1 Lean 4 formalization of all new lemmas (build on zeta-23-lean).
  • → SKELETON STAGE COMPLETE (session 010, D-061): NguyenRH1 package (research/lean/NguyenRH1/) — 9 statements compile against Mathlib + Zeta23 types. TIER (i) COMPLETE (session 011): chain_rule_sqrt_shift, sInfty_lower_bound, marginTilde_convex PROVED (~1100 lines; full support library — see journal-011).
  • TIER (ii) STEPS 1+2 COMPLETE (session 012, D-062): lambda_pos_finite_height_verified PROVED modulo the single named analytic hypothesis SfBoundProp + the declared computational perimeter (assembly-first split per session-012-notes; FAlt majorant swap; secant two-point base; base points discharged by certified interval bounds in LiBasePoints.lean — margiñ(8×10⁴) ≥ 8001 certified, margiñ(10⁵) ≥ 85 501 certified).
  • TIER ii′ LAUNCHED (session 014, user directive — BEFORE submission, option (a); design D-064): TWO DISCOVERIES — (1) liCoeff encoding defect (unordered tsum NOT Summable ⟹ junk; LiVerifiedUpTo/SfBoundProp FALSE as encoded; paired-form fix = ii′-1a); (2) crux identity Sf(n) = Res₁(n) EXACT (numerically verified vs E-015/E-021) ⟹ assembly TAIL-FREE. Routes R1–R5; sub-stage map ii′-1a..7 (~9–16 sessions); perimeter unchanged (Trudgian N(T)/S(T) declared, D-062 §4). Freeze protocol: paper files + existing proofs untouched until ii′-7 (liCoeff fix excepted). Remaining after ii′: (iii) valley, (iv) Suzuki.
• [~] 5.2 #print axioms audit — only propext, Classical.choice, Quot.sound permitted.
  • → Inherited library VERIFIED LIVE (session 010, D-061 §3): full build (9010 jobs) + all comparator PrintAxioms scripts match AUDIT.md verbatim. NguyenRH1: all proved declarations (tier (i), session 011; tier (ii) steps 1+2 incl. lambda_pos_finite_height_verified, session 012) show the 3 standard axioms ONLY; sorryAx remains only on the 5 skeleton statements (1 Suzuki + 4 valley) by design. No new axioms anywhere.
• [x] 5.3 Full paper draft with proofs, numerics appendix, Lean appendix.
  • → COMPLETE (session 010): all stubs written (Introduction, Background, Formal verification), abstract refreshed with tags, references resolve, MiKTeX compile clean (12 pp).
• [x] 5.4 Final honesty audit: every claim tagged and justified.
  • → COMPLETE (session 010, D-060): ~55 claims, 4 independent audit instances; 0 unsupported; 10 draft corrections (critical: (1.12)⟺ split — converse is skeleton L3/L4); 7 archive errata filed (D-036 sign, D-056 title, D-055/D-058 0.9% overclaim, D-042/D-043 Z/6 supersession by D-045, R-004 post-repair).

✅ PHASE 5B — TIER ii′: close SfBoundProp in Lean (COMPLETE 2026-08-26, session 041 — sfBoundProp PROVED + lambda_pos_finite_height_closed; design D-064)

FREEZE PROTOCOL: paper files (paperA/paperB/draft/references.bib) and existing Lean proofs are untouched until ii′-7 — the ONLY exception is the liCoeff correctness fix (ii′-1a). Paper A stays submission-ready at every sub-stage boundary (D-064 §8). Perimeter (D-062 §4 + the session-035 additions, user-approved 2026-08-23): Platt–Trudgian RHUpTo, LiVerifiedUpTo, Trudgian N(T)/S(T) [ZeroCountProp — strengthened to the mult-weighted form session 035, matching the declared source; PLUS ZeroCountProp2 (the two-unit specialization) and NoLowZeros (|γ| ≥ 14, the Platt-class zero-location certificate), both for 5f], M₀.

• [x] ii′-0 Design + capability inventory + identity chain.
  • → COMPLETE (session 014, D-064). TWO DISCOVERIES: (1) liCoeff encoding defect — unordered tsum NOT Summable ⟹ junk 0; LiVerifiedUpTo/SfBoundProp FALSE as encoded (theorems vacuous); paired-form fix designed. (2) Crux identity Sf(n) = Res₁(n) EXACT (Lagarias (4.10) summed binomially; verified numerically: j=0 exact 15 digits, λ₂ matches E-015 certified value, residue theorem sides = λ_n(T)+triv+Res₁ to 2e-21) ⟹ assembly TAIL-FREE: |Sf| ≤ |λ_n(T)| + |sides| + |triv| = B(n). All 8 planned Zeta23 dependencies axiom-checked live (3 standard axioms only).
• [x] ii′-1a liCoeff pairing fix + summability (D-064 §1).
  • → COMPLETE (session 015). liSummand = ½·mult·(f ρ + f ρ̄) (manifestly real, liSummand_eq) replaces the junk tsum; liSummable PROVED (re_li_summand_le |Re f(ρ)| ≤ 2n²/‖ρ‖² tail
  • normSq_gammaOf_le_mul_norm_sq (9/4) + liSummand_norm_le (9/2)n²·mult/(1+‖γ‖²) + Zeta23 zero_sum_inv_sq comparison + finite ball via IsCompact.inter_riemannZetaZeros_finite). Full rebuild GREEN (8741 jobs, zero downstream changes); axiom audit: 3 standard axioms only on all new + main declarations. LiVerifiedUpTo/SfBoundProp now TRUE statements (defect repaired).
• [x] ii′-1b R1 residue machinery: general finite-order residue (MeromorphicNF), rectangle residue theorem extension beyond HasSimplePolesOn, w=1 residue by Leibniz ((w−1)^{n+1}J = [wⁿ−(w−1)ⁿ]h(w), h = (w−1)(−ζ′/ζ)), zero residues via vendored logDerivResidue.
  • → COMPLETE (sessions 016–017): LiResidue.lean (zetaA/hLi analytic at 1; lcoeff; A_iter; ResW1_eq_sum — the w=1 residue = Σ_j C(n,j)·lcoeff(j−1) by iteratedDeriv_mul) + LiPrincipal.lean (rectInt_deriv_eq_zero per-side FTC; rectInt'_ppart — principal part integrates to ResW1 n on any rectangle with 1 interior) + LiSides.lean (session 017: rectInt'_Jlag — RectangleIntegral' (Jlag n) z w = ResW1 n + Σ_{ρ∈Sz} (zeroMult ρ)·(1−(ρ/(ρ−1))ⁿ) on rectangles with 1 interior, ζ ≠ 0 on border; removable singularity at 1 via Ffun−TaylP order ≥ n+1; logDeriv NF residues at zeros, multiple zeros OK; vendored residueTheorem_finset; full build GREEN 8745 jobs — root now imports all three files; 19 new decls, 3 standard axioms only). NOTE: zeroMult(−2) = 1 (trivial-zero simplicity) deferred — zeroMult stays symbolic in the sum; the Sz = {nontrivial} ∪ {−2} split is ii′-4 territory.
• [x] ii′-2 R2(i)/(ii) elementary swaps: λ_n = Σ_j(−1)^{j+1}C(n,j)σ_j (binomial + paired swap); S_∞ = Σ_j C(n,j)τ_{j−1} (odd-m tsum ↔ binomial form, D-037 §3 swap).
  • → COMPLETE (session 018): LiSwaps.lean — liCoeff_eq_sum_sigma (paired power sums σ_j := sigmaP; per-slice summability cloned from the ii′-1a skeleton: j=1 via Re(1/ρ) = Re(ρ)/|ρ|² exactness, j≥2 by |ρ|^{−j} ≤ |ρ|^{−2}, radius-2 finite ball; swap via Summable.tsum_finsetSum + CommRing-polymorphic one_sub_one_sub_pow)
  • sInfty_eq_sum (SInfty n = Σ_{j=1}^n (−1)^jC(n,j)·lagariasA j, n ≥ 1; lagariasA encoded 1 + odd≥3 tsum; oddSlice_summable by p-series domination; Σ_{j=2}^n(−1)^jC(n,j) = n−1). Full build GREEN (8746 jobs); 12 new decls, 3 standard axioms only.
• [x] ii′-3 R2(iii) Lagarias (4.10): τ_j = c_j + (−1)ʲσ_{j+1} − (−1)ʲ — LONG POLE. Sanity gate: j=0 is Σ1/ρ = 1 + γ/2 − ½log 4π.
  • → DESIGN COMPLETE (session 019, D-066): route β4 ADOPTED (contour moments + coefficient split) — β1 (Hadamard) ruled out (Mathlib has no Weierstrass product/order theory; extract_zeros_poles is finite-only), β2 (EF reuse) ruled out (moments not entire — outside the EF test class). Factorization: (4.10-a) ⟺ (M) moments σ_k = −g^{(k−1)}(0)/(k−1)! [contour] + (A) τ_j = (−1)^{j+1}a_{j+1} [digamma] + (B) ζ-piece [done]; R-bound SHARED with ii′-5 ⟹ resequenced pipeline: ii′-3a (A+B) → ii′-4 → ii′-5 → ii′-3b (moments) → ii′-3c (assembly → crux). Piece (B) PROVED (session 019, LiZetaCoeff.lean: iteratedDeriv_hLiExt — Taylor coefficients of 1/s + ζ′/ζ(1+s) at 0 are −j!·lcoeff j; 6 decls axiom-clean; build 8747 jobs green). Piece (A) next: τ₀ via Mathlib digamma_one_half; j ≥ 1 via digamma series from logGammaSeq.
  • ii′-3a COMPLETE (session 020): piece (A) PROVED — LiArchimedean.lean + LiDigamma.lean (~1200 lines): the capstone iteratedDeriv_logDeriv_Gammaℝ — the archimedean Taylor coefficients of logDeriv Gammaℝ(1+s) at 0 are (−1)^{j+1}·j!·lagariasA(j+1) for ALL j ≥ 0. Via: the Gammaℝ logDeriv split + τ₀ (Mathlib digamma_one_half) + the digamma partial-fraction series BUILT FROM SCRATCH (logGammaSeq → real identity by deriv-limit interchange → complex series by Weierstrass + identity principle → polygamma values at 1/2 by iteratedDerivWithin_tsum → odd-m reindexing → 2^{j+1} scaling). Build GREEN (8749 jobs); 18 key decls audited: 3 standard axioms.
  • ii′-3c COMPLETE (session 038): LiCrux.lean (~430 lines, root-imported, full build GREEN 8771 jobs): the FE derivative relation (gFun_one_sub_fun + iteratedDeriv_gFun_zero via the UNCONDITIONAL iteratedDeriv_comp_const_sub), the shift expansion (gFun_one_add_punctured/gFun_one_add_eventuallyEq), the coefficient extraction (iteratedDeriv_gFun_one) ⟹
  • lagarias_4_10_a (hZC) PROVED (lcoeff (k−1) = (−1)^k·(lagariasA k + sigmaP k) + (−1)^{k−1}, all k ≥ 1) ⟹
  • THE CRUX sf_eq_resW1 (hZC) PROVED: (ResW1 n).re = Sf n for n ≥ 1 (ResW1_eq_sum + (4.10-a) + both ii′-2 swaps + the binomial sum Σ(−1)^{j−1}C(n,j) = 1). Audit session038b: 8 decls, 3 standard axioms only. ii′-3 (ALL of Lagarias (4.10)) COMPLETE — Sf(n) = Res₁(n) is Lean-proved modulo the declared perimeter.
  • ii′-3b COMPLETE (sessions 037–038) — ROUTE REVISION (D-070): the moments (M) came from 5e's partialFraction_identity by PURE ALGEBRA + series calculus (no contours — the contour work was 5e's): gFun := logDeriv xiL = B + seriesFun at good points (xiL entire via the Λ₀ closed form; perimeter ZeroCountProp ONLY — 5f's hZC2/hNLZ not needed). LiMoments.lean (~1020 lines, root-imported, full build GREEN 8770 jobs): xiL + the conj/reflect subtype equivs, (G) gFun_eq_momentB, evaluations gFun_zero/gFun_one/gFun_one_eq_neg (FE sign), the summability budget (master Σ mult/‖ρ‖² + AM-GM mixed bound), the reindex machinery (sigmaP_eq_unpaired k ≥ 2, vTerm_tsum_eq_zero), k = 1 (sigmaP_one_eq_neg_gFun_zero), §5 the termwise iterated derivation at 0 (iteratedDeriv_zpow_neg_one, iteratedDeriv_seriesTerm, the M-test seriesTerm_deriv_summableLocallyUniformlyOn, iteratedDeriv_seriesFun_zero — the LiDigamma:749–785 iteratedDerivWithin_tsum pattern), §6 gFun_eventuallyEq_zero +
  • THE CAPSTONE sigmaP_eq_neg_iteratedDeriv_gFun_div (hZC : ZeroCountProp): sigmaP k = −gFun^{(k−1)}(0)/(k−1)! PROVED for ALL k ≥ 1 (session 038, first-pass green). Audit session038: 23 decls, 3 standard axioms only. Remaining: ii′-3c (the (4.10-a) assembly; needs the FE derivative relation gFun^{(k−1)}(0) = (−1)^k·gFun^{(k−1)}(1), small from xiL_one_sub).
• [x] ii′-4 L3 zero-avoiding T (pigeonhole on perimeter C₀/FAlt) + L1 kernel bounds (|k_n| ≤ 2, e⁴+1, e^{√n/2}+1; trivial residue).
  • → COMPLETE (session 021, LiContour.lean, ~400 lines): L3 exists_zero_avoiding_T — clearance 1/(3·C0hat(a+1)) in any unit window [a, a+1], a ≥ 2, from the perimeter ZeroCountProp (Trudgian N(T)/S(T) in Ĉ₀ form) via the midpoint pigeonhole exists_avoiding_midpoint (k+1 midpoints, injective-badness); finiteness via Zeta23 zerosIn_finite. L1: kFun_norm_le_two (re s ≤ 1/2), kFun_shift_norm_le_exp_four_add_one (horizontals, re s ≤ 3, n ≤ im²), kFun_shift_norm_le_exp_sqrt_half_add_one (right vertical, 2√n ≤ re s), kFun_neg_two + norm ≤ 1. PLUS the deferred trivial-zero simplicity zeroMult_neg_two (zeroMult(−2) = 1): local factorization ζ = (s+2)·Λ/Hfun with Hfun = 4π^{−s/2}Γ(s/2+2)/s analytic, Hfun(−2) = −2π ≠ 0, Λ(−2) = Λ(3) = ΓR(3)ζ(3) ≠ 0. Build GREEN (8751 jobs); 17 decls audited: 3 standard axioms only.
• [x] ii′-5 R3 R-bound (D-056, A = 10.5, B₀ = 48) via LOCAL route: Borel–Carathéodory (Mathlib) + Jensen (Mathlib) + Blaschke (StrongPNTPrefix); FE polynomial strip bound via riemannZeta_one_sub + Stirling; digamma Lemma D.
  • → DESIGN COMPLETE (session 022, D-067): route b″ — Davenport disc at 2+it (R = 5/2) + FE-reflection with EXACT zero-sum cancellation; Stirling-free (Zeta23 digamma_stirling subsumes Lemma D), Hadamard-free; geometry obstruction (every covering disc dips left of σ = 0) resolved via one extra EM level.
  • ii′-5b COMPLETE (session 022): LiRBound.lean — the level-2 Euler–Maclaurin representation ζ(s) = 1/2 + 1/(s−1) − s(s+1)∫₁^∞ B̃₂(x)x^{−s−2}dx (re s > −1; b2Fun machinery, IBP identity, parameter-integral analyticity, W± convex-region identity principle) + norm_riemannZeta_le_disc: ‖ζ‖ ≤ (3/4)|t|² on B(2+it, 5/2), |t| ≥ 10. Build GREEN (8752 jobs); 27 decls audited clean. ROUTE REVISION (session 023, D-067 §6): the disc-only constants provably CANNOT reach the baked 10.5/48 (BC derivative factor ≥ 16× the M-coefficient; honest assembly ~270) ⟹ two-stage plan: loose disc bound as the GROWTH INPUT for the partial-fraction identity (5e), tight constants from D-056's analysis of the identity (5f). ii′-5c COMPLETE (sessions 023–024): LiDisc.lean — zeroDiscFinset + zeroDisc_isNontrivial; scaledZeta (unit-disc scaling) + F(0) = 1 via Zeta23 zeta_lower_bound_two (‖ζ(2+it)‖ ≥ 1/3, no μ-series build); the multiplicity-invariance chain (analyticOrderNatAt_riemannZeta_ affine/const_mul/scaledZeta); scaledZeta_jensen_count (ZerosBound, ≤ log((9/4)|t|²)/log(33/32)); session 024 back half: R-gap via the ×10-rescaled midpoint pigeonhole (R_c ∈ [2.3, 2.4], clearance gapD = 1/(50(k+1))); g = Cf r_c F analytic + nonvanishing on closedBall(0, r_c) (Zeta23 Cf/ZeroFactorization); |g| ≤ (9/4)|t|²·gapD^{−M_c} on the ball (max-modulus over the zero-free sphere); LogOfAnalyticFunction + BorelCaratheodoryDeriv (450·M factor); logDeriv chain + affine push-forward + near/extras split.
  • Capstone: logDeriv_riemannZeta_sub_nearZeros_le — the LOOSE R-bound ‖ζ′/ζ(s) − Σ_{|γ−t|<1} m/(s−ρ)‖ ≤ 100000·(log|t|)² on σ ∈ [1/2, 7/2], |t| ≥ 10, ζ s ≠ 0 (no perimeter hypothesis — Jensen count input). Build GREEN (8753 jobs, LiDisc now root- imported); 32 new decls audited: 3 standard axioms only.
  • ii′-5d COMPLETE (session 025): LiReflect.lean (~640 lines, 26 decls audited clean) — logDeriv_zeta_fe (pointwise logDeriv FE: logDeriv ζ s = −logDeriv ζ(1−s) − [logDeriv ΓR s + logDeriv ΓR(1−s)]); sum_nearZeros_neg_reflect (the EXACT zero-sum cancellation under ρ ↦ 1−ρ: nearZeros(−t) = image, zeroMult invariant via analyticOrderAt_zeta_one_sub); logDeriv_Gammaℝ_shift (the +4 ΓR shift putting both digamma arguments in re > 0) + digamma_stirling ⟹ ΓR-bracket ≤ 4(log|t|)²; capstone
  • logDeriv_riemannZeta_sub_nearZeros_le_left ≤ 200000·(log|t|)² on σ ∈ [−5/2, 1/2], |t| ≥ 10; PLUS the 5e input
  • norm_digamma_sub_log_le_of_two_le_abs_im (‖ψ(w) − log w‖ ≤ 3 for 2 ≤ |im w|, uniform in the shift chain: digamma_add_natCast
  • first-order EM + arctan-FTC). Build GREEN (8761 jobs, LiReflect root-imported). DEFERRED to session 026 first item: zeroMult(−2n) = 1 for ALL n (5e's entirety at trivial zeros).
• [x] ii′-5e R3 partial-fraction identity (D-068 design; two-stage plan's second stage). COMPLETE session 034 — capstone partialFraction_identity PROVED (perimeter ZeroCountProp only).
  • → DESIGN COMPLETE (session 026, D-068) with TWO CORRECTIONS to D-067 §6: (C1) the circle series bound is O((log R)³) via the RADIAL split (γ-gap only in the critical annulus [R±2]; the naive split gives O(R log R) — fatal, recorded with fix); (C2) the near-axis left-plane digamma bound is a separate build.
  • 5e-0 COMPLETE (session 026): LiTrivialZeros.lean — gamma_mul_prod (product-form Γ recurrence) + the HfunT n cofactor + zeroMult_neg_two_mul: zeroMult(−2n) = 1 for ALL n ≥ 1 (8 decls audited clean; build 8762 jobs, root-imported).
  • 5e-i COMPLETE (session 027): LiGapCircles.lean — exists_gapCircle_radius (R ∈ [4k+5/2, 4k+3], dist(R/2,ℤ) ≥ 1/4, ordinate clearance 1/(16·C0hat(4k+9/2)); ×2-rescaled pigeonhole).
  • 5e-ii COMPLETE (session 027): LiDigammaLeft.lean — norm_digamma_le_of_two_le_re (B: ‖ψ‖ ≤ 20 log(2+‖w‖), re ≥ 2), digamma_recip_sum_le (C: Σ‖(w+j)⁻¹‖ ≤ 2/c+2+2 log m), norm_digamma_le_of_dist_nat (A: near-axis bound, re ≤ 2), logDeriv_Gammaℝ_eq (G: the general identity for im ≠ 0); 15 decls audited clean; build 8764 jobs.
  • 5e-iii COMPLETE (session 028): LiSeries.lean — the zero-side partial-fraction series seriesFun s := ∑' ρ, mult·(1/(s−ρ)+1/ρ): seriesSummable (unconditional, the ii′-1a D-trick with the (17/12)‖ρ‖² comparison), seriesFun_analyticOnNhd off the nontrivial zeros (three-case avoiding balls + the Weierstrass M-test pattern), nontrivialZero_isolated (min-distance), seriesFunSub_analyticAt + seriesFun_sub_polar_analyticAt (series − mult/(s−ρ₀) analytic AT ρ₀ — the 5e-iv residue cancellation input); 22 decls audited clean; build 8765 jobs.
  • 5e-iv COMPLETE (session 029): LiFEntire.lean — F ENTIRE via the punctured-limit extension Gentire s := limUnder (𝓝[≠] s) Fexpr (no removable-singularity theorem in Mathlib; junk values at the excluded points sidestepped by limUnder uniqueness): principal-part-split witnesses at nontrivial zeros (NF + seriesFun_sub_polar_analyticAt), at 1 (logDeriv zetaA), at 0 and −2n (the digamma-series splits: digammaSeriesPart on ball(0,1/2), digammaSeriesPartSub on ball(−n,1/2), both M-test); supporting zeta_zero_classification (zeros = nontrivial ∪ {0} ∪ {−2n}) + analyticAt_digamma (off {0}∪−ℕ). Capstone gentire_analyticAt_and_eq: (∀ s, AnalyticAt ℂ Gentire s) ∧ (∀ s good, Gentire s = Fexpr s); 30 decls audited clean; build 8766 jobs. 5e-v-b + 5e-v-c COMPLETE (sessions 030–033): LiCircleBound.lean (~3928 lines) — count bridges (A0count from Zeta23's RvM local count, mult-weighted, all t, unconditional), the Dirichlet bound ‖ζ′/ζ‖ ≤ dirichletC2 (re ≥ 2), tsum_split_finset, lowZeroConst, the far-tail bound zero_tail_inv_sq_le (Σ_{|γ|>X} m/(1+γ²) ≤ 16·A₀·log X/X, X ≥ 200 — the dyadic fiber machine + ENNReal.tsum_fiberwise),
  • the series circle bound seriesFun_norm_le_gapCircle (‖seriesFun s‖ ≤ 2·lowZeroConst + 2900·A₀·Ĉ₀(4k+9/2)·(log R)² on the γ-gap circle, k ≥ 4000), and the Fexpr circle bound Fexpr_circle_le (‖Fexpr s‖ ≤ 2·lowZeroConst + dirichletC2 + 400000·A₀·Ĉ₀(R+2)·(log R)²): three-region logDeriv assembly (Dirichlet / 5c+5d capstones + the near sum via gapCircle_sep / FE + ΓR bracket), digamma_circle_le (uniform ψ bound, left near-axis via the ℤ-clearance), and
  • logDeriv_Gammaℝ_eq_of_not_neg_nat (the (G) formula at any non-pole point incl. s = −R — direct logDeriv_mul, no continuity). 5e-v-d COMPLETE (session 034) — ii′-5e DONE: LiSqueeze.lean (~330 lines, 5 decls audited clean; LiCircleBound
  • LiSqueeze root-imported; full build GREEN) — the Schwarz squeeze (gentire_const: max-modulus + ball-form Schwarz on the γ-gap circles, growth (log R)³/R → 0 via Q := R^{1/4} ⟹ Gentire ≡ Gentire 0 =: B) and THE CAPSTONE partialFraction_identity (hZC : ZeroCountProp): ∃ B : ℂ, ζ′/ζ(s) = B + seriesFun s − 1/s − 1/(s−1) + ½log π − ½ψ(s/2) off the excluded set — the partial-fraction identity Lean-proved modulo ONLY the declared perimeter. Remaining: 5f (tight constants 10.5/48 from D-056's two-point analysis).
• [x] ii′-5f R3 tight constants (D-056's Theorem R: |R(s)| ≤ 10.5·log (|t|+2) + 48). → COMPLETE (sessions 035–036, LiTightR.lean ~4300 lines). Perimeter repair (user-approved): ZeroCountProp strengthened to the mult-weighted form (the second ii′-1a-class encoding defect — the unweighted set-card under-captured the declared Trudgian N(T) source; one_le_zeroMult bridge; consumers adapted; full build green, audit clean). P1/P2 perimeter additions (user-approved, D-069): ZeroCountProp2 (two-unit count 0.6·L + 0.886·LL + 2.7) + NoLowZeros (|γ| ≥ 14).
  • D-069 Finding 1: D-056's piece 2 charges the near sum one C₀(t) for a TWO-unit window — the honest two-unit Trudgian form makes the assembly fit 10.5/48 (pinch margin ≈ 1.9). Finding 2 (ii′-6 repair map): H(T)'s near sum has a clearance-coverage gap (honest ≈ 7·Ĉ₀² vs baked 3·Ĉ₀²; margin survives, crossover moves). 5f-i COMPLETE (Rexpr_decomp + pieces 1 dirichletC2_le_one, 2 near_sum_refPoint_le, 4/5 one_div_diff_le); 5f-ii piece 6 COMPLETE (digamma_diff_le ≤ 6/t) + piece 3 COMPLETE (session 036): the far interval machine — certified numerics, farW + S₃ ≤ 1.3476, six tail bricks (RW₀/1/2 = 0.1/0.3303/0.1216, LA₀/1/2 = 1/23/0.1687/0.0621), C0hat bridges (2k+1/j+1/2t+1), zeroMult_conj machinery, farG + norm reduction, main bucket machine (unit_family_le + main_bucket_count + farG_main_le), two tail machines (farGLeft_le ≤ 1.1729, farGRight_le ≤ 2.7343), far_series_le ≤ 12.1284·C₀ + 7.2425. 5f-iii COMPLETE (session 036): pinch lemma pinch_tight_R (11.6318·LL − 4.6484·L ≤ 0.397094 for L ≥ log 12, concave tangent at the certified critical point 2.5024, f(2.5024) ≤ −0.96231) + the C0hat L/LL conversion + THE CAPSTONE logDeriv_riemannZeta_sub_nearZeros_le_tight (hZC) (hZC2) (hNLZ): ‖logDeriv ζ s − Σ_{near} m/(s−ρ)‖ ≤ 10.5·log(t+2) + 48 PROVED (six-piece assembly; fold 5.8516L + 11.6318LL + 47.6029 ≤ 10.5L + 48 via the pinch). Audits session036/036b: 33 decls, 3 standard axioms only; full build GREEN (8762 jobs).
• [x] ii′-6 L0 assembly: sides identity + bridge |λ_n(T)| ≤ 4·FAlt(T) (hRH, BOTH-signs correction F-A) + |Sf n| ≤ Bn FAlt n on [10⁵, N₁].
  • ⚠ FINDING F-D (session 038, D-072): the (6.12) stepping in Lagarias's Thm 6.1 is broken at T = √n (right-tail ~e^{0.066√n}, ~5.9×10¹⁰ envelope at n = 10⁵ measured by E-031); D-036/D-037/ R-004's B(n) inherits it (charge "3.3" off by ~10⁷×; margin collapses for n ≳ 3×10⁴). Theorem statement survives (verified to 5×10⁵; sides cancel by conjugation + phase winding); all Lean work to date survives. REPAIR ROUTE CHOSEN (2026-08-25, user directive): the D-074 zero-free dog-leg (entry below) — keeps T_cut = √n and the ORIGINAL N₁ = (T₀−1)² ≈ 9×10²⁴; the horizontal right-tail piece of ii′-6-c now comes from ii′-6-DL. The T = c√n global repair (D-073: N₁ → (T₀/c)²) is the PAUSED fallback (c = 1.5 WIP on branch wip/c-1.5-margin-redo, 642d47a).
  • → ii′-6-0 DESIGN COMPLETE (session 038, D-071 + E-030 ALL CHECKS PASS): THREE findings — F-A bridge factor-2 (both-signs sum with one-sign N(T) in D-036/D-037/E-023; R-004 unaffected, paper erratum at ii′-7), F-B I_III two-unit count ((2/3)Z2 honest), F-C baked Bn unprovable beyond ~5×10⁷. USER-APPROVED (8-step protocol): redefine Bn honestly (2F → 4F, (2/3)Ĉ₀ → (2/3)Z2hat); fold validated (E-030 V2/V3/V4). Perimeter additions approved: ZeroCountGlobalProp (global Trudgian N(T) ≤ FAlt) + MZeroProp (M₀ ≤ 1.3352). Sub-stages: 6-a (Bn redefinition + convexity re-proof + base-point re-certification) → 6-b (perimeter Props + extended pigeonhole + sides identity + bridge) → 6-c (four side bounds; horizontals = segment-integral machine) → 6-d (fold ⟹ sfBoundProp).
• [x] ii′-6-R F-D REPAIR SIDE THREAD (COMPLETE, 2026-08-25, session 039): focused re-proof of ONLY the right part of the horizontal segments in Lagarias Thm 6.1 (the broken (6.12) stepping).
  • → 6-R-0 (E-032 diagnostic, ALL CHECKS PASS): TRUE complex I_right at T = √n by direct quadrature (Dirichlet series certified-tail primary, mpmath validated 6e-10, dps 50) — verdict HIDDEN CANCELLATION, decisive: |I_right| = 7.2/16.7/26.2 vs envelope 5.1e1/1.0e4/4.7e10 (n = 10³/10⁴/10⁵), ratio collapsing to 5.6e-10; the per-side claim |I_II| = O(√n) is empirically TRUE (|I_II|/√n decreasing 0.235 → 0.098) but envelope-unprovable at T = √n; mid-segment honest (ratio 0.7–0.95); repair heights honest (ratio ≈ 1, envelope collapses). STOP-rule reported; user direction: repair only, salvage parked (open question, D-073 §8 D4).
  • → 6-R-1 (D-073 §§3–7, repaired proof): dependency audit (only the stepping is proof-breaking; the (1+4/(16+n))ⁿ intermediate is a harmless looseness, e⁴+1 valid); Lemma 4.1 corrected stepping + Cor 4.2 explicit R(c) = |ζ′/ζ(2)|·[e^{4/c²}/ (4(1−q)log 2) + 1/(2 log 2)], q = e^{1/c²}/2 [PROVED, elementary]; AUDIT CORRECTION — recommend c = 1.5 (reverses D-072's "2 margin/1.5 range": the fold is I_III-length-dominated, c = 1.5 wins BOTH base margins (181 256 vs 109 370 at 10⁵) AND range (N₁ = 4×10²⁴); c = 2 the ultra-conservative option, R = 1.97 < broken 3.3); consequence audit (Thm 6.1 statement unchanged, O-constant c-dependent; Thm 1.1 height ((T₀−1)/c)²; no new perimeter); E-033 ALL CHECKS PASS (Z₀ certified [0.5699210, 0.5703661], R covers E-032 measured 3.2–6.3×, kernel charge, fold fit ≤ 0.40, margins > 0 to N₁, full fold).
  • → 6-R-2 (D-073 §8, drafts only, correspondence untouched): D3 letter repair paragraph + D4 T = √n per-side verdict paragraph (open question: the hidden-cancellation mechanism).
  • THEN: main line executes repair (R) — 8-step protocol re-run at
  • c = 1.5 (ii′-6-a redo: Bn_c(n) := 4F + 4T[(2/3)Z2 + 10.5 log
  • 48] + 40·1.3352 + 2(e^{16/9}+1)(7Ĥ + 5.94) + IIMaj_c + 1, T = 1.5√n+1; convexity re-proof + base-point re-certification, values IMPROVE) → ii′-6-c with the fixed stepping.
  • [SUPERSEDED as the main route 2026-08-25 by ii′-6-DL (user directive: the goal is the ORIGINAL N₁ = 9×10²⁴); preserved as the PAUSED FALLBACK — WIP on branch wip/c-1.5-margin-redo (642d47a, resume map in its commit message).]
• [x] ii′-6-DL F-D DOG-LEG REPAIR (COMPLETE, 2026-08-25, user directive; directive file PROJECT_DIRECTIVE_D-074.txt; design/progress anchor D-074; route to the ORIGINAL N₁ = (T₀−1)² ≈ 9×10²⁴). Design: keep T_cut = √n (residues/bridge/λ_n(T_cut) UNCHANGED); replace ONLY the broken right horizontal tail [3, 2√n] by a zero-free dog-leg: lift σ = 3 from T_cut to U = (3/2)√n (V_left ≤ (√n/2)(e^{5/2}+1)·C_zeta3 ≈ 1.07√n explicit), traverse at U (H_high = D-073's R(1.5) = 5.94, q = e^{4/9}/2 < 1 certified), drop at X_R = 2√n (V_right exponentially tiny); the dog-leg rectangle is entirely in Re w ≥ 3 — ζ zero-free + no pole UNCONDITIONALLY (no new perimeter, no RH above T_cut). Mid-segment [−5/2, 3] at T_cut untouched (honest, E-032). Bn impact ≈ +2.2√n; the dog-leg charge decomposes into existing margin-block shapes (convexity re-proves at coefficient level). Sub-stages (crash-safe, commit per sub-stage; D-074 §1 log):
  • → DL-0 COMPLETE (session 040): §2 audit (Lean contour matches; Jlag n s = (s/(s−1))ⁿ−1·(−ζ′/ζ s), CCW orientations pinned); §3 derivation (identity H_low = H_high − V_right + V_left; analyticity unconditional at Re ≥ 3); §4 constants (C_zeta3 = 0.165 certified — hand-estimate 0.150 caught wrong by smoke test; e^{5/2}+1 ≤ 13.19; q = 0.7798; HHigh = 5.94; VRight = IIMaj/4); E-034 ALL CHECKS PASS (identity exact to 2–5e-5; piece slack 4–13×; margins 14 419 / 90 317 / 2.458e26 at 8×10⁴ / 10⁵ / N₁ = (3×10¹²−1)² — ORIGINAL endpoint restored; fold fit ≤ 0.399); §7 A–L report — AWAITING USER GATE before DL-1 (Lean).
  • → DL-1 COMPLETE (session 040, LiDogLeg.lean, build 8773 jobs, audit clean): Jlag_differentiableAt_dogleg + holomorphicOn_Jlag_dogleg (Re ≥ 3 zero-free via Mathlib, NO perimeter), rectangleIntegral(_')_Jlag_dogleg_eq_zero (Cauchy), upper_right_horizontal_eq_dogleg (the exact identity (★) PROVED), kFun_conj/Jlag_conj (lower-side machinery).
  • → DL-2 COMPLETE (session 040, LiDogLeg.lean +~250 lines, build 8773, audit clean): kFun_three_add_it_norm_le_exp_five_halves_add_one (kernel ≤ e^{5/2}+1), dirichletC3 ≤ 1/2 (termwise 3-vs-2 comparison + dirichletC2 ≤ 1 — C_zeta3 charged 0.5, fold- indifferent; 0.165/0.17 tightening path documented), norm_logDeriv_zeta_le_half (‖ζ′/ζ‖ ≤ 1/2, re ≥ 3), vIntegral_Jlag_three_norm_le: ‖V_left‖ ≤ (U−T)(e^{5/2}+1)/2. E-034 re-validated at C = 0.5: ALL CHECKS PASS (margins 13 165/88 916/2.458e26).
  • → DL-3 COMPLETE (session 040, LiDogLeg.lean +~430 lines, build 8773, audit clean): norm_term/norm_logDeriv_zeta_le_two_pow (zeta halving 2^{−(σ−2)}·dirichletC2), one_add_div_pow_norm_le_exp_four_ninths (kernel envelope e^{(4/9)σ} — single-exponential, no geometric series), Jlag_dogleg_norm_le_envelope (dirichletC2·(4e^{−cσ}+4·2^{−σ})), integral_exp_neg_le (FTC machine), cdog_gt (c ≥ 0.2487), exp_four_thirds_le (e^{4/3} ≤ 3.8073), hIntegral_Jlag_dogleg_norm_le ≤ 8.38 (charged with dirichletC2 ≤ 1; tight R(1.5) = 5.94 = documented tightening path). E-034 re-validated at Lean constants: ALL CHECKS PASS (margins 13 160/88 911/2.458e26).
  • → DL-4 COMPLETE (session 040, LiDogLeg.lean +~160 lines, build 8773, audit clean): kFun_right_vertical_norm_le_exp_sqrt_half_add_one (w = 2√n kernel variant, e^{√n/2}+1), vIntegral_Jlag_right_norm_le ≤ (U−T)(e^{√n/2}+1) 2^{−(2√n−2)}·dirichletC2 — exponentially tiny; VRightBound charged IIMaj/2 (provable with dirichletC2 ≤ 1; IIMaj/4 = tightening path).
  • → DL-5 COMPLETE (session 040, LiDogLeg.lean +~210 lines, build 8773, audit clean): hIntegral_Jlag_low_le_dogLegUpper + hIntegral_Jlag_low_neg_norm_le_dogLegUpper (both ≤ ((√n+1)/2)(e^{5/2}+1)/2 + 8.38 + IIMaj/2 for T ∈ [√n, √n+1], U = (3/2)T) + dogLegUpper_two_sides — the full dog-leg PROVED in Lean, no perimeter, nothing above T_cut.
  • → DL-6 COMPLETE (session 040, LiDogLeg.lean +~350 lines, build 8773, audit clean): the direct Dirichlet bound at re = 2√n — norm_logDeriv_zeta_le_iimZeta ≤ 0.57·2^{−(2√n−2)} (n ≥ 5), NO dirichletC2 ≤ 0.57 needed (log2-leading + 3^{−(2√n−2)} tail with dirichletC2 ≤ 1); V_right ≤ IIMaj/4 EXACTLY; DL-5 upgraded to the quarter charge (dogLegUpper = VLeft + 8.38 + IIMaj/4 per side ⟹ 1.5·IIMaj total in Bn, the convexity-safe coefficient). E-034 re-validated at IIMaj/4: ALL CHECKS PASS.
  • → ii′-6-a2 COMPLETE (session 040): DogLegRight def + Bn redefined (horizontal share 2(e⁴+1)(7Ĥ) + 2·DogLegRight, T = √n+1 UNCHANGED — N₁ = (T₀−1)² ≈ 9×10²⁴ PRESERVED); margin lockstep at coefficient level; 4/3-bracket strengthening cherry-picked onto master (e11ad95); marginTilde_convex re-proved (1.5·IIMaj, strict); base points re-certified (Bn(8e4) ∈ [273k, 332k], Bn(10⁵) ≤ 352k ⟹ margin(8e4) ≥ 4 001, hbase2 66 001 < 80 501); endpoints UNCHANGED; build GREEN (8773 jobs); audit: 41 decls, 3 standard axioms, 0 sorryAx.
  • THEN THE ORIGINAL PLAN RESUMES (D-074 §8 return map): ii′-6-c (four side bounds with the repaired horizontal) → ii′-6-d (fold ⟹ sfBoundProp) → ii′-7 (closure at the ORIGINAL N₁ ≈ 9×10²⁴). Fallbacks: (a) c = 1.5 paused branch (N₁ = 4×10²⁴); (b) c = 2 (N₁ = 2.25×10²⁴); (c) T = √n hidden-cancellation open question (D-073 §8 D4).
  • → ii′-6-c STARTED (session 040 block B): FINDING F-E (D-074 §9) — the I_I kernel charge e^{√n/2}+1 is off by one at re w = 2√n near t = 0 (true value e^{√n/2+1/8}; latent in the original D-036 charge); REPAIR ADOPTED: I_I charged honestly as e^{1/3}·IIMaj (uniform kernel ≤ e^{√n/2+1/3}+1, n ≥ 4), the overrun absorbed by the fold's free dropped 2π (e^{1/3} ≤ 1.4 ≤ 2π) — NO change to Bn/IIMaj/convexity/pinch/base points (fatten-IIMaj rejected: iimaj_bracket_bound's 4.56 is linear).
  • 6-c-i COMPLETE (a8c5b1e): LiSideBounds.lean scaffolding (Z2hat_mono, nearZerosSub_mult_sum_le, logDeriv continuity, Jlag_norm_eq, both zero-freeness lemmas, rectangle side decomposition, VIntegral/HIntegral machinery, even symmetry).
  • ii′-6-c..6-d COMPLETE (session 041): 6-c-ii I_III (vIntegral_Jlag_left_norm_le, 6e5a98f), 6-c-iii I_I F-E form (vIntegral_Jlag_right_le_exp_third_IIMaj, 9bd8ba9), 6-c-iv the mid-horizontal segment machine (arcsinh-FTC from scratch — integral_one_div_sqrt_sq_add_sq + endpoints + per-zero ≤ 2·log(16.5/δ) by pure log-mono, 1fed1df), 6-c-v the horizontal assembly (mid + DL-5 tails both sides, 5d3dc0a), and 6-d THE FOLD (774fec5): sfBoundProp : SfBoundProp PROVED — |Sf n| ≤ Bn FAlt n on [10⁵, N₁] from EXACTLY the six declared perimeter hypotheses (RHUpTo, ZeroCountProp, ZeroCountProp2, ZeroCountGlobalProp, NoLowZeros, MZeroProp); the pinch NI + 5.5R ≤ 7·Ĥ discharged by a fully elementary log-mono chain (no certified log numerics); the bridge cloned at T ≤ 3·10¹² (the range actually used — T ≤ √n+1 holds exactly incl. n = N₁).
  • ii′-6 COMPLETE.
• [x] ii′-7 Closure: theorem sfBoundProp : SfBoundProp; final lambda_pos_finite_height_closed (3 perimeter hypotheses only); full axiom audit; paper Appendix B + tag upgrade (D-062 §4 endpoint); archive closure + D-037 line-63 erratum pointer.
  • → COMPLETE (session 041): lambda_pos_finite_height_closed PROVED (a0943a6, LiClosed.lean) — λ_n > 0 for ALL 1 ≤ n ≤ N₁ = (3×10¹²−1)² from EXACTLY SEVEN declared hypotheses (the two computational certificates + the five analytic perimeter Props); full axiom audit (AuditSession041: 29 decls incl. the closed chain — 3 standard axioms only, 0 sorryAx); Paper A closure (b64a839 + the session-042 review revision, compiles clean 11 pp — Appendix B rewritten: second tier COMPLETE + the verbatim signature + the instantiation list + the dependency chain; the B(n) display corrected + the F-A/F-B/F-E correction-note footnote + the F-D dog-leg promoted to §3.1; abstract/intro to the seven-hypotheses headline; hedged novelty (Oesterlé's unpublished precursor noted); AI Contribution Statement factual refresh); archive closure (D-037 erratum block + addendum, R-004 Lean-closure status, NGUYEN.md, STATE.md, journals 041–042). SESSION-042 REVIEW REVISION (user review): the finite-verification certificate Misguich–Voros (deformed sequence, private communication) was RETRACTED and replaced by Johansson 2015 § 4.2 (rigorous ordinary-λ_n to 10⁵); LiVerifiedUpTo reduced (5·10⁵) → (10⁵) (79c96f2, matches the checkable evidence — the assembly's hfinite branch uses exactly n < 10⁵).

6. GRAVEYARD (documented dead ends — REQUIRED logging)

7. RESULT LEDGER

8. SESSION PROTOCOL & RESEARCH ARCHIVE (MANDATORY)

Multi-stage project: computer is shut down between stages. NOTHING may live only in conversation. The archive below is the single source of truth.

8.1 Archive map

STATE.md                    ⭐ resume point — READ FIRST every session
research/
├── journal/session-NNN.md  per-session narrative log
├── results/R-NNN-*.md      one file per result (+ index.md ledger)
├── graveyard/G-NNN-*.md    one file per dead end (+ index.md)
├── derivations/D-NNN-*.md  worked derivations (+ index.md)
├── numerics/scripts/       deterministic experiment scripts
├── numerics/data/          E-NNN-*.csv + E-NNN-*.json metadata sidecars
├── research.db             SQLite catalog (sessions, results, graveyard,
│                           derivations, experiments) — schema in
│                           numerics/scripts/schema.sql, CLI: db.py
└── paper/                  paperA.tex (Paper A, split 2026-08-20),
                            paperB.tex (research-note skeleton),
                            draft.tex (FROZEN pre-split combined copy),
                            references.bib

8.2 Storage conventions

• Results/derivations/graveyard: plain Markdown, honesty tag on every claim.
• Numerics: DUAL storage — CSV+JSON sidecar (human/paper-readable) AND SQLite registration (queryable), written together via db.py.
• Data is cached; scripts never recompute unless --force.
• Paper assembled only from tagged files in results/.

8.3 Session START protocol

1. Read STATE.md → resume point, next action, open threads, blockers.
2. Skim latest journal entry + results/index.md.

8.4 Session END protocol (before any shutdown — no exceptions)

1. Write journal/session-NNN.md (work, decisions, outcomes).
2. File every result/dead end/derivation in its own file; update index.md files; register in research.db.
3. Update NGUYEN.md checklist (§5), Graveyard (§6), Result Ledger (§7).
4. Update STATE.md LAST with an explicit "NEXT ACTION:" line.
5. git add + commit with session number in the message. NOTE: save artifacts IMMEDIATELY when produced (crash-safe), not batched.

8.4a FORK RULE (user directive, 2026-08-17)

When the path FORKS (multiple candidate directions), do ALL of them — one by one — then pause to gather thoughts and evaluate the next step together. No path is dropped at a fork by choice alone; paths are only closed by documented obstruction (Graveyard) or deprioritized by evidence after all forks are explored.

8.5 PACING & SUB-STAGES (user directive, 2026-08-17)

• NO RUSH. This is long-term research; correctness and rigor outrank speed. Take whatever time a stage needs to be done right.
• SUB-STAGE RULE: if a stage will take a few hours, break it into smaller sub-stages, each ending in a clean, committed, resumable state (per §8.4). Record sub-stage breakdowns in STATE.md.
• BREAK PROMPT: if work is running long — ESPECIALLY approaching 5:00 PM local time — pause and ASK the user whether to continue, take a break, or log off (run §8.4 end protocol before stopping).

8.6 SESSION LOG (summary; details in research/journal/)

• Session 001 (2026-08-17): Blueprint + mission prompt ingested; research archive installed (git + SQLite + LaTeX skeleton). → Begin Phase 0.
• Session 002 (2026-08-17): Phase 0 + Phase 1 complete (Track A → monitoring mode, D-013); Track C begun (3.1 D-014, E-006–E-008, 3.4a/b, D-018 Suzuki scoping).
• Session 003 (2026-08-17): Q-3.4c complete — E-009a (Suzuki g validated), E-009b (Galerkin A_a, validated vs zero side 4.5e-6; λ_a cliff), D-019 (analysis; Q-S1 verdict; E-010 proposed). Weil explicit-formula conventions machine-verified (D-001 NT-1).
• Session 004 (2026-08-17): recovered killed session (E-011 orphaned mid-edit); paper archive reorg; E-010 extended (a≤8, λ=−1); ALL 4 FORKS COMPLETE — E-010 (fork 1, session 003); E-011/R-001 (fork 2: Li λ_n > 0, n ≤ 2000, arithmetic side); 3.3 answered NO (fork 3: D-021 → G-003, E-012); T4 CLOSED (fork 4: D-022/R-002 — ξ′ strength = perfect-square node in D₁, not portable to ξ; T4b opened). Q-S3 attacked (D-023, E-014): Cor 1.6 density wall mapped to a=10 (maximal lattice, interlacing exact, no thinning — scale limitation, not a wall); θ=π candidate found; Q-S3a/b/c queued. Detached-run machinery established.
• Session 005 (2026-08-18): user approved do-all-one-by-one plan (A3→A1→A2→C→B, D in background). D launched: E-015 Li n≤3000 detached (in progress at stop; sandbox blocks multiprocessing spawn — detached launches need sandbox disabled). A3 done: E-016 + D-024 — Herglotz ρ_W at θ=π vs ρ_F; V1/V2/V4 pass, V3 (zero-Poisson reconstruction) fails rel ~0.3, root cause open; findings: θ=π zeros real, z₁(π)·a≈4.5 stiff law, no θ=π zero in (0,π/a), raw-L2 θ=π≈θ=0 (plateau-dominated metric). Stopped mid-V3-root-cause (user break; 3 network dropouts, no state loss).
• Session 006 (2026-08-18): REGROUP (user-requested). Full archive audit: all 16 experiments have CSV+JSON sidecars and db registrations; fixed db hygiene (sessions 3–5 registered; row_counts corrected for E-010– E-016). Checklist revised: Phase 2 restructured — Suzuki/Cor 1.6 line recognized as the live spectral program (2.1 partial, 2.4 active; new tasks 2.6 V3-root-cause, 2.7 Q-S3a analytic, 2.8 Q-S3b backend); 3.4 checked off (answered YES); NEW tasks 3.5 (Li asymptotic attack — most direct criterion-#1 path), 1.6 (ξ′-world ceiling), 1.7 (T4b scoping). Active order confirmed: 2.6 → 2.7 → 2.8 → 1.6 → 1.7, with 3.5 as standing high-value background thread.
• Session 006 cont. (2026-08-18): task 2.6 COMPLETE — E-016 V3 root-caused (E-016b: winding-excess diagnostic finds double zero at origin, ±iε pair; EM-tail factor-y bug found + confirmed quantitatively) and REPAIRED (E-016c: V5 1.75e-16, V6 ≤4.4e-15, V3R 1.5–2.0e-5, ALL CHECKS PASS); D-025 filed; E-016 F1–F4 stand.
• Session 006 cont.2 (2026-08-18): task 2.7 COMPLETE — breakthrough reduction: W(a,θ;z) = F·(R₀+R_τ) EXACT (F = z²ξ/ξ′, R₀ closed-form sine skeleton); Cor 1.6 ⟺ (★) tail-cancellation (Wiener–Hopf remainder, RH-gated). R-003 promoted to ledger (#5). E-017: off-axis cancellation already 99.8% at a=4; θ=π preferred; open content isolated to ℝ.
• Session 006 cont.3 (2026-08-18): task 2.8(i) complete — E-018 descent profile: (★) cancellation strip-uniform (median |M|/|R₀| ~5–7e-3, y₀∈[0.1,1]); open content = zero set of M only; θ-preference found metric-dependent. D-028.
• Session 006 cont.4 (2026-08-18): task 2.8(ii) complete — backend v2 (blockwise Λ to e²⁴, validated 2.2e-7/4.4e-8) + E-019 at a=12: NO transition (maximal lattice, z₁·a=4.495, gap CV ↓, origin pair +2.0000 winding excess, γ-proximity chance-level, envelope stationary). 2.8 CLOSED; a=13+ deprioritized by evidence (D-029). → Next: 1.6 (ξ′-world ceiling).
• Session 006 cont.5 (2026-08-18): task 1.6 COMPLETE — E-020b window optimum for kernel D₁ = 0.86864 to 1e-6 (quartic window IS the optimum; control recovers MT); ξ′-world saturated, nothing transfers to ξ; E-020 adversary-pool limitation documented (D-030). User decision: do 1.6 then 1.7 as queued (option #1). → Next: 1.7 (T4b scoping).
• Session 006 cont.6 (2026-08-18): task 1.7 COMPLETE — T4b CLOSED (D-031): node mechanism iterates formally (ξ″ ≈ 0.94 leading-order) but G-001 symmetry caps every ξ⁽ᵏ⁾ data class below 100%; Speiser/ Levinson–Montgomery route to RH closed at every order; revival condition noted. Session-005 queue (A3→A1→A2→C→B) NOW FULLY DONE. → Next: 3.5 (Li asymptotic attack) or (★) analytic attack.
• Session 006 cont.7 (2026-08-18): task 3.5 DESIGN COMPLETE (user directive: do 3.5 then (★), then analyze for next stage). D-032 literature map: Voros — "λ_n>0 ∀n≥N₀" ⟺ RH at ANY N₀; Lagarias Thm 6.1 finite-height bridge is the exploitable skeleton. D-033: achievable deliverable = EXPLICIT finite-height theorem (λ_n>0 ∀n≤N₁ ≈ 10²⁰–10²⁴ from Platt T₀ + traced constants + finite verification); wall = three-way arithmetic cancellation (triangle bounds explode). New tasks 3.6/3.7/3.8 (D-036 constants, E-021 S_∞, D-037 assembly).
• Session 006 cont.8 (2026-08-18): task (★) DESIGN COMPLETE. D-034: WH factorization + RH is unexplored territory (26 arXiv hits all Riemann–Hilbert); Krein/Gohberg–Feldman/de Branges–Krein machinery exists. D-035: resolvent-convergence route — D_{a,θ(a)}→D in Krein space; Cor 1.6 ⟺ D has real spectrum (deliverable D1); three-layer wall (index/persistence=RH/circularity); off-axis 99.8% cancellation is TAUTOLOGICAL (entirety of W forces it), the ℝ-envelope is the whole problem. New tasks 2.9/2.10/2.11.
• Session 007 (2026-08-18/19): task 3.6 marked done; task 3.7 (E-021) COMPLETE after 6-bug root-cause saga (mpmath zeta ~58-digit ceiling, GAMMA_E float literal, 3× parse-before-dps, σ-omission boundary (15/14)ⁿ, float64 zeros). E-021 ALL CHECKS PASS: V1 4.8e-25 vs E-015; A = 0.9, B₀ = 1.0 measured; c₀ = −1/4 (+1/(24n) correction); |S_f| max 13.52 at n = 3298 vs traced bound ~2280 (~170× slack). Resources folder (29 RH-equivalence notes) read in full. Next: 3.8 (D-037 → R-004 finite-height theorem assembly).
• Session 008 (2026-08-19): REGROUP + R7 registration (resources atlas indexed: resources/index.md, manifest R7, D-001 Part III pointer). Task 3.8 COMPLETE — R-004 finite-height Li theorem: λ_n > 0 for all n ≤ N₁ = (T₀−1)² ≈ 9.0×10²⁴ (T₀ = 3×10¹² Platt–Trudgian); conservative window N₁ = 2.73×10²¹. E-023 support computation ALL CHECKS PASS: D-036 |t|<10 gap found + closed (M₀ = 1.3352), S_∞ elementary lower bound validated vs exact (min slack 9.52), N₀ = 5×10⁴ adopted (crossover 32 871 traced / 30 217 measured), margin convex, margin(N₁) = 2.46×10²⁶. Ledger #6. Criterion-3 deliverable — the maximal content of the Li route short of RH. Task 2.10 COMPLETE same session: E-022/E-022b + D-040 — spectral measures μ_a (Clark weights 1/K_a(z_k,z_k)) for a ≤ 12; valley observable*: K_a(z,z) dips exactly at the true γ's, Δ(a) ≈ 3.33 − 4.76/a saturating at fixed θ=π; γ-information flows through weights, not positions; mass within ±0.1 of γ's 63→72.5%; new constraint on 2.9-D1 (θ(a) must drive Δ → ∞). Next: 2.9-D1, 2.11 (D-038); optional D-039 digamma upgrade.
• Session 009 (2026-08-19): PHASE 4 COMPLETE. Session-008 leftovers (D-052 4.1/4.2, D-053 4.3a gate PASS) committed. 4.3b (D-054): four independent-instance reviews + hand-verification — ALL THREE TAGS downgraded (D-039 proof broken/bound true; D-036 §1 far-sum O(|t| log t) hole — reference-point trick missing; D-049 B1/B3 lower bounds broken; δ_crit one-direction; T-2 ⇐ skeleton; D-052 accounting fixes). Theorem statements survive (margins robust); repair map 4.5a–4.5d opened. 4.4 (E-027 + D-055, ALL CHECKS PASS): detector stress test — bare-form negativity immediate for any δ > 0 (no threshold); tuned-carrier threshold π/(2a) exact (≤0.9%); pencil onset magnitude-limited (0.11@a=4, 0.038@a=8); directions localized at the pair. Repairs 4.5a–4.5d COMPLETE same day: D-056 (R-bound reference-point proof, A = 10.5/B₀ = 48, honest C₀) + E-028 (N₀ = 80 000, 26× slack); D-057 (convexity proved) + E-029; D-058 (valley lower bounds via node-killing; B3/m_γ/detector fixes); D-059 (bookkeeping: punctured compacts, R_τ, Lemma FD, L1). R-004 tag fully restored with the analytic chain proved end-to-end. Paper updated (R-004 constants, valley theorem corrected form, E-027 appendix item). Next: Phase 5 / paper finalization.
• Session 010 (2026-08-19): PHASE 5: 5.3 + 5.4 COMPLETE; 5.1/5.2 at skeleton stage. 5.3: paper draft fully written (Introduction, Background, Formal verification; abstract retagged; clean 12 pp MiKTeX compile). 5.4 (D-060): full honesty audit — 4 independent instances, ~55 claims, 0 unsupported; 10 draft corrections (critical: (1.12)⟺spec(D)⊂ℝ split — converse is SKELETON L3/L4; flat-window fix; B(n) explicit remainders); 7 archive errata filed (D-036 −1/(24n) sign, D-056 title constants, D-055/D-058 "0.9%" → 0.02–2.3%, D-042/D-043 Z/6 → Z/(2π) supersession by D-045, R-004 post-repair update). 5.1/5.2 (D-061): elan + v4.33.0-rc2 installed; zeta-23-lean FULL BUILD green (9010 jobs — D-007 rebuild done); 5.2 verified LIVE (all comparator PrintAxioms = 3 standard axioms, verbatim AUDIT.md match); NguyenRH1 skeleton package created (research/lean/NguyenRH1/, 9 statements compile, path-requires to the vendored repo, no new axioms, sorryAx-marked). Next: prove the elementary Lean tier (sInfty_lower_bound, marginTilde_convex) or optional numerics (E-023b, E-021 n=10⁴).
• Session 011 (2026-08-19): Lean tier (i) COMPLETE (journal-011; ~1100 lines, 10 commits; user machine crashed mid-session, zero work lost). chain_rule_sqrt_shift, sInfty_lower_bound (Bernoulli truncation
• γ-shifted harmonic bounds, parity algebra, tsum summability discharged), marginTilde_convex (8-block ψ-table + analytic IIMaj″ bound ≤ 1.316 < 2 via factor monotonicity; convexOn_of_deriv2_nonneg) all PROVED, PrintAxioms = 3 standard axioms only. End-of-session user directive: read session-012-notes.txt before Session 012.
• Session 012 (2026-08-20): Lean tier (ii) STEP 1 COMPLETE (option (a) per session-012-notes.txt, assembly-first split). lambda_pos_finite_height PROVED modulo the single named analytic hypothesis SfBoundProp (∀ n ∈ [10⁵, N₁], |Sf n| ≤ Bn FAlt n) + perimeter (RHUpTo, LiVerifiedUpTo) + 2 elementary margin evaluations (hbase/hbase2). No sorryAx in LiSkeleton.lean. Design: FAlt majorant swap (true F+S_b has ψ > 0 on [5.47,~16] — caught pre-instantiation; negative-weight term dropped, cost 0.9√n); secant two-point base (pos_of_convex_of_two_points); margin regularity → ContDiffOn (Ioi 1). D-062: SfBoundProp triage (layers L0–L7) + PERIMETER DECISION — Trudgian 2014 N(T)/S(T) inside the trusted perimeter, declared in the paper appendix (compile clean, 12 pp). D-062 §5: base-point discharge plan validated at dps 40 (plan bounds margin(8×10⁴) > 9 960; margin(10⁵) > margin(8×10⁴) by ≥ 2.2×10⁴ slack). CONTINUATION same day (session-012-end-notes.txt, mathematician review actioned): tier (ii) STEP 2 COMPLETE — LiBasePoints.lean (~560 lines) discharges both margin evaluations by certified rational interval bounds (exp ≤ (1−x/16)⁻¹⁶ trick, partial sums, d9/d20 rationals); lambda_pos_finite_height_verified = R-004 modulo SfBoundProp + perimeter ONLY (3 hypotheses), PrintAxioms clean. Paper reconciled: margin trail footnote (16 020 → 15 764 → ≥ 8 001 certified), formal-status paragraph at 3 hypotheses; compile clean 12 pp. Review guidance adopted: tier ii′ (contour interior) is post-publication; Paper A ready to split/finish.
• Session 013 (2026-08-20): PAPER SPLIT EXECUTED (user "go go" after the minor-items assessment). paperA.tex (8 pp, clean): the self-contained finite-height Li artifact — retargeted abstract/intro with the three-named-hypotheses Lean headline, §3 R-004 with the reconciled margin-trail footnote, obstruction context, Li numerics appendix, formal-verification appendix. paperB.tex (6 pp skeleton): spectral-line note opening with the §0 standing-items box (trace-or- demote R-003's FT bookkeeping/o(eᵃ); L3/L4; authorship policy). draft.tex FROZEN (pre-split combined archive copy). Minor item 1 (number-trail note) filed at 10fdda6 before the split. Author block carried verbatim except one typo fix ("fromAnthropic" → "from Anthropic"); authorship itself untouched (user's call). Also repaired: the §9 header accidentally eaten by the session-011/012 log edit. CONTINUED same day: authorship set to sole author Dan T Nguyen, Research Ai (user directive; both papers + frozen draft); AI Contribution Statement + title footnote + one-line Acknowledgments added to both papers (user directive, review template); voros2017li reference corrected (real: Exp. Math. 29(4) 2020); submission documents written (cover-letter.md targeting Experimental Mathematics + referee-list.md); pre-submission audit of NguyenRH1 ALL CHECKS PASS (D-063): clean-room rebuild green, exhaustive axiom sweep of all 139 declarations (134 standard-only + 5 intended skeletons), statement-to-paper correspondence exact, inherited comparators verbatim. Paper A is submission-ready pending the user's read-through. Paper B assessment: more experiments NOT needed (evidence ceiling documented); queued Task 1 = R-003 tempered-FT bookkeeping trace (→ D-064) as next research action.
• Session 014 (2026-08-21): TIER ii′ LAUNCHED (user decision: option (a) — close SfBoundProp in Lean BEFORE submission; Paper A frozen/submittable throughout). Sub-stage ii′-0 COMPLETE (D-064 design doc). TWO DISCOVERIES: (1) liCoeff encoding defect — unordered tsum NOT Summable (junk 0) ⟹ LiVerifiedUpTo/SfBoundProp FALSE as encoded, session-012 theorems vacuous; paired-form fix designed (ii′-1a, next). (2) Crux identity Sf(n) = Res₁(n) EXACT (Sf := S_∞+1−λ_n = the w=1 residue Σ_j C(n,j)c_{j−1}) — numerically verified: (4.10) j=0 exact 15 digits; λ₂ prediction matches E-015 certified value; residue theorem sides = λ_n(T)+triv+Res₁ verified 2e-21. Assembly TAIL-FREE: |Sf| ≤ |λ_n(T)|+|sides|+|triv| = B(n). Routes R1–R5 decided (R2(iii) (4.10) = long pole: EF-reuse first, Hadamard fallback); sub-stage map ii′-1a..7 (~9–16 sessions); all 8 planned Zeta23 dependencies axiom-checked live (clean). NOTE: the R-003 bookkeeping doc is renumbered D-065 (D-064 taken by this design doc). Freeze protocol in force.
• Session 015 (2026-08-21): ii′-1a COMPLETE — liCoeff encoding defect repaired: paired symmetric liSummand (½·mult·(f ρ + f ρ̄), manifestly real) replaces the junk tsum; liSummable PROVED (~340 lines LiSkeleton §1: geometric-sum tail bound |Re f| ≤ 2n²/‖ρ‖², (9/4)‖ρ‖² comparison, (9/2)n²·mult/(1+‖γ‖²) dominator, Zeta23 zero_sum_inv_sq + finite ball); full rebuild GREEN (8741 jobs, zero downstream changes); axiom audit 3 standard axioms only. LiVerifiedUpTo/SfBoundProp are now TRUE statements. Phase 5B checklist installed (commit 7a395b2). Next: ii′-1b residue machinery.
• Session 016 (2026-08-21): ii′-1b(i)+(ii) COMPLETE — LiResidue.lean (zetaA = (w−1)ζ analytic at 1 via removable singularity; hLi analytic, value 1, punctured agreement; lcoeff; A_iter; ResW1_eq_sum: the w=1 residue = Σ_{j=1}^n C(n,j)·lcoeff(j−1) by iteratedDeriv_mul Leibniz) + LiPrincipal.lean (rectInt_deriv_eq_zero per-side FTC; Acoeff/ppart/Gprim; rectInt'_ppart: principal part integrates to ResW1 n on any rectangle with 1 interior). 3 standard axioms only.
• Session 017 (2026-08-21): ii′-1b(iii) COMPLETE — ii′-1b FULLY DONE — LiSides.lean (~460 lines): rectInt'_Jlag, the rectangle residue theorem for the Lagarias-kernel integrand: RectangleIntegral' (Jlag n) z w = ResW1 n + Σ_{ρ∈Sz} (zeroMult ρ)·(1−(ρ/(ρ−1))ⁿ) (1 interior, ζ ≠ 0 on border, Sz = zeros inside, supplied form). Removable singularity at 1 via Taylor-remainder order ≥ n+1 (Ffun−TaylP); logDeriv-NF residues at zeros (multiple zeros OK); zeta_order_ne_top_of_ne via the entire zetaA (identity principle on univ, no punctured-plane connectedness needed; zetaA 1 = 1 makes ζ(1)'s junk value irrelevant). Root NguyenRH1.lean now imports LiResidue/LiPrincipal/LiSides; full build GREEN (8745 jobs); 19 new decls, 3 standard axioms only. Deferred: zeroMult(−2) = 1 (trivial-zero simplicity) — ii′-4. Next: ii′-2 elementary swaps.
• Session 018 (2026-08-21): ii′-2 COMPLETE — LiSwaps.lean: the two elementary swaps. R2(i) liCoeff_eq_sum_sigma: λ_n = Σ_{j=1}^n (−1)^{j+1}C(n,j)σ_j with paired power sums (per-slice summability via the ii′-1a skeleton; j=1 paired exactness Re(1/ρ) = Re(ρ)/|ρ|²). R2(ii) sInfty_eq_sum: S_∞(n) = Σ_{j=1}^n (−1)^jC(n,j)a_j (n ≥ 1; oddSlice p-series domination; the j=1 −n/m + n/m exact cancellation; Σ_{j=2}^n(−1)^jC(n,j) = n−1). 12 new decls, 3 standard axioms only; full build GREEN (8746 jobs). Next: ii′-3 (4.10), the long pole.
• Session 019 (2026-08-21): ii′-3 DESIGN (D-066) + piece (B) PROVED. Route investigation: β1 (Hadamard) OUT — Mathlib lacks Weierstrass/order machinery (extract_zeros_poles is finite-only); β2 (EF reuse) OUT — moment kernels not entire. Route β4 ADOPTED: contour moments (ii′-1b machinery) + coefficient split; R-bound identified as shared with ii′-5 ⟹ resequenced pipeline ii′-3a → ii′-4 → ii′-5 → ii′-3b → ii′-3c. Mathlib inventory verified live (digamma_one_half ✓, Weierstrass-convergence ✓, LSeries vonMangoldt ✓, logGammaSeq ✓; completedRiemannZeta₀ noted as the wrong ξ). Piece (B): LiZetaCoeff.lean — iteratedDeriv_hLiExt (coefficients of 1/s + ζ′/ζ(1+s) at 0 are −j!·lcoeff j); 6 decls, 3 standard axioms; build 8747 green. Next: piece (A) archimedean τ-evaluation.
• Session 020 (2026-08-21/22): ii′-3a COMPLETE — piece (A) PROVED: iteratedDeriv_logDeriv_Gammaℝ (the archimedean Taylor coefficients are (−1)^{j+1}·j!·a_{j+1}, all j ≥ 0). The digamma partial-fraction series built from scratch (logGammaSeq → deriv-limit interchange → Weierstrass + identity principle → iteratedDerivWithin_tsum termwise values → odd-m reindexing → 2^{j+1} scaling); LiDigamma.lean + LiArchimedean.lean. Build GREEN (8749 jobs); 18 decls audited clean. Two elaboration gotchas banked (bare π auto-binds; bare ↑ drops coe). Next: ii′-4 (L3 zero-avoiding T + L1 kernel bounds).
• Session 021 (2026-08-22): ii′-4 COMPLETE (LiContour.lean, ~400 lines, three sub-stage commits). L3 exists_zero_avoiding_T (midpoint pigeonhole on the perimeter ZeroCountProp; clearance 1/(3·C0hat(a+1))). L1 kernel bounds (kFun_norm_le_two, kFun_shift_norm_le_exp_four_add_one, kFun_shift_norm_le_exp_sqrt_half_add_one, kFun_neg_two ≤ 1) via the normSq core norm_one_add_one_div_le. Trivial-zero simplicity zeroMult_neg_two (zeroMult(−2) = 1) via ζ = (s+2)·Λ/Hfun near −2, Hfun = 4π^{−s/2}Γ(s/2+2)/s, Hfun(−2) = −2π ≠ 0, Λ(−2) = Λ(3) ≠ 0. Build GREEN (8751 jobs); 17 decls audited: 3 standard axioms only. Also (website, non-research): fixed /dashboard/ 500 (git_log cp1252 decode) + Roadmap Phase 2/5B list rendering (python-markdown list interruption) — web/ only, logged in RH-WEBSITE.md §7. Next: ii′-5 (R-bound, the long pole).
• Session 022 (2026-08-22): ii′-5a DESIGN (D-067) + ii′-5b COMPLETE. D-067: route b″ for the R-bound — Davenport disc at 2+it (R = 5/2)
• FE-reflection with exact zero-sum cancellation; Stirling-free (digamma_stirling subsumes Lemma D), Hadamard-free; the "every disc dips left of σ = 0" obstruction resolved by one extra EM level. ii′-5b (LiRBound.lean, ~640 lines): b2Fun machinery (comp_fract'' continuity trick), the level-2 IBP identity integral_b1_cpow_eq, parameter-integral analyticity (re > −1), the level-2 ζ representation via the convex W± regions (sidesteps the punctured-halfplane connectedness grind), and norm_riemannZeta_le_disc (‖ζ‖ ≤ (3/4)|t|² on B(2+it, 5/2), |t| ≥ 10). Build GREEN (8752 jobs); 27 decls axiom-clean. Next: ii′-5c (Davenport disc argument).
• Session 023 (2026-08-22, HALT BY USER at a clean boundary): ROUTE REVISION (D-067 §6) — the disc-only BC constants provably cannot reach the baked 10.5/48 (factor ≥ 16× the M-coefficient) ⟹ two-stage plan: loose disc bound = growth input for the partial-fraction identity (5e), then D-056's tight analysis of the identity (5f). ii′-5c HALF (LiDisc.lean, green): zeroDiscFinset + zeroDisc_isNontrivial (re ≥ 1 via Mathlib's one_le_re nonvanishing; re ≤ 0 via ΓR-pole/FE); scaledZeta + F(0) = 1 (Zeta23 zeta_lower_bound_two, no μ-series build); the multiplicity-invariance chain (affine/const-mul/scaled); scaledZeta_jensen_count (ZerosBound). Next: 5c back half — R-gap, g analytic+nonvanishing, BC assembly.
• Session 024 (2026-08-22): ii′-5c COMPLETE (commit c7cbae5; LiDisc.lean +~1000 lines, 32 new decls, all audited: 3 standard axioms only). R-gap selection by the ×10-RESCALE TRICK (zero new pigeonhole code: exists_avoiding_midpoint at a = 23 on the ×10 zero-norm image, ÷10 ⟹ R_c ∈ [2.3, 2.4], clearance gapD = 1/(50(k+1))); the Blaschke quotient g = Cf r_c F built entirely on Zeta23's Cf API (CfAnalytic/ZeroFactorization; nonvanishing on closedBall(0, r_c) — the gap makes the sphere zero-free); |g| ≤ (9/4)|t|²·gapD^{−M_c} by max-modulus; center log|g(0)| ≥ 0; LogOfAnalyticFunction (r = 3/5, R = r_c) + BorelCaratheodoryDeriv (16M·r_c²/(r_c−3/5)³ ≤ 450M); logDeriv chain (div/prod/pow/comp) + the affine push-forward (sum_image + order invariance) + the near/extras split (extras ≤ Jensen count via |s−ρ| ≥ |t−γ| ≥ 1). Capstone logDeriv_riemannZeta_sub_nearZeros_le: the LOOSE R-bound ≤ 100000·(log|t|)² on σ ∈ [1/2, 7/2], |t| ≥ 10, ζ s ≠ 0 — no perimeter hypothesis (Jensen count, not ZeroCountProp). Constant fold: log(33/32) ≥ 1/33 (log x ≥ 1−1/x), log 4150 ≤ 9 (e > 2.71), M_bound ≤ 420L². Build GREEN (8753 jobs; LiDisc now root-imported). Next: ii′-5d (FE-reflection + left digamma bound).
• Session 025 (2026-08-22): ii′-5d COMPLETE (LiReflect.lean, ~640 lines, 26 new decls, all audited: 3 standard axioms only). The FE logDeriv identity logDeriv_zeta_fe (via Λ =ᶠ ΓR·ζ near good points
• the Λ(1−z) = Λ(z) chain-rule negation); the EXACT zero-sum cancellation sum_nearZeros_neg_reflect (nearZeros(−t) = image under ρ ↦ 1−ρ by the symmetric ball estimate (1+ρ.re)²+(ρ.im−t)² ≤ 5; zeroMult invariant by analyticOrderAt_zeta_one_sub); the ΓR +4 shift logDeriv_Gammaℝ_shift (Gammaℝ_def + Gamma_add_one twice + exp-form cpow arithmetic) putting both digamma arguments in re > 0, then StirlingVert digamma_stirling ⟹ ΓR-bracket ≤ 4(log|t|)². Capstone logDeriv_riemannZeta_sub_nearZeros_le_left: the loose R-bound ≤ 200000·(log|t|)² on σ ∈ [−5/2, 1/2], |t| ≥ 10. PLUS the 5e input norm_digamma_sub_log_le_of_two_le_abs_im: ‖ψ(w) − log w‖ ≤ 3 for 2 ≤ |im w|, uniform in the shift chain (digamma_add_natCast + first-order EM sum_eq_integral_add_integral_deriv + arctan-FTC ∫dx/((x+a)²+c²) ≤ π/c — no full-line integral needed). Build GREEN (8761 jobs; LiReflect root-imported). Banked gotchas: this Mathlib's add_le_add_left/right are swapped vs classic; push_cast EM conclusions before linear_combination; single-cast sum families. Next: ii′-5e (partial-fraction identity), first item zeroMult(−2n) = 1 for all n (generalize ii′-4c).
• Session 026 (2026-08-22): ii′-5e PREP + DESIGN COMPLETE (commit 0d9887a). LiTrivialZeros.lean (~290 lines, 8 decls audited clean): gamma_mul_prod (product-form Γ recurrence by induction on Gamma_add_one) + the HfunT n cofactor (analytic/nonzero at −2n)
• zeroMult_neg_two_mul: zeroMult(−2n) = 1 for ALL n ≥ 1 (the ii′-4c pattern via analyticOrderAt_eq_natCast). D-068 (5e design): F entire via principal-part splits (no removable-singularity theorem, no Hadamard); TWO CORRECTIONS to D-067 §6 — (C1) circle series bound O((log R)³) via the RADIAL split (the naive annulus split gives O(R log R) — fatal); (C2) near-axis left-plane digamma bound separate (recurrence + separated reciprocal sum). Sub-stage map 5e-i..v. Banked: DifferentiableAt.analyticAt does NOT exist (use fun_prop); Gammaℝ_eq_zero_iff gives −(2*↑m); lt_trichotomy exists / le_or_lt does NOT. Next: ii′-5e-i (γ-gap circles).
• Session 027 (2026-08-22): ii′-5e-i + 5e-ii COMPLETE (commits e28eff6, 0e9336e, ec13029; two new files, 17 decls, all audited: 3 standard axioms only). 5e-i (LiGapCircles.lean): exists_gapCircle_radius — R ∈ [4k+5/2, 4k+3] with dist(R/2,ℤ) ≥ 1/4 and ordinate clearance ≥ 1/(16·C0hat(4k+9/2)) (the ×2-rescaled midpoint pigeonhole + C0hat_mono). 5e-ii (LiDigammaLeft.lean): the telescope tail + norm_digamma_le_of_two_le_re (B: Weierstrass split, harmonic head + telescoping tail, integers via digamma_natCast_eq) + digamma_recip_sum_le (C: the V-split separated reciprocal sum) + norm_digamma_le_of_dist_nat (A: the near-axis bound via digamma_add_natCast′ — pole-avoidance form, covering real points) + logDeriv_Gammaℝ_eq (G: logDeriv ΓR s = −(log π)/2 + ½ψ(s/2) for im ≠ 0, the m-fold shift). Build GREEN (8764 jobs). Banked: ascribe cast haves (stuck typeclasses else); pin ℕ-sub casts (Nat.cast_sub before push_cast; elaborator lifts Real.log (m−k) to real-sub); sum_add_tsum_nat_add's shifted terms are beta-redexes (state goals in redex form); prod_range_succ's f explicit-first. Next: ii′-5e-iii (the zero series).
• Session 028 (2026-08-23): ii′-5e-iii COMPLETE (LiSeries.lean, ~600 lines, 22 decls, all audited: 3 standard axioms only). The zero-side partial-fraction series seriesFun s := ∑' ρ : nontrivial zeros, mult·(1/(s−ρ)+1/ρ): seriesSummable at every s (the ii′-1a D-trick; tail 2‖s‖/‖ρ‖² via 1/(s−ρ)+1/ρ = s/(ρ(s−ρ)); the (17/12)‖ρ‖² γ-comparison; Zeta23 zero_sum_inv_sq dominator); seriesFun_analyticAt
• seriesFun_analyticOnNhd off the nontrivial zeros (the three-case avoiding balls: ζ≠0 continuity / ζ=0 order normal form / s₀=1 zetaA; the Weierstrass M-test of_norm_le_summable_eventually + the journal-020/021 TendstoLocallyUniformlyOn→differentiableOn→ analyticOnNhd pattern); nontrivialZero_isolated (finite unit-ball min-distance); seriesFunSub_analyticAt (the ρ₀-term-zeroed series analytic AT ρ₀); seriesFun_sub_term (the everywhere split seriesFun = seriesFunSub + the ρ₀-term); capstone seriesFun_sub_polar_analyticAt (series − mult/(s−ρ₀) analytic at ρ₀) — the 5e-iv residue-cancellation input. Build GREEN (8765 jobs, LiSeries root-imported). Banked: redex-RHS show-before-rw; no rw at set-var-dependent hypotheses (standalone membership iff route); obtain-rfl needs a variable RHS; if_pos/if_neg under binders via simp only; Finset.image lambda type-pinning; file ends end NguyenRH1 then end; push_neg/Set.mem_setOf_eq deprecated. Next: ii′-5e-iv (F entire by the principal-part splits).
• Session 029 (2026-08-23): ii′-5e-iv COMPLETE (commits 58e03e2 + closure; LiFEntire.lean, ~1130 lines, 30 decls, all audited: 3 standard axioms only). F ENTIRE: the difference Fexpr = logDeriv ζ − seriesFun + 1/s + 1/(s−1) − (log π)/2 + ψ(s/2)/2 extends via the punctured limit Gentire s := limUnder (𝓝[≠] s) Fexpr (Mathlib has no general removable-singularity theorem; the junk point-values are sidestepped by limUnder uniqueness + per-bad-point analytic witnesses). Witnesses: nontrivial zeros (the NF logDeriv witness + 5e-iii polar subtraction), s = 1 (logDeriv zetaA), s = 0 (digamma-series split, ψ(s/2)/2 + 1/s = −γ/2 + ½·series), s = −2n (NF + zeroMult_neg_two_mul + the dropped-term series H_n). Support: zeta_zero_classification (every zero is nontrivial/0/−2n — the LiDisc argument globalized via completedRiemannZeta_eq_zero_iff + Gammaℝ_eq_zero_iff), analyticAt_digamma (off {0}∪−ℕ). Capstone gentire_analyticAt_and_eq: Gentire analytic everywhere AND equal to Fexpr at every good point. Build GREEN (8766 jobs, LiFEntire root-imported). Banked: AnalyticAt.comp HOU pin (f := ...); the (−2↑n)/2 non-defeq value-normalization; cast-leaf vs single-cast pinning (((x:ℤ):ℂ) forms); abs_re_le_norm as the robust norm-of-cast-expr route; eventually_ne's implicit target pinned by ascription; EventuallyEq wrapper vs raw ∀ᶠ (show-bridges); subst eliminating the wrong local. Next: ii′-5e-v (the circle bound O((log R)³) + the max-modulus squeeze ⟹ ∃ B capstone).
• Session 030 (2026-08-23): ii′-5e-v STARTED — 5e-v-a + 5e-v-b chunk 1 COMPLETE (commits 5d24756, e6a654b; LiCircleBound.lean, ~340 lines so far, clean elaboration, not yet root-imported). 5e-v-a: isNontrivialZero_conj; the count bridges — A0count from Zeta23's RvM zeta_local_zero_count (mult-weighted, two-sided, ALL t, unconditional — the series-bound count input) + Ncount_window_le / Ncount_add_of_le / Ncount_chain_le / Ncount_le_of_interval / Ncount_le_of_interval_gen; norm_logDeriv_zeta_le_dirichlet (‖ζ′/ζ‖ ≤ dirichletC2 for re ≥ 2, the LSeries vonMangoldt pattern from ZetaBounds); 5e-v-b chunk 1: tsum_split_finset (tsum = finset sum + if-zeroed tail via tsum_eq_sum) + lowZeros/ lowZeroConst. Full remaining design (tail bound via ENNReal.tsum_fiberwise + the key machinery; the one-split series bound; logDeriv/elem assembly; Schwarz squeeze; ∃ B capstone) in journal-030. Banked: le_or_gt (le_or_lt absent); finsum_mem_union/ finsum_mem_empty/tsum_eq_sum forms; Nat.cast_nonneg ascription; Ncount_add_of_le endpoint pinning; nested calc-by parser fragility; positivity vs Classical.choose defs; [DecidableEq ι] for statement-level ifs; root.riemannZeta_conj. Next: 5e-v-b chunk 2 (the tail bound + the main series circle bound).
• Session 031 (2026-08-23): ii′-5e-v-b chunk 2 COMPLETE (commits c26241c, f984afc, closure 8f16424; LiCircleBound.lean ~830 lines, clean). The far-tail bound zero_tail_inv_sq_le: Σ_{|γ|>X} m/(1+γ²) ≤ 16·A0count·log X / X for X ≥ 200 — the dyadic fiber machine: dyadClass (Nat.log-2 classes) + lower/upper bounds, dyadClass_fiber_finite, fiber_mult_count (the two-window cover via Ncount_le_of_interval_gen), fiber_tail_le (per-fiber bound via tsum_subtype + tsum_eq_sum + filter split), tsum_dyadic_log (closed form 10 log 2 + 2 log X via hasSum_coe_mul_geometric) and the ENNReal.tsum_fiberwise + ofReal_tsum_of_nonneg assembly. Banked: coercion-lambda type-pinning in Finset.image/filter/ sum_subtype (use Subtype.val); the unary-minus precedence (-(2^(j+1) * X) parenthesization + abs_neg/neg_mul); Finset.disjoint_left; tsum_subtype explicit args; indicator_of_notMem camelCase; of_norm_bounded's norm-kept goal; rw-pow_succ' rfl-close (no trailing ring); nlinarith can't multiply hypotheses by factors — rw the pow identity at goal+haves first. Next: 5e-v-b chunk 3 (the main seriesFun circle bound).
• Session 032 (2026-08-23): ii′-5e-v-b chunk 3 COMPLETE (commits 787b9c0, 727f656, d2bfde6, 222d65d + capstone; LiCircleBound.lean ~2867 lines, clean, zero warnings; audit-session032-axioms.txt: 19 decls, 3 standard axioms only). The series circle bound seriesFun_norm_le_gapCircle: ‖seriesFun s‖ ≤ 2·lowZeroConst + 2900·A₀·Ĉ₀(4k+9/2)·(log R)² on the γ-gap circle (k ≥ 4000). Pieces: 3a gapCircle_threshold (416·Ĉ₀ ≤ 4k+5/2, explicit exp/log arithmetic) + not_isNontrivialZero_on_gapCircle; 3b seriesTerm_norm_eq_div, circleZeros R, the count brick sum_zeroMult_le_of_im_band (band [a,b] + sign-separation c ⟹ 3·A₀·(b−a+2)·log(3·max|a||b|+5) via the (M−1,b] ∪ (−b−1,−M] two-window cover), series_tail_le (91·A₀·log R), seriesFun_norm_le_split; 3c dyadic_family_le (generic machine via Finset.sum_fiberwise_of_maps_to with t := Ico 1 (J+1) — avoids the Fintype-ℕ gap), shell_low (2·lowZeroConst), shell_inlo/shell_inhi (60·A₀L²), shell_up (45·A₀L², dyadic class reaches J+1), shell_crit (2688·Ĉ₀A₀L: uniform separation 1/(32Ĉ₀) — strip arcs |t−γ| ≥ 1/(32Ĉ₀) via the γ-gap (conj for γ < 0) + the threshold; near-axis |s−ρ| ≥ √13−1), and the five-way partition assembly. Banked: linarith can't relate distinct reciprocal atoms (bridge P = 2Q by field_simp first); sum_fiberwise needs Fintype (use sum_fiberwise_of_maps_to); sum_image's f is auto-bound (pin (f := ...)); Finset.eq_empty_iff_forall_notMem; div_le_div_of_nonneg_right exists / div_le_div_right does NOT; floor-integrality must route through ℕ +1-cast before linarith; filter-conjunction nesting ⟨hF, pred⟩; lt_of_not_le does NOT exist (lt_of_not_ge). Next: 5e-v-c (logDeriv/elem assembly ⟹ ‖Fexpr‖ ≤ C(log R)³).
• Session 033 (2026-08-23): ii′-5e-v-c COMPLETE (commits 1c76576, 5da957c + capstone; LiCircleBound.lean ~3928 lines, clean, zero warnings; audit-session033-axioms.txt: 14 decls, 3 standard axioms only). The Fexpr circle bound Fexpr_circle_le: ‖Fexpr s‖ ≤ 2·lowZeroConst + dirichletC2 + 400000·A₀·Ĉ₀(R+2)·(log R)² on the γ-gap circle (k ≥ 4000). Pieces: c-i differentiableAt_Gammaℝ_of_not_neg_nat + logDeriv_Gammaℝ_eq_of_not_neg_nat (the (G) formula at ANY non-pole point incl. s = −R — direct logDeriv_mul on Gammaℝ_def, digamma := logDeriv Γ by def, no continuity argument) + gapCircle_sep (standalone γ-gap separation) + nearZeros_count_le + gapCircle_sep_of_mem_nearZeros; c-ii digamma_right_le (48+23·log) + digamma_circle_le (uniform 62+23·log(2+R/2): strip sub-log, right_le, left near-axis via 5e-ii (A) c = 1/8 from the ℤ-clearance — the R+re s = im²/(R−re s) identity, no square roots) + elems; c-iii logDeriv_circle_le (three regions: Dirichlet / 5c+5d capstones + near sum ≤ 32Ĉ₀·count / FE logDeriv_zeta_fe with all 10 hyps discharged + Dirichlet at 1−s + ΓR bracket) and the six-norm-chain assembly. Banked: riemannZeta_ne_zero_of_one_le_re takes ONLY re; div_lt_iff₀ is a/c<b here (lt_div_iff₀ for a<b/c); add_le_add_left/right SWAPPED (use per-step norm haves + linarith); rw [X = 1*X] rewrites everywhere (use calc); linear_combination -h for the 1−s bridges; congrArg Complex.re + simp for cast-bridges; left-assoc products through every calc; Real.pi_lt_d2 : π < 3.15; abs_one/abs_neg for |x±1|; one_div_le_one_div_of_le takes the small side's positivity first. Next: 5e-v-d (Schwarz squeeze ⟹ ∃ B capstone partialFraction_identity).
• Session 034 (2026-08-23): ii′-5e-v-d COMPLETE — ii′-5e DONE (commit 5a262a1; new file LiSqueeze.lean, ~330 lines, clean, zero warnings; LiCircleBound + LiSqueeze root-imported; full build GREEN; audit-session034-axioms.txt: 5 decls, 3 standard axioms only). C0hat_add_two_le (Ĉ₀(R+2) ≤ 5·log R, R ≥ 16002); not_badPoint_on_gapCircle (every gap-circle point good); gentire_circle_le (the circle bound transfers to Gentire); gentire_const (the Schwarz squeeze: max-modulus via Zeta23's AnalyticOn.norm_le_of_norm_le_on_sphere + the ball-form Schwarz lemma on the γ-gap circle sequence; growth RB ≤ C₀′ + 64·C₁·Q³ with Q := R^{1/4}, R = Q⁴ (Real.log_le_rpow_div + pow_le_pow_left₀ + rpow_inv_natCast_pow), radius choice Q ≥ 2 + (128·C₁+2·C₀′)·‖z₀‖/ε ⟹ dist ≤ ε ⟹ Gentire ≡ Gentire 0); THE CAPSTONE partialFraction_identity (hZC : ZeroCountProp): ∃ B : ℂ, ∀ s good, logDeriv riemannZeta s = B + seriesFun s − 1/s − 1/(s−1) + (log π)/2 − ψ(s/2)/2 — the partial-fraction identity Lean-proved modulo ONLY the declared perimeter (first perimeter use in the 5e chain: the γ-gap circles need ZeroCountProp). Banked: le_or_lt absent (le_or_gt + the dist/2 contradiction closes the squeeze); set-Q + rw [← hQ] after push_cast for the rpow_inv_natCast_pow bridge; log_le_rpow_div's exponent-hypothesis form. Next: ii′-5f (D-056's tight constants 10.5/48 from the identity) → ii′-3b → ii′-3c → ii′-6 → ii′-7.
• Session 035 (2026-08-23/24): ii′-5f STARTED — 5f-0 + 5f-i + piece 6 COMPLETE (commits 75172e6, f850d9a, 0cca091, d808f52, 1eeda9b, c9c1362, b5e3f53). Perimeter repair (user-approved): ZeroCountProp strengthened to the mult-weighted form (the second ii′-1a-class encoding defect — the unweighted set-card under-captured the declared Trudgian N(T) source; one_le_zeroMult bridge via analyticOrderAt_ne_zero + ENat.toNat_pos; exists_zero_avoiding_T + exists_gapCircle_radius adapted via card ≤ Σ mult; full build GREEN; audit-session035-axioms.txt: 5 decls, 3 standard axioms only). P1/P2 perimeter additions (user-approved, D-069): ZeroCountProp2 (the two-unit Trudgian specialization 0.6·L + 0.886·LL + 2.7) + NoLowZeros (|γ| ≥ 14, Platt-class zero-location certificate). D-069 Finding 1: D-056's piece-2 one-C₀ usage is for a TWO-unit window — the honest two-unit form makes the assembly fit 10.5/48 (margin ≈ 1.9). Finding 2 (ii′-6 map): H(T) clearance coverage (honest ≈ 7·Ĉ₀² vs baked 3·Ĉ₀²). 5f-i (LiTightR.lean, new file): tsum_split_finset_complex, nearZerosSub, seriesDiffTerm + seriesFun_sub_seriesFun, Rexpr_decomp (the six-piece reference-point decomposition; B cancels; linear_combination hsid − hs₀id + hdiff + hsplit + hnear), piece 1 dirichletC2_le_one (the level-2 integral machinery: hasDerivAt_neg_log_add_one_div + integral_Ioi_of_hasDerivAt_of_tendsto'
• AntitoneOn.tsum_comp_add_le_integral + the log2/log3 numeric fold), piece 2 near_sum_refPoint_le, pieces 4/5 one_div_diff_le (≤ 0.045). 5f-ii piece 6: log_diff_le (the segment-FTC log bound ≤ 5/t) + digamma_diff_le (‖(ψ(s/2)−ψ(s₀/2))/2‖ ≤ 6/t via the +2 shift + StirlingVert.digamma_stirling + digamma_add_natCast). The sharp Lemma-D remainder turned out UNNECESSARY (digamma_stirling's 3/im² suffices; piece 3's sharper interval sum freed the budget). Banked: the real-cast-first ((t/2 : ℝ) : ℂ)·I form; re/im ext-goals via explicit per-component rw chains; field_simp can close the goal; Summable.sum_add_tsum_nat_add method form; cpow_natCast's (2:ℂ) = ((2:ℕ):ℂ) bridge. Next: piece 3 (the far-sum interval machine) → 5f-iii (assembly + pinch + capstone) → ii′-3b → ii′-3c → ii′-6 → ii′-7.
• Session 036 (2026-08-24): ii′-5f COMPLETE (commits 79c506b, 0829421, 7a2af96, 642b851, 22b98c9, b347559, 52bb2cb, e6d57e1). Piece 3 (LiTightR.lean sections 9–19, ~2700 lines): certified numerics (integral-comparison log machines + all certified log/exp/ sqrt bounds), the farW weight with S₃ ≤ 1.3476 (4 exact sqrt-rational terms + telescope 1/4), the six tail bricks via the antitone-integral machine (RW₀/1/2 = 0.1/0.3303/0.1216 with the loglog ≤ (1/e)log trick; LA₀/1/2 = 1/23/0.1687/0.0621 with the −log x/(x+10) + (1/10)log(x/(x+10)) antiderivative), the C0hat bridges (2k+1/j+1/ 2t+1 + C0hat(2t+1) ≤ C0hat(t+1)+0.55), the conj machinery (hasDerivAt_conj_of_conj_eq → iteratedDeriv_riemannZeta_conj → analyticOrderAt_riemannZeta_conj → zeroMult_conj), farG + summability
• the per-term bound + norm reduction, the main bucket machine (unit_family_le + main_bucket_count + farG_main_le), the two tail machines (farGLeft_le ≤ 1.1729, farGRight_le ≤ 2.7343, ENNReal fiberwise cloned from LiCircleBound), the tail split farG_tail_eq, and far_series_le ≤ 12.1284·C₀ + 7.2425. 5f-iii (sections 20–21, ~550 lines): the pinch lemma pinch_tight_R (11.6318·LL − 4.6484·L ≤ 0.397094 for L ≥ log 12 — concave tangent at the certified critical point 2.5024, f′ antitone, FTC both directions, f(2.5024) ≤ −0.96231 certified), the supporting bounds (log 12 = 4 log 2 − log(4/3) ≥ 2.4848 via the 4-term neg_log machine, log 12 ≤ 2.5024, log 3 ≤ 1.0987, log 2.5024 ≤ 0.9173), the C0hat L/LL conversion, and THE CAPSTONE logDeriv_riemannZeta_sub_nearZeros_le_tight (hZC) (hZC2) (hNLZ): ‖logDeriv ζ s − Σ_{near} m/(s−ρ)‖ ≤ 10.5·log(t+2) + 48 PROVED (six-piece assembly: dirichletC2 ≤ 1 + near two-unit 0.6L+0.886LL+2.7 + far 12.1284·C₀+7.2425 + 2×0.045 + 6/t ≤ 0.6; fold 5.8516L + 11.6318LL + 47.6029 ≤ 10.5L + 48 via the pinch). Audits session036/036b: 33 decls, 3 standard axioms only; full build GREEN (8762 jobs). Banked: a * b / c parses as (a·b)/c (write c * (b / d) with parens or isDefEq explodes); Float-literal pinning; rw first-unifier-only; x⁻¹ vs 1/x; div/mul_le_mul signatures; pow_nonneg for odd powers; Summable.mul_left/add lambda forms; tsum_add beta-rfl bridges; two_le_C0hat for C0hat nonnegativity; pinch coefficient-exactness (mixed-sign rounding breaks large L). Next: ii′-3b (moments) → ii′-3c → ii′-6 → ii′-7.
• Session 037 (2026-08-24, HALT at a clean boundary — user log-off): capstone dependency audit (user-requested, pre-ii′-3b): AuditSession037.lean + audit-session037-axioms.txt — #print axioms logDeriv_riemannZeta_sub_nearZeros_le_tight = [propext, Classical.choice, Quot.sound] ONLY; the exact perimeter recorded verbatim (ZeroCountProp unit-window mult-weighted ≤ Ĉ₀(t+1); ZeroCountProp2 two-unit 0.6L+0.886LL+2.7; NoLowZeros |γ| ≥ 14; nearZerosSub/Zeta23.zeroMult/zeroAbsWindow constructs). ii′-3b STARTED — ROUTE REVISION (D-070): the moments (M) come from 5e's partialFraction_identity by pure algebra + series calculus (NO contours — the contour work was 5e's): gFun := logDeriv xiL = B + seriesFun at good points; xiL entire via the Λ₀ closed form; perimeter ZeroCountProp ONLY (5f's hZC2/hNLZ not needed). LiMoments.lean §1–§4 COMPLETE, build GREEN (~730 lines): xiL + conj/reflect subtype equivs, (G) gFun_eq_momentB, evaluations gFun_zero/gFun_one/gFun_one_eq_neg (FE sign), the summability budget (master Σ mult/‖ρ‖² + AM-GM mixed bound), the reindex machinery (sigmaP_eq_unpaired k ≥ 2 via the conj reindex, vTerm_tsum_eq_zero via V = W = −V), k = 1 PROVED: sigmaP_one_eq_neg_gFun_zero (2σ₁ = seriesFun 1 = −2·gFun 0 by the FE sign). §5/§6 fully designed + Mathlib-probed (iteratedDerivWithin_tsum/ SummableLocallyUniformlyOn_of_locally_bounded/iteratedDeriv_neg/ AnalyticAt.contDiffAt/Equiv.tsum_eq/Summable.tsum_add signatures all confirmed); skeleton banked in journal-037. Banked: SummationFilter refactor (tsum_add/tsum_sub are method-form Summable.tsum_add only; tsum_neg/tsum_zero/tsum_congr/tsum_mul_left plain); eq_zero_of_neg_eq needs LinearOrder (ℂ N/A → 2V = 0 route); Complex.norm_conj takes starRingEnd directly; ascribe EVERY tsum binder (zeroMult ρ coerces ρ to ℂ otherwise); beta-redex show-before-rw; deriv_comp's point arg explicit; field_simp's trailing-ring errors ×3. Housekeeping: Scratch.lean (old session-029 audit script) overwritten with the lemma probe — session-029 audit results preserved in audit-session029-axioms.txt. Next: LiMoments §5 (termwise iterated derivation at 0, k ≥ 2) → §6 (capstone sigmaP_eq_neg_iteratedDeriv_gFun_div) → root import (with LiTightR) → audit → ii′-3c.
• Session 038 (2026-08-24): ii′-3b COMPLETE (LiMoments.lean §5/§6, ~290 new lines, file now ~1020 lines). §5: iteratedDeriv_zpow_neg_one, iteratedDeriv_seriesTerm, seriesTerm_deriv_summableLocallyUniformlyOn (the M-test on ball(0, δ/2); dominator j!·2^{j+1}·(1/δ)^{j−1}·mult/‖ρ‖²; the h1/h2/h3 one_div/div_pow/pow_add chain), iteratedDeriv_seriesFun_zero (the LiDigamma:749–785 iteratedDerivWithin_tsum pattern verbatim; local pole_free via norm_sub_norm_le + norm_sub_rev). §6: gFun_eventuallyEq_zero (eventually_nhdsWithin_iff + point values) + THE CAPSTONE sigmaP_eq_neg_iteratedDeriv_gFun_div (hZC : ZeroCountProp): sigmaP k = −(iteratedDeriv (k−1) gFun 0)/(k−1)! PROVED for ALL k ≥ 1 (k=1: §4 reindex; k≥2: (G) + §5 + per-term sign algebra (−1)^k·(−1)^{k+1} = −1 + ← sigmaP_eq_unpaired + field_simp k! ≠ 0 — FIRST-PASS GREEN). Perimeter: ZeroCountProp ONLY. Closure: LiTightR + LiMoments root-imported; full build GREEN (8770 jobs); AuditSession038.lean + audit-session038-axioms.txt — 23 decls, [propext, Classical.choice, Quot.sound] ONLY, 0 sorryAx. Banked: factorial ! needs open scoped Nat (the parse error looks like spacing); Summable.mul_left dominators CONSTANT-FIRST (D ρ * C whnf-loops the refine); rw [seriesFun] fails UNAPPLIED (show beta-expansion); norm_sub_norm_le has no abs on the LHS here; simpa-only a copy of memberships before rw-ing them away; (neg_neg _).symm funext direction; simp only [neg_mul, neg_neg] for buried negs; iteratedDeriv_add needs the Pi.add bridge (hsplit := rfl); calc reassociation via trailing mul_assoc. CONTINUED same day: ii′-3c COMPLETE (LiCrux.lean, ~430 lines, root-imported) — the FE relation (gFun_one_sub_fun + iteratedDeriv_gFun_zero via the unconditional iteratedDeriv_comp_const_sub), the shift expansion (gFun_one_add_punctured/eventuallyEq), iteratedDeriv_gFun_one ⟹ lagarias_4_10_a (hZC) PROVED (all k ≥ 1) ⟹ THE CRUX sf_eq_resW1 (hZC) PROVED: (ResW1 n).re = Sf n for n ≥ 1 — Sf(n) = Res₁(n) in Lean, perimeter ZeroCountProp only. Full build GREEN (8771 jobs); audit session038b: 8 decls, 3 standard axioms only. ii′-3 (ALL of (4.10)) DONE. Banked: ContDiffAt.congr_of_eventuallyEq takes hev NOT hev.symm; Finset.sum_add RENAMED Finset.sum_add_distrib; succ-normalize via Nat.succ_eq_add_one before Nat.add_sub_cancel; simp using X.deriv silently derails (use the direct .deriv term); ContinuousAt.comp numerals not kernel-defeq (add_zero-rw hg FIRST); show-statements ASCII-only (U+2212 breaks the parser); ← hS direction after sum-splits; mul_div_cancel_left₀ for (s·X)/s; div_add_div + div_eq_div_iff + ring as the always-works fraction pattern. CONTINUED: ii′-6-0 DESIGN COMPLETE (D-071 + E-030 ALL CHECKS PASS) — THREE findings: F-A bridge factor-2 (λ_n(T) both-signs ⟹ honest 4·FAlt vs baked 2·FAlt; R-004 unaffected, paper erratum at ii′-7), F-B I_III two-unit count ((2/3)Z2 vs (2/3)Ĉ₀ — D-069 Finding 2 exact), F-C baked Bn unprovable beyond ~5×10⁷ (killers T·log T outgrow (log T)² slack: 0.656 at 10⁵ → 1.012 at 10¹²). USER-APPROVED 8-step protocol: redefine Bn honestly (4F, (2/3)Z2hat); convexity re-proof; base points re-certification (values improve); endpoint margins re-run; ii′-6 against corrected Bn; paper correction note at ii′-7; audit history preserved (E-030). Perimeter additions approved: ZeroCountGlobalProp + MZeroProp. CONTINUED: ii′-6-a COMPLETE — Bn redefined honestly (4F, (2/3)Z2hat); marginTilde_convex re-proved (ψ-row literals + norm_num; Z2hat added to the eq_expanded unfold list; a hardcoded const_mul fixed); base points re-certified (329,000/350,000; margins ≥ 7,001/82,501); endpoint margins re-run (14,682/90,653/2.458×10²⁶); full build GREEN (8771 jobs); audit session038c: 3 standard axioms only. Banked: lake env lean uses the STALE olean — lake build the dependency first; re-check certified constants at 1e-4 (114.0655 vs 114.06553 linarith catch). CONTINUED: ii′-6-b COMPLETE — perimeter Props ZeroCountGlobalProp
• MZeroProp declared; wide pigeonhole exists_zero_avoiding_T_wide; LiAssembly.lean NEW (sides identity + bridge ‖Σ‖ ≤ 4·FAlt + 1); build GREEN (8772 jobs); audit session038d: 3 standard axioms only. Banked: RectangleBorder-rcases trap (rw + simp only + tauto route); Finset.image plain-function + Set.InjOn; set-x breaks mem_toFinset; linarith proves ≠; projections for IsNontrivialZero; sq_eq_sq₀; pow_le_one₀ implicit n. CONTINUED to ii′-6-c design-check — FINDING F-D (D-072, session end, user paused to think): the (6.12) stepping in Lagarias's Thm 6.1 is broken at T = √n (product ratio e/2 > 1; right-tail ~e^{0.066√n}, ~5.9×10¹⁰ envelope at n = 10⁵ measured by E-031); D-036/D-037/R-004's B(n) inherits it (charge "3.3" off by ~10⁷×; margin collapses for n ≳ 3×10⁴). The theorem statement survives (verified to 5×10⁵; sides cancel by conjugation + phase winding); all Lean work to date survives (the bug is in the horizontal piece, not yet built). Repair path (R) verified numerically: T = c√n with c > 1.2012 ⟹ the stepping works (monotone decrease at c = 1.5, 2); N₁ → (T₀/c)² ≈ 2.25–4×10²⁴. Literature: no erratum found. Session ends at a clean committed boundary with the direction OPEN.
• Sessions 039–044 (2026-08-25/26): F-D repair (side thread ii′-6-R, then the D-074 dog-leg), ii′-6-c..d + ii′-7 CLOSURE (lambda_pos_finite_height_closed, seven hypotheses), Paper A closure + three review rounds + freeze at 13 pp — recorded in §5B above, journals 039–042/044 and STATE.md (journal-043 not written; git log 4001c5d..eca7fab).
• Session 045 (2026-09-01): PAPER A EXPERT-REVIEW REVISION (five reviewer suggestions; user: apply all). §2 (certificate-method background) and §4 (obstruction analysis) DELETED — Paper B material; the density theorem removed from the framing (zeta-23-lean cited only as the imported Lean library; grep-verified that no density-theorem statement is referenced by NguyenRH1); the Lagarias (6.12) gap VERIFIED against the published AIF 2007 version (pp. 1724–1725 verbatim; no erratum; arXiv v4's remainder correction concerns (6.13)) and stated so in §2.1; NEW Appendix C deriving the three zero-count perimeter Props from Rosser Thm 19 + Trudgian-II ((1.2), Cor. 1, Thm 1) — FINDING (D-075): ZeroCountProp is Rosser-derivable only to log u ≈ 106.6 (two-endpoint coefficient 0.433155 > 0.433), Trudgian Thm 1 needed beyond, and LiSqueeze uses it at radii → ∞, so the attribution is "Rosser and Trudgian" (abstract/intro/App. B corrected); enlarged-majorant cost 0.9√n → 1.8√n (4F form). E-035 ALL CHECKS PASS (grid check; precision gotcha banked: pass window widths exactly). Paper 15 pp, clean. cover-letter.md rewritten (stale since session 013), referee-list.md updated; sessions 043–045 registered in research.db. Next: user read-through → submission decision.

9. SUCCESS CRITERIA (ordered)

1. 🏆 Full proof of RH (formally verified).
2. 🥇 Unconditional improvement past 2/3 (or past 0.6725 / 5/6).
3. 🥈 New equivalence, reduction, or removal of a known obstruction.
4. 🥉 Rigorously documented obstruction map advancing the field.