Current task: —

Updated 08-26-2026

Session 040 (2026-08-25) — D-074 dog-leg repair: DL-0 through DL-6 COMPLETE

Mission

Execute PROJECT_DIRECTIVE_D-074.txt (the zero-free dog-leg repair of the F-D broken (6.12) stepping): keep T_cut = √n (⟹ the ORIGINAL N₁ = (T₀−1)² ≈ 9×10²⁴), deform only the right horizontal tail [3, 2√n] up to U = (3/2)√n through the unconditionally zero-free region Re ≥ 3.

Sub-stages DL-0 → DL-6, each committed per the crash-safe protocol.

DL-0 — design + audit + E-034 + fold (commit 8f9ccb2)

DL-1 — the exact deformation identity in Lean (commit 4c36802)

LiDogLeg.lean (new): Jlag_differentiableAt_dogleg + holomorphicOn_Jlag_dogleg (Re s ≥ 3 zero-free via Mathlib riemannZeta_ne_zero_of_one_lt_re, NO perimeter, no pigeonhole at U); rectangleIntegral(_')_Jlag_dogleg_eq_zero (Cauchy via HolomorphicOn.vanishesOnRectangle); the capstone upper_right_horizontal_eq_dogleg: H(3→X_R, T) = H(3→X_R, U) − V(X_R, T→U) + V(3, T→U); kFun_conj/Jlag_conj. Build 8773, audit clean.

DL-2 — the V_left bound (commit b959a31)

kFun_three_add_it_norm_le_exp_five_halves_add_one (kernel ≤ e^{5/2}+1, the 1+5/(4+t²) computation); dirichletC3 ≤ 1/2 (termwise 3-vs-2 comparison + dirichletC2 ≤ 1 — C_zeta3 charged 0.5, fold-indifferent; the tight 0.165/0.17 upgrade path documented in D-074 §4); norm_logDeriv_zeta_le_half; capstone vIntegral_Jlag_three_norm_le: ‖VIntegral (Jlag n) 3 T U‖ ≤ (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 — the H_high stepping (commit 6eaf531)

norm_term/norm_logDeriv_zeta_le_two_pow (the (6.10) halving in LSeries form: ‖ζ′/ζ(σ+it)‖ ≤ 2^{−(σ−2)}·dirichletC2); one_add_div_pow_norm_le_exp_four_ninths (the kernel envelope e^{(4/9)σ} — SINGLE-EXPONENTIAL form replacing the unit-step geometric series, the D-073 R(1.5) alternative); Jlag_dogleg_norm_le_envelope (dirichletC2·(4e^{−cσ}+4·2^{−σ}), c = log 2 − 4/9); integral_exp_neg_le (the FTC machine); certified constants (cdog_gt c ≥ 0.2487; exp_four_thirds_le e^{4/3} ≤ 3.8073); capstone hIntegral_Jlag_dogleg_norm_le ≤ 8.38 (charged with dirichletC2 ≤ 1; the tight R(1.5) = 5.94 = documented tightening path). E-034 re-validated at HHigh = 8.38: ALL CHECKS PASS.

DL-4 — the far-right vertical drop (commit 4bc3c09)

kFun_right_vertical_norm_le_exp_sqrt_half_add_one (the w = 2√n kernel variant: ‖kFun n (2√n+it)‖ ≤ e^{√n/2}+1, n ≥ 16, t² ≥ n — the 4√n−1 ≤ t² computation); vIntegral_Jlag_right_norm_le ≤ (U−T)(e^{√n/2}+1)·2^{−(2√n−2)}·dirichletC2 — exponentially tiny. VRightBound charged IIMaj/2 at the time (later re-charged IIMaj/4 by DL-6-ii). E-034 re-validated at IIMaj/2: ALL CHECKS PASS.

DL-5 — the total right-horizontal bound (commit 737397a)

hIntegral_Jlag_low_le_dogLegUpper + the lower side by conjugation (hIntegral_Jlag_low_neg_norm_le_dogLegUpper via Jlag_conj + intervalIntegral.intervalIntegral_conj) + dogLegUpper_two_sides: both horizontal right tails ≤ ((√n+1)/2)(e^{5/2}+1)/2 + 8.38 + IIMaj/4 (IIMaj/2 at the time; upgraded to IIMaj/4 by DL-6-ii). The full dog-leg proved in Lean, no perimeter, nothing above T_cut.

DL-6 — the direct dirichlet bound at re = 2√n (commit a19172f)

KEY UNBLOCK of the I_I/0.57 problem: the I_I charge in IIMaj is 0.57·2^{−(2√n−2)} (the (6.10)-route |ζ′/ζ(2)|); certifying dirichletC2 ≤ 0.57 directly needs a ~100-prime partial-sum build (the antitone-integral tail is too fat at K ≤ 1000). AVOIDED: the DIRECT dirichlet-series bound at re = 2√n — log2-leading + 3^{−(2√n−2)} tail (dirichletC2 ≤ 1) — gives norm_logDeriv_zeta_le_iimZeta: ‖ζ′/ζ(2√n+it)‖ ≤ 0.57·2^{−(2√n−2)} for n ≥ 5 — the IIMaj zeta form exactly, NO dirichletC2 ≤ 0.57 anywhere. Pieces: dirichletCX + norm_term_vonMangoldt_X_le_three_pow + dirichletCX_le + log_nine_quarters_ge (log(9/4) ≥ 0.8109 via the e/e^{0.1891} tight route) + four_ninths_rpow_sqrt_le ((4/9)^{√n} ≤ 0.164 certified) + three_pow_neg_two_sqrt_sub_two_eq + V_right ≤ IIMaj/4 EXACTLY (vIntegral_Jlag_right_le_IIMaj_quarter). DL-5 upgraded to the quarter charge (dogLegUpper = VLeft + 8.38 + IIMaj/4 ⟹ the fold's total IIMaj coefficient is I_I + 2·(1/4) = 1.5·IIMaj — the convexity-safe coefficient: 1.5·(4/3-bracket)/(4n) = 1/(2n) strictly). E-034 re-validated at IIMaj/4: ALL CHECKS PASS (margins 13 160/88 911/ 2.458e26 — IIMaj ~ 10⁻¹⁰⁵ invisible).

State at checkpoint

Banked (technical)

Next (per the D-074 §8 return map)

ii′-6-a2 (the Bn dog-leg redefinition at the DL-5 quarter-charge constants + the bracket < 4/3 cherry-pick from the paused branch for the 1.5·IIMaj convexity) → the ORIGINAL plan resumes: ii′-6-c (four side bounds with the repaired horizontal) → ii′-6-d (fold ⟹ sfBoundProp) → ii′-7 (closure at the ORIGINAL N₁ = 9×10²⁴).

CONTINUATION (same-day block B): ii′-6-a2 committed; ii′-6-c STARTED; FINDING F-E

What was done (in order)

  1. ii′-6-a2 COMMITTED (0dfbd6e) — the Bn dog-leg redefinition (DogLegRight def + Bn/marginTilde/marginExpanded/mK lockstep + convexity re-proof at 1.5·IIMaj + base points re-certified: margin(8e4) ≥ 4 001, hbase2 66 001 < 80 501; build GREEN 8773 jobs; audit 41 decls, 3 standard axioms only, 0 sorryAx). NOTE: git identity is passed per-command (git -c user.name="NGUYEN-RH-1" -c user.email="research@local" commit ...) — the machine's git config has NO identity; do NOT set config (project safety rule), use the -c flags.
  2. ii′-6-c pre-flight — read LiAssembly.lean (sides identity + bridge), D-071 §4.4 (four-side designs), Zeta23 ResidueCalcOnRectangles (RectangleIntegral = H bottom − H top + V right − V left), the 5f tight capstone signature (logDeriv_riemannZeta_sub_nearZeros_le_tight: σ ∈ [−5/2, 3], 10 ≤ t, s.im = t, ζ s ≠ 0 ⟹ ≤ 10.5·log(|t|+2)+48), nearZerosSub (|γ−t| < 1, subtype finset), ZeroCountProp2 (= Z2hat closed form), the kernel lemma signatures.
  3. FINDING F-E (D-074 §9, committed 8068ea6) — the I_I (right vertical σ₁ = 2√n) kernel charge e^{√n/2}+1 is OFF BY ONE: kFun_shift_norm_le_exp_sqrt_half_add_one takes re s ≥ 2√n at the SHIFTED point s+1 (i.e. re w ≥ 2√n+1), DL-4's direct variant needs t² ≥ n — neither applies at re w = 2√n near t = 0, where the true kernel is (2√n/(2√n−1))ⁿ = e^{√n/2+1/8} > e^{√n/2}. Latent in the ORIGINAL D-036 charge (same defect class as F-A/F-B; margin unaffected — I_I ~ 10^{−106} at n = 8×10⁴). REPAIR ADOPTED: charge I_I honestly as e^{1/3}·IIMaj(n) — uniform-in-t kernel ≤ e^{√n/2+1/3}+1 for n ≥ 4 (|w/(w−1)| ≤ 1+1/(2√n−1) by normSq monotonicity in t² (worst at t = 0), add_one_le_exp, and n/(2√n−1) ≤ √n/2+1/3 ⟺ n ≥ 4 pure algebra). The overrun vs the charged IIMaj is absorbed by the fold's FREE dropped 2π normalization (D-071 §4.5: ‖RectInt'‖ ≤ Σ sides/(2π) ≤ Σ sides; e^{1/3} ≤ 1.4 ≤ 2π — one linarith step in ii′-6-d). NO change to Bn/IIMaj/DogLegRight/convexity/pinch/base points. The fatten-IIMaj alternative (0.57 → 0.8) was REJECTED: iimaj_bracket_bound is an ABSOLUTE ψ̃-bracket with 4.56 = 2·2·0.57·4 as a LINEAR factor (certified product 4.56×1.2237×0.2124×1.1099 = 1.3155) — ×(0.8/0.57) pushes it to 1.847 > 4/3 and breaks marginTilde_convex.
  4. 6-c-i scaffolding COMPLETE (a8c5b1e) — LiSideBounds.lean (build GREEN): Z2hat_mono; nearZerosSub_mult_sum_le (Σ mult ≤ Z2hat t, the LiTightR image/subset bridge + hZC2); continuousAt/On_logDeriv_zeta (analyticity quotient: ((analyticAt_riemannZeta h1).deriv).div _ hζ); Jlag_norm_eq (‖Jlag‖ = ‖kFun‖·‖logDeriv‖); zeta_ne_zero_left_vertical (classification at re = −5/2); zeta_ne_zero_horizontal (wide- pigeonhole clearance); rectangleIntegral_Jlag_eq (the four-side decomposition at rectZ/rectW); VIntegral_norm (I• drops); HIntegral_split; jlag_left_vertical_norm_even.
  5. 6-c-ii STARTED (I_III left vertical) — design fully worked out (see STATE.md NEXT ACTION for the per-piece recipe); no Lean written yet beyond the scaffolding.

Decisions

Banked (this block)

State at stop