Current task: —

Updated 08-26-2026

D-074 — Zero-free dog-leg repair of the Lagarias horizontal right tail (design + progress anchor)

Date: 2026-08-25 | Session: 040 (thread START) | Status: DL-0 COMPLETE (E-034 ALL CHECKS PASS; A–L report §7) — AWAITING USER GATE before DL-1 (Lean) Directive: PROJECT_DIRECTIVE_D-074.txt (repo root, user-authored — the persisted mission; §19's work order = execute §2–§11 then STOP and report answers A–L). This file is the in-archive design/progress anchor (the D-073-pattern: nothing lives only in conversation). Evidence: E-031 (finding), E-032 (hidden-cancellation diagnostic), E-033 (c-repair constants), E-034 (planned dog-leg validation). Related: D-072 (Finding F-D), D-073 (the c-repair side thread — Lemma 4.1

0. Mission and plan-integration (user directives 2026-08-25)

MISSION (D-074): recover the ORIGINAL finite-height endpoint N₁ = (T₀−1)² ≈ 9×10²⁴. Keep T_cut = √n (the residue cutoff, the RH bridge, and λ_n(T_cut) are UNCHANGED); replace ONLY the broken right horizontal tail [3, 2√n] (Finding F-D) by a zero-free dog-leg up to U = (3/2)·T_cut, where D-073's repaired stepping applies (q = e^{4/9}/2 < 1). The dog-leg rectangle lies entirely in Re w ≥ 3 (our w-convention; Lagarias's Re(s+1) ≥ 4) — ζ zero-free + no pole UNCONDITIONALLY, so the Cauchy deformation is exact and needs NO new perimeter and NO RH above T_cut.

PROTOCOL DIRECTIVES (user, same date): (i) the plan is integrated into the standard protocol (NGUYEN.md §5 entry ii′-6-DL + this anchor + index/db registration); (ii) stop-and-go at any time without loss — crash-safe per NGUYEN.md §8: artifacts saved IMMEDIATELY when produced, a clean committed state at every sub-stage, this file's progress log (§1) is the in-thread stop-and-go record, STATE.md updated LAST with an explicit NEXT ACTION; (iii) when this plan completes, the ORIGINAL plan resumes and finishes the theorem — the return map is §8 below.

BACKGROUND (established; do not re-derive): Finding F-D (D-072 — the (6.12) stepping is broken at T = √n; both ingredient bounds sharp; no side-wise fix possible there). E-032 (the T = √n per-side claim is empirically TRUE via hidden cancellation but envelope-unprovable; mid-segment [−5/2, 3] honest). D-073 (the repaired stepping Lemma 4.1

THE DESIGN (our w-convention, rectInt'_Jlag: integrand Jlag(w) = k_n(w−1)·(−ζ′/ζ(w)), right tail w = σ+iT_cut, σ ∈ [3, 2√n], T_cut = √n + ε zero-avoiding). Replace H_low (σ : 3 → 2√n at height T_cut) by the dog-leg:

Key properties: N₁ stays (T₀−1)² (only T_cut enters the bridge); Bn's dog-leg charge decomposes into C·√n + const + IIMaj-shaped ε — the SAME block shapes as the existing margin machinery (convexity re-proofs with coefficient edits only; the parked c = 1.5 k-shift branch wip/c-1.5-margin-redo (642d47a) is NOT needed for this route and stays parked as the fallback). Estimated Bn impact ≈ +2.2·√n (~700 at n = 10⁵ vs margin ~9×10⁴; margin(N₁) marginally smaller but the range is the full 9×10²⁴).

1. Progress log (append one entry per sub-stage; crash-safe record)

2. Coordinate/convention audit (directive §2)

All items verified live in the Lean sources (session 040). The Lean contour MATCHES the assumed geometry — no STOP condition triggered. The one convention note: the Lean integrand is Jlag n s = (s/(s−1))ⁿ−1 · (−ζ′/ζ(s)) — i.e. k_n(s−1) with k_n(x) = (1+1/x)ⁿ−1, ζ evaluated at s (= Lagarias's s+1). The dog-leg region Re s ≥ 3 is Lagarias's Re(s+1) ≥ 4. Same region, shifted names.

mathematical object current Lean name (file:line) shift domain orientation existing lemma(s)
integrand Jlag n s = kFun n s * (-(deriv ζ s / ζ s)) (LiSides.lean:58) s = w (Lagarias's s+1) ℂ ∖ ({1} ∪ {ζ-zeros}) — Jlag_differentiableAt (needs s ≠ 1, ζ s ≠ 0), LiSides:82
kernel kFun n s = (s/(s−1))ⁿ − 1 (LiSides.lean:55) = k_n(s−1), k_n(x) = (1+1/x)ⁿ−1 pole order n at s = 1 — kFun_differentiableAt (s ≠ 1), LiSides:63
main rectangle corners rectZ T = −5/2 − iT, rectW n T = 2√n + iT (LiAssembly.lean:64–65) variant B — — —
orientation convention RectangleIntegral f z w = H f z.re w.re z.im − H f z.re w.re w.im + V f w.re z.im w.im − V f z.re z.im w.im; RectangleIntegral' = (1/(2πi))•RectangleIntegral (Zeta23 FromPNTPlus.ResidueCalcOnRectangles:52–59); H f x₁x₂y = ∫{x₁}^{x₂} f(x+yi)dx, V f x y₁y₂ = i∫{y₁}^{y₂} f(x+yi)dy — — CCW: bottom L→R, right ↑, top R→L, left ↓ —
upper horizontal (II) top side: −H f z.re w.re (w.im) — im = +T_cut R→L (x : 2√n → −5/2) —
lower horizontal (IV) bottom side: +H f z.re w.re (z.im) — im = −T_cut L→R (x : −5/2 → 2√n) —
right vertical (I) +V f w.re z.im w.im — re = 2√n ↑ (y : −T → +T) —
left vertical (III) −V f z.re z.im w.im — re = −5/2 ↓ (y : +T → −T) —
right edge X_R 2 * Real.sqrt n (= rectW's re) — 2√n ≥ 632 (n ≥ 10⁵) — —
T_cut (zero-avoiding) the wide-pigeonhole T — T ∈ [√n, √n+1] — exists_zero_avoiding_T_wide (LiContour:404): ∃ T ∈ [a,a+1], clearance 1/(9·Ĉ₀(a+2)) vs zeros with im ∈ (a−1, a+2), a ≥ 3
sides identity sf_abs_le_rectInt_add_zeroSum (LiAssembly.lean:76) T-window as HYPOTHESES (√n ≤ T ≤ √n+1 + clearance) Sz = {nontrivial, |γ| ≤ T} ∪ {−2} — |Sf n| ≤ ‖RectInt‖ + ‖Σ‖
bridge zeroSum_norm_le_four_FAlt_add_one (LiAssembly.lean:443) hTle : T ≤ 3×10¹²−1 hypothesis — — ‖Σ‖ ≤ 4·FAlt T + 1 (hRH)
kernel, left vertical kFun_norm_le_two (LiContour:449) s.re ≤ 1/2 — — ‖kFun n s‖ ≤ 2
kernel, mid charge kFun_shift_norm_le_exp_four_add_one (LiContour:503) kFun n (s+1), s.re ≤ 3, n ≤ (im s)² — — ≤ e⁴+1
kernel, I_I / V_right kFun_shift_norm_le_exp_sqrt_half_add_one (LiContour:553) kFun n (s+1), 2√n ≤ s.re — — ≤ e^{√n/2}+1
right-half-plane ζ bound norm_logDeriv_zeta_le_dirichlet (LiCircleBound) re s ≥ 2 — — ‖ζ′/ζ s‖ ≤ dirichletC2 := ∑'‖LSeries.term Λ 2 n‖ (≈ 0.57)
I_I majorant IIMaj n (LiSkeleton:754) — — — Bn's I_I piece; IIMaj_le_two_mul, IIMaj_nonneg
"3.3" entry point (BROKEN, D-072) Bn/marginTilde horizontal share: 2 * (Real.exp 4 + 1) * (7 * Hhat T + 3.3), T = √n+1 (LiSkeleton Bn:2431, marginTilde:766, mK:1832) — — — the F-D inheritance — DL replaces ONLY this
conj machinery riemannZeta_conj, isNontrivialZero_conj, zeroMult_conj (LiTightR, session 036) — — — NO Jlag_conj lemma yet — DL-1 builds it (Jlag n (conj s) = conj (Jlag n s), short)
perimeter ZeroCountProp, ZeroCountProp2, NoLowZeros, ZeroCountGlobalProp, MZeroProp — — — declared (D-062 §4 + session-038 additions)
2π slack RectangleIntegral' is (2πi)⁻¹-normalized; Bn charges the RAW side bounds (the paper's convention; the 1/(2π) is spare slack) — — — D-071 §4.5

Dog-leg-specific consequences of the audit:

  1. The dog-leg region [3, X_R]×[T_cut, U] has Re s ≥ 3 > 1: ζ nonvanishing UNCONDITIONALLY (Mathlib nonvanishing for re > 1) and s ≠ 1 (im ≥ T_cut ≥ 315) — Jlag analytic on a neighborhood. No new perimeter; NO pigeonhole/zero-avoidance needed at U (that is the point of the design).
  2. The upper right tail [3, X_R] is traversed R→L in the main contour; the dog-leg pieces inherit compatible orientations (§3).
  3. H_high needs kernel-ratio ≤ e^{n/U²} ≤ e^{4/9}: U ≥ (3/2)√n ⟹ U² ≥ (9/4)n ✓ — the T_cut pigeonhole's +1 slack is harmless (U := (3/2)·T_cut with T_cut ∈ [√n, √n+1] ⟹ U ≥ 1.5√n ✓).
  4. The bridge/sides-identity lemmas take T_cut as a parameter with explicit window hypotheses — the dog-leg does NOT touch them; Sz stays {|γ| ≤ T_cut} ∪ {−2}.
  5. The broken "3.3" sits ONLY in the horizontal share of Bn/ marginTilde/mK — DL-0's fold replaces exactly that slot.

3. Exact dog-leg derivation (directive §§3–5, 9, 10)

3.1 Analyticity (directive §4) — no new perimeter

On the open neighborhood Ω := {s : 2 < Re s, T_cut − 1 < Im s < U + 1} of the closed dog-leg rectangle [3, X_R]×[T_cut, U]: (i) s ≠ 1 (Im ≥ T_cut − 1 ≥ 314); (ii) ζ(s) ≠ 0 — Mathlib's nonvanishing for 1 < Re s (the Euler-product region; UNCONDITIONAL, no perimeter); (iii) kFun analytic off s = 1 (kFun_differentiableAt); (iv) −ζ′/ζ analytic (analyticAt_riemannZeta + (ii)); hence Jlag is analytic on Ω ⊃ [3, X_R]×[T_cut, U]. [PROVED-modulo-Lean-build — DL-1 formalizes; analyticity content: standard + Mathlib]

3.2 The exact deformation identity (directive §5)

Cauchy's theorem on the dog-leg rectangle (analytic on a neighborhood, §3.1 — zero residues, the residue-sum side is EMPTY; no perimeter):

RectangleIntegral (Jlag n) (3+iT) (X_R+iU) = 0

which expands (the Zeta23 H/V convention, CCW) to

H(3→X_R, T) − H(3→X_R, U) + V(X_R, T→U) − V(3, T→U) = 0,

where H(a→b, y) = ∫_a^b Jlag(σ+iy) dσ and V(x, a→b) = i∫_a^b Jlag(x+it) dt. The main contour's upper right tail is the REVERSED low segment (the top side runs R→L), i.e. −H(3→X_R, T). Solving:

upper right tail = −H(3→X_R, T) = −H(3→X_R, U) + V(X_R, T→U) − V(3, T→U) = [H_high, traversed X_R→3 at U] + [V_right, traversed T→U at X_R] + [V_left, traversed U→T at 3].

Equivalently, in the same-direction (L→R / upward) forms for bounding: H(3→X_R, T) = H(3→X_R, U) − V(X_R, T→U) + V(3, T→U). (★)

INTERPRETATION (directive §9, prominent): we bound |∫ Jlag| AFTER analytic deformation — |H(3→X_R, T)| ≤ |H(3→X_R, U)| + |V(X_R)| + |V(3)| — NOT ∫|Jlag| along the dangerous low path (the e^{0.066√n} envelope of F-D never enters). Finding F-D cannot be reintroduced: the low-path envelope is simply abandoned, not bounded.

3.3 The three piece bounds (directive §§6–8)

V_left (lift at Re = 3). For t ∈ [T_cut, U], t² ≥ T_cut² ≥ n: |kFun n (3+it)| = |(3+it)/(2+it)|ⁿ − 1's magnitude ≤ ((9+t²)/(4+t²))^{n/2} + 1 = (1+5/(4+t²))^{n/2} + 1 ≤ exp(5n/(2(4+t²))) + 1 ≤ e^{5/2} + 1 (log(1+x) ≤ x, 5n/(2(4+t²)) ≤ 5/2). And |ζ′/ζ(3+it)| ≤ Σ_{m≥2} Λ(m)/m³ = −ζ′(3)/ζ(3) ≤ C_zeta3 (absolute convergence, Re = 3 > 1; termwise ≤ the s = 3 sum — the dirichletC2 argument at 3). Hence

|V_left| ≤ (U − T_cut)·(e^{5/2}+1)·C_zeta3 ≤ ((√n+1)/2)·(e^{5/2}+1)·C_zeta3 =: VLeftBound(n),

since U − T_cut = (1/2)T_cut ≤ (√n+1)/2. (True value −ζ′(3)/ζ(3) = 0.16482; VLeftBound ≈ 1.09·(√n+1) ≈ 1.07·√n.)

H_high (traverse at U = (3/2)T_cut ≥ (3/2)√n). D-073 Cor 4.2 APPLIES VERBATIM with U in place of T: (i) kernel ratio per unit step ≤ (1+1/U²)ⁿ ≤ e^{n/U²} ≤ e^{4/9} (U² ≥ (9/4)n); (ii) the (6.10) halving (σ ≥ 3 > 2, unconditional Dirichlet); (iii) the initial kernel charge e^{4n/(9+U²)} ≤ e^{16/9} at Re(w−1) ∈ [2,3]. With q := e^{4/9}/2 < 1 (certified, §4):

|H_high| ≤ ∫₃^{X_R} |Jlag(σ+iU)| dσ ≤ Z₀·[ e^{16/9}/(4(1−q)·log 2) + 1/(2·log 2) ] = R(1.5) ≤ 5.94 =: HHighBound(n),

Z₀ = |ζ′/ζ(2)| charged at its certified upper edge 0.5703661 (E-033 V1). HHighBound is n-INDEPENDENT. [D-073 Lemma 4.1 + Cor 4.2, PROVED elementary; constants E-033-validated]

V_right (drop at X_R = 2√n). Kernel (ii′-4 kFun_shift_norm_le_exp_sqrt_half_add_one, t-independent): |kFun n (X_R+it)| ≤ e^{√n/2}+1. Zeta: |ζ′/ζ(X_R+it)| ≤ 2^{−(X_R−2)}·Z₀ ≤ 0.57·2^{−(2√n−2)} ((6.10), X_R > 2). Hence

|V_right| ≤ ((√n+1)/2)·(e^{√n/2}+1)·0.57·2^{−(2√n−2)} =: VRightBound(n) (= (1/4)·IIMaj(n) exactly — IIMaj(n) = 2(√n+1)(e^{√n/2}+1)·0.57·2^{−(2√n−2)}).

3.4 The total right-horizontal bound (directive §9)

Per side (upper; lower by conjugation — the Jlag conj identity Jlag n (conj s) = conj (Jlag n s) from ζ's conj-symmetry and kFun's real-coefficient form, DL-1):

|H_low| ≤ VLeftBound(n) + HHighBound(n) + VRightBound(n) =: DogLegRight(n).

The full horizontal charge in Bn becomes (both sides): mid [unchanged: (e⁴+1)·(NI + 5.5·(10.5·log(T+2)+48)) per side] + DogLegRight(n) per side, ×2.

3.5 The §10 dependency statement (why N₁ = (T₀−1)² survives)

4. Candidate rational constants (directive §§6–8)

All certifiable by the LiBasePoints machinery (rational interval bounds; NO floats into Lean):

constant value certification route
C_zeta3 ≥ −ζ′(3)/ζ(3) = 0.16482268… → charge 0.165 (first hand-estimate 0.150 was WRONG — series truncated early; caught by the E-034 smoke test) Dirichlet partial sum Σ_{m≤K} Λ(m)/m³ + certified tail (2·log(K−1)+1)/(4(K−1)²) (E-034 V1: partial 0.1648226814 + tail 8.5e-9)
e^{5/2}+1 ≤ 13.19 e²·e^{1/2} ≤ 7.3891·1.6488 = 12.185 → 12.19 (+1); d9-rational route
e^{4/9} ≤ 1.56 (< 2 — the q-condition) e^{4/9} = e/e^{5/9}: e ≤ 2.7183, e^{5/9} ≥ Σ₀⁷(0.5556ⁱ/i!) ≥ 1.7430 ⟹ ≤ 1.5596 → 1.56
q = e^{4/9}/2 ≤ 0.78 (< 1) from the e^{4/9} bound
Z₀ = |ζ′/ζ(2)| ≤ 0.5703661 E-033 V1's certified upper edge (already charged)
VLeftBound(n) ((√n+1)/2)·13.19·0.165 ≈ 1.088·(√n+1) the assembled explicit form
HHighBound(n) 5.94 D-073 R(1.5) charged (E-033: 5.93924)
VRightBound(n) (1/4)·IIMaj(n) exact identity with IIMaj/4
DogLegRight(n) VLeftBound + 5.94 + IIMaj/4 ≈ 1.088·(√n+1) + 5.94 + ε per side

The Bn horizontal share (both sides) becomes: 2·(e⁴+1)·[NI + 5.5·(10.5·log(T+2)+48)] + 2·DogLegRight(n) replacing the broken 2·(e⁴+1)·[NI + 5.5·(10.5·log(T+2)+48) + 3.3]. ΔBn vs session-038 honest Bn ≈ 2·(1.088·(√n+1) + 5.94) − 2(e⁴+1)·3.3 ≈ +2.2·√n − 355 at 10⁵ (i.e. ≈ +350 at 10⁵ against margin ~9×10⁴; the fold analysis is E-034's §6 job).

3. Exact dog-leg derivation (directive §§3–5, 9)

(to be written — the deformation identity with audited orientations; the analyticity statement (no new perimeter); the prominent "bound |∫| after deformation, NOT ∫|·| along the low path" note; V_left/H_high/V_right bounds with the exact constants; the conjugation transfer; the §10 dependency statement (residues/λ_n(T_cut)/RHUpTo only via T_cut ≤ T₀).)

4. Candidate rational constants (directive §§6–8)

(to be written — C_zeta3 (rational ≥ −ζ′(3)/ζ(3)); e^{5/2}+1 certified; e^{4/9} < 2 certified; q = e^{4/9}/2 < 1 certified; VLeftBound(n), HHighBound(n), VRightBound(n) explicit forms; no floats into Lean.)

5. E-034 numerical validation (directive §11)

E-034 (research/numerics/scripts/E-034-dogleg-validation.py + CSV/JSON sidecars, db-registered, dps 50): ALL CHECKS PASS (V1–V6 + VA; session 040). Architecture: certified-tail Dirichlet series primary (σ ≥ 5), mpmath (σ ∈ [3,5) + verticals) validated against it (discrepancy ≤ 5.0×10⁻¹⁰); two trapezoid grids per piece (h-delta ≤ 5×10⁻⁵).

V1 (C_zeta3 certified): −ζ′(3)/ζ(3) ∈ [0.1648226814, 0.1648226899] (partial K = 25 000 + certified tail 8.5×10⁻⁹); charged 0.165. [The first hand-estimate 0.150 was WRONG — caught by the smoke test; recorded for honesty.] V2 (kernel charge): e^{5/2}+1 = 13.182494 ≤ 13.19. V3 (q certified): q = e^{4/9}/2 = 0.77981175 ≤ 0.78 < 1 (e^{4/9} = 1.55962 < 2).

V4 (the identity is EXACT) — |H_low − (H_high − V_right + V_left)|:

n T_cut U residual quadrature tol
10³ 31.6728 47.5092 5.0×10⁻⁵ 3.9×10⁻⁴
10⁴ 100.05 150.075 4.5×10⁻⁵ 3.5×10⁻⁴
10⁵ 316.6278 474.9417 2.1×10⁻⁵ 2.2×10⁻⁴

(residuals at the quadrature-convergence level — the identity holds to the measured precision; H_low cross-validates E-032's independent values 7.18463/16.7016/26.2292 EXACTLY.)

V5 (piece slack) — measured vs majorant:

n |V_left| / VLeftBound |H_high| / 5.94 |V_right| / VRightBound |H_low| / DogLegRight
10³ 8.01 / 35.5 (0.23) 1.11 / 5.94 (0.19) 2.3e-14 / 2.5e-11 7.19 / 41.44 (0.17)
10⁴ 16.98 / 109.9 (0.155) 1.09 / 5.94 (0.18) 1.3e-43 / 3.7e-37 16.7 / 115.8 (0.144)
10⁵ 26.0 / 345.2 (0.075) 1.01 / 5.94 (0.17) 2.9e-136 / 6.9e-120 26.23 / 351.1 (0.075)

All ratios ≤ 1 with slack 4–13× (V_right: 120+ orders). Note |V_left| ≈ |H_low| itself — the lift carries the dominant share of the dog-leg charge, as designed.

6. Temporary fold vs N₁ (directive §11 gate)

The temporary dog-leg Bn (session-038 honest Bn with the broken 2(e⁴+1)·3.3 replaced by 2·DogLegRight(n), DogLegRight = VLeftBound + 5.94 + IIMaj/4, NOT multiplied by the mid kernel charge):

n Bn_DL(n) margin_DL(n) = S_∞ − Bn_DL + 1
8×10⁴ 323 654 14 419 (session-038 broken charge: 14 682 — cost 263)
10⁵ 343 432 90 317 (broken: 90 653 — cost 336)
10⁸ 6.44×10⁶ 7.73×10⁸
10¹² 8.19×10⁸ 1.24×10¹³
N₁ = 9×10²⁴ 4.44×10¹⁵ 2.458×10²⁶ (the ORIGINAL endpoint)

Full fold: honest_DL(n) ≤ Bn_DL(n) on the dense grid [8×10⁴, N₁] (the mid-segment fit NI + 5.5(10.5 log+48) ≤ 7Ĥ is the unchanged E-030 fit, max ratio 0.3986); margin > 0 everywhere (min on grid 14 419 at 8×10⁴). GATE (directive §11): PASS.

7. DL-0 report (directive §19, answers A–L)

A. Is the dog-leg contour identity exact? YES — Cauchy deformation in the zero-free region; verified numerically to 2–5×10⁻⁵ (the quadrature-convergence level) at n = 10³/10⁴/10⁵, cross-validating E-032 exactly. B. Is the entire deformation zero-free/unconditional? YES — Re s ≥ 3 > 1 (Euler-product nonvanishing, Mathlib), Im ≥ 314 (no pole, no trivial zeros), kernel analytic off s = 1. NO perimeter, NO pigeonhole at U. C. Certified left-lift constant? C_zeta3 = 0.165 (certified bracket [0.1648226814, 0.1648226899]); kernel ≤ e^{5/2}+1 ≤ 13.19; VLeftBound(n) = ((√n+1)/2)·13.19·0.165 ≈ 1.088·(√n+1). D. q at α = 3/2? q = e^{4/9}/2 = 0.77981175 ≤ 0.78 < 1 (certified e^{4/9} < 2). E. Certified high-horizontal bound? HHighBound = 5.94 (D-073's R(1.5), E-033-charged, n-independent; measured |H_high| ≤ 1.11). F. Certified far-right vertical bound? VRightBound = IIMaj/4 (measured 2.9×10⁻¹³⁶ at 10⁵ — negligible at every scale). G. Total horizontal charge replacing the broken 3.3? DogLegRight(n) = VLeftBound + 5.94 + IIMaj/4 per side (≈ 1.088·(√n+1)

DL-0 VERDICT: the design is validated on every directive gate. Awaiting the USER GATE before DL-1 (Lean: dog-leg analyticity + the exact deformation identity).

8. RETURN TO THE ORIGINAL PLAN (after D-074 completes)

This thread REPLACES the horizontal right-tail piece of ii′-6-c; it does not fork the main line. On completion (DL-5 + ii′-6-a2 done):

  1. ii′-6-a2 (Bn dog-leg redefinition, the freeze-exception protocol: honest Bn with horizontalRightDoglegBound(n) explicit; D-074/E-034 documentation; marginTilde_convex re-proof (coefficient-level — same block shapes); base-point re-certification; endpoint margins at N₁ = (T₀−1)²; git history preserved; paper-correction queue; full axiom audit).
  2. ii′-6-c (the four side bounds): horizontals = mid-segment-integral machine (unchanged, session-038 design) + the DL-5 dog-leg bound; other three sides unchanged (ii′-4 kernel bounds, 5f tight R-bound, M₀, I_I).
  3. ii′-6-d (the fold ⟹ sfBoundProp : SfBoundProp).
  4. ii′-7 (closure): lambda_pos_finite_height_closed at the ORIGINAL N₁ = (3×10¹²−1)² ≈ 9×10²⁴ (3 perimeter hypotheses only); full axiom audit; Paper A correction note (F-A both-signs factor + F-B two-unit count + the F-D dog-leg repair; the N₁ headline is UNCHANGED from the pre-F-D paper); archive closure + errata pointers. Success criterion #3 restored at the original range. Fallbacks if D-074 fails its gates: (a) the c = 1.5 global repair (branch wip/c-1.5-margin-redo, N₁ = 4×10²⁴); (b) c = 2 (N₁ = 2.25×10²⁴); (c) the T = √n hidden-cancellation open question (D-073 §8 D4, research-level).

9. FINDING F-E (session 040, ii′-6-c pre-flight) — the I_I kernel off-by-one

Finding. The I_I (right vertical σ₁ = 2√n, t ∈ [−T, T]) kernel charge e^{√n/2}+1 is NOT provable as charged: the cited lemma 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 (off by one from the rectangle edge re w = 2√n), and DL-4's direct variant needs t² ≥ n (fails near t = 0). At t = 0 the TRUE kernel is (2√n/(2√n−1))ⁿ = e^{√n/2+1/8+O(1/√n)} — genuinely larger than the charged e^{√n/2}. Latent in the ORIGINAL D-036 charge (predates D-074); the same defect class as F-A/F-B (lemma-citation range error; the margin is unaffected — the I_I piece is ~10^{−106} at n = 8×10⁴ and decaying).

Repair (adopted, session 040). Charge I_I honestly as e^{1/3}·IIMaj(n): the uniform-in-t kernel bound ‖kFun n (2√n+it)‖ ≤ e^{√n/2+1/3}+1 (n ≥ 4) via |w/(w−1)| ≤ 1+1/(2√n−1) (normSq monotone in t², worst at t = 0), (1+1/(2√n−1))ⁿ ≤ e^{n/(2√n−1)} (add_one_le_exp), and n/(2√n−1) ≤ √n/2 + 1/3 ⟺ n ≥ 4 (pure algebra). Then I_I ≤ 2T·(e^{√n/2+1/3}+1)·0.57·2^{−(2√n−2)} ≤ e^{1/3}·IIMaj(n). The overrun e^{1/3}·IIMaj vs the charged IIMaj is absorbed by the FREE 2π normalization factor the fold already drops (D-071 §4.5: ‖RectInt'‖ ≤ Σ sides/(2π) ≤ Σ sides): e^{1/3} ≤ 1.4 ≤ 2π — one linarith step in ii′-6-d, factor ~4.5 to spare. NO change to Bn, IIMaj, DogLegRight, the convexity (coefficient stays 1.5 with the exact 1/(2n) bridge), the pinch, or the base points. (The alternative — fattening IIMaj's constant 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; ×(0.8/0.57) pushes the certified product 1.3155 → 1.847 > 4/3 and breaks marginTilde_convex.)

Paper queue (ii′-7). The paper's B(n) statement is UNCHANGED and still valid (the fold's dropped 2π covers the repaired I_I bound exactly); D-036's I_I kernel claim gets the footnote "e^{√n/2+1/3}+1 (uniform in t), absorbed by the 2π normalization slack — Finding F-E".