[{"type":"thinking","thinking":"DL-2 committed (b959a31). Now DL-3: the H_high stepping bound. This is the biggest of the dog-leg pieces. Components:\n\n(i) **Per-step kernel ratio** (D-073 Lemma 4.1's kernel part): for w = σ+iU, σ ≥ 3, U² ≥ (9/4)n:\n‖(1+1/w)ⁿ‖/‖(1+1/(w−1))ⁿ‖ ≤ e^{4/9} — actually the (6.12) chain gives the ratio ≤ (1+1/U²)ⁿ ≤ e^{n/U²} ≤ e^{4/9}. \n\nIn Lean form: ‖(1 + 1/(σ+1+iU))‖ⁿ/‖(1+1/(σ+iU))‖ⁿ ≤ e^{4/9}?? — careful with the shift: the product P(σ) = |1+1/(σ−1+iU)|ⁿ·2^{−(σ−2)} — the ratio P(σ+1)/P(σ): kernel part = |1+1/(σ+iU)|ⁿ/|1+1/(σ−1+iU)|ⁿ ≤ e^{4/9}.\n\nThe (6.12) chain: |1+1/(s+1)|ⁿ/|1+1/s|ⁿ = |1 + (1/(s+1) − 1/s)/(1+1/s)|ⁿ ≤ (1 + 1/|s+1|²)ⁿ... wait the printed chain: |1+1/(s+1)|/|1+1/s| = |(1 + (1/(s+1)−1/s))/(1+1/s)| = |1 + (1/(s+1)−1/s)/(1+1/s)|... let me redo cleanly:\n\n|1+1/(s+1)|ⁿ/|1+1/s|ⁿ = [|1+1/(s+1)|/|1+1/s|]ⁿ and\n|1+1/(s+1)|/|1+1/s| = |(1+1/(s+1))/(1+1/s)| = |1 + (1/(s+1) − 1/s)/(1+1/s)| \n= |1 + (−1/(s(s+1)))·(s/(s+1))| = |1 − 1/(s+1)²| ≤ 1 + 1/|s+1|².\n\nSo the ratio = |1 − 1/(s+1)²|ⁿ ≤ (1+1/|s+1|²)ⁿ ≤ (1+1/U²)ⁿ ≤ e^{n/U²} ≤ e^{4/9} (since |s+1| ≥ U = im, and n/U² ≤ 4/9 when U² ≥ (9/4)n).\n\nIn Lean: with s = σ−1+iU (so s+1 = σ+iU), s+2 = σ+1+iU... let me set it up directly: for w = σ+iU (σ real ≥ 3), w−1 = σ−1+iU:\n\n‖(1+1/w)‖ⁿ/‖(1+1/(w−1))‖ⁿ = (‖1+1/w‖/‖1+1/(w−1)‖)ⁿ and\n(1+1/w)/(1+1/(w−1)) = ((w+1)/w)/((w)/(w−1)) = (w+1)(w−1)/w² = (w²−1)/w² = 1 − 1/w².\nSo the ratio = ‖1 − 1/w²‖ⁿ ≤ (1+1/‖w‖²)ⁿ ≤ (1+1/U²)ⁿ ≤ e^{n/U²} ≤ e^{4/9}.\n\nCLEAN! (1+1/w)/(1+1/(w−1)) = 1 − 1/w² exactly (complex identity: (1+1/w)/(1+1/(w−1)) = ((w+1)/w)·((w−1)/w) = (w²−1)/w² ✓).\n\nIn Lean:\n```\ntheorem kernel_ratio_step {n : ℕ} {σ U : ℝ} (hσ : 3 ≤ σ) (hU : 0 < U) (hnU : (n:ℝ) ≤ (4/9) * U ^ 2) :\n    ‖(1 + 1/((σ:ℝ) + U*I))‖ ^ n / ‖(1 + 1/(((σ:ℝ) - 1) + U*I))‖ ^ n ≤ Real.exp (4/9) := by\n```\nHmm — actually, what's the cleanest form for the DL-3 assembly? Let me think about what the geometric-series bound needs:\n\nThe target: ‖HIntegral (Jlag n) 3 XR U‖ ≤ ∫₃^XR ‖Jlag(σ+iU)‖ dσ ≤ R(1.5)-charged.\n\nD-073 Cor 4.2's structure: ‖Jlag(σ+iU)‖ ≤ ‖(1+1/(w−1))ⁿ‖·‖ζ′/ζ(w)‖ + ‖ζ′/ζ(w)‖ with w = σ+iU:\n- ‖ζ′/ζ(σ+iU)‖ ≤ 2^{−(σ−2)}·dirichletC2 ≤ 2^{−(σ−2)}·1 (dirichletC2 ≤ 1!) — the (6.10) halving in the LSeries form: Λ(m)/m^σ ≤ 2^{−(σ−2)}Λ(m)/m² — wait — dirichletC2 gives the bound at re = 2; at re = σ: ‖ζ′/ζ(σ+iU)‖ ≤ ΣΛ(m)/m^σ ≤ 2^{−(σ−2)}·ΣΛ(m)/m² = 2^{−(σ−2)}·dirichletC2 — the LSeries.norm_term comparison: ‖term Λ (σ:ℂ) m‖ ≤ 2^{−(σ−2)}·‖term Λ (2:ℂ) m‖ — a termwise lemma like the 3-vs-2 one (with rpow: m^σ = m²·m^{σ−2}: Λ/m^σ = (1/m^{σ−2})·(Λ/m²) ≤ 2^{−(σ−2)}·(Λ/m²) since m^{σ−2} ≥ 2^{σ−2} for m ≥ 2, σ ≥ 2 ✓). So ‖ζ′/ζ(σ+iU)‖ ≤ 2^{−(σ−2)}·dirichletC2 ≤ 2^{−(σ−2)} (≤ 1).\n- P(σ) := ‖(1+1/(w−1))ⁿ‖·2^{−(σ−2)} with the ratio P(σ+1)/P(σ) ≤ e^{4/9}/2.\n\nThe geometric series: ∫₃^XR P(σ)dσ ≤ (Σ_{j≥0} q^j)·∫₀¹ P(3+r)dr with q = e^{4/9}/2. P(3+r) = ‖(1+1/(2+r+iU))ⁿ‖·2^{−(1+r)} ≤ (e^{16/9})·2^{−1}·... — the kernel charge at Re(w−1) = 2+r ∈ [2,3]: |1+1/(2+r+iU)| ≤ 1+(3+r)/((2+r)²+U²) ≤ 1+4/(9+U²) (max at r = 1... the (6.11) bound — hmm — the norm_one_add_one_div_le gives ‖1+1/s‖ ≤ 1+(re s+1)/normSq s with s = 2+r+iU: (3+r)/((2+r)²+U²) ≤ 4/(9+U²)? At r = 1: 4/(9+U²) ✓; at r = 0: 3/(4+U²) ≤ 4/(9+U²) ✓ (3·9 = 27 ≤ 16+4U² ⟺ 11 ≤ 4U² ✓ U ≥ 1.66). So ‖(1+1/(2+r+iU))ⁿ‖ ≤ (1+4/(9+U²))ⁿ ≤ e^{4n/(9+U²)} ≤ e^{4n/U²} ≤ e^{16/9} (U² ≥ 9n/4).\n\nThen ∫₀¹ P(3+r)dr ≤ e^{16/9}·∫₀¹2^{−(1+r)}dr = e^{16/9}/(4·log2)·... — hmm wait ∫₀¹ 2^{−(1+r)} dr = (1/2)·(1−1/2)/log2 = 1/(4 log 2). So ∫₃^XR P ≤ e^{16/9}/(4(1−q)log2)·dirichletC2·... — and the +1 part: ∫₃^XR ‖ζ′/ζ‖ dσ ≤ ∫₃^∞ 2^{−(σ−2)}dσ·dirichletC2 = dirichletC2/(2 log 2).\n\nTotal: ‖H_high‖ ≤ dirichletC2·[e^{16/9}/(4(1−q)log 2) + 1/(2 log 2)] with dirichletC2 ≤ 1: R = e^{16/9}/(4(1−q)log 2) + 1/(2 log 2). With q ≤ 0.78: 1−q ≥ 0.22: e^{16/9} ≤ 5.92: 5.92/(4·0.22·0.6932) = 5.92/0.610 = 9.70; +0.7214 = 10.43. So charge R_loose = 10.43 (vs the tight R(1.5) = 5.94 which used Z₀ = 0.57). With dirichletC2 ≤ 1 the charge is 10.43 — margin impact: DogLegRight grows by ~4.5 per side vs the E-034 5.94: ΔBn ≈ +9 at every n — negligible ✓ fold indifferent ✓.\n\nHmm — should I try to charge the tighter Z₀ ≤ 0.5703661 (E-033's certified value)? That needs dirichletC2 ≤ 0.5703661 in Lean — the SAME infeasibility as dirichletC2 ≤ 0.57 (partial-sum tail too lossy; dirichletC2_le_one is what's in hand). So charge dirichletC2 ≤ 1, R = 10.43. Actually — wait, can I do better cheaply? dirichletC3 ≤ 1/2 exists! Use the m ≥ 4 split for the zeta factor: ‖ζ′/ζ(σ+iU)‖ ≤ 2^{−(σ−3)}·‖ζ′/ζ(3+iU)‖ ≤ 2^{−(σ−3)}·(1/2) — the (6.10) halving from 3: Λ/m^σ ≤ 2^{−(σ−3)}Λ/m³ for σ ≥ 3 ✓. Then the geometric series starts at σ = 3 with the zeta factor ≤ 1/2 instead of dirichletC2 ≤ 1: P(σ) = ‖(1+1/(w−1))ⁿ‖·2^{−(σ−3)}·(1/2)... hmm wait — cleaner: ‖ζ′/ζ(σ+iU)‖ ≤ 2^{−(σ−3)}·dirichletC3 ≤ 2^{−(σ−3)}/2. The per-step ratio: kernel e^{4/9} × zeta 1/2 — same q = e^{4/9}/2. P(3+r) ≤ e^{16/9}·2^{−r}·(1/2): ∫₀¹ ≤ e^{16/9}·(1/2)·∫₀¹2^{−r}dr = e^{16/9}·(1/2)·(1/(2 log 2)) = e^{16/9}/(4 log 2). Total: (1/2)·[e^{16/9}/(4(1−q)log 2) + 1/(2 log 2)]·... — the +1 part: ∫₃^∞ 2^{−(σ−3)}/2 dσ = (1/2)·(1/log 2). So R = (1/2)·e^{16/9}/(4(1−q)log2) + 1/(2 log 2) = 9.70/2+0.7214·... wait: (1/2)·9.70 = 4.85 + 0.7214 = 5.57?? Hmm let me redo: R = e^{16/9}/(4(1−q)log2)·(1/2) + 1/(2 log 2)·... no — let me redo carefully:\n\n‖Jlag‖ ≤ ‖(1+1/(w−1))ⁿ‖·‖ζ′/ζ‖ + ‖ζ′/ζ‖ — with ‖ζ′/ζ(σ+iU)‖ ≤ 2^{−(σ−3)}/2 (dirichletC3 ≤ 1/2 form):\nP(σ) := ‖(1+1/(w−1))ⁿ‖·2^{−(σ−3)}/2, ratio ≤ e^{4/9}·(1/2) = q.\n∫₃^XR P ≤ (1/(1−q))·∫₀¹P(3+r)dr ≤ (1/(1−q))·e^{16/9}·(1/2)·∫₀¹2^{−r}dr = (1/(1−q))·e^{16/9}·(1/2)·(1/(2 log 2)) = e^{16/9}/(4(1−q)log 2)·... hmm: (1/2)·(1/(2 log 2)) = 1/(4 log 2): so ∫ P ≤ e^{16/9}/(4(1−q)log 2) — SAME as before?! Because the zeta-at-3 factor 1/2 is inside P(3+r)... wait no: P(3+r) = ‖kernel‖·2^{−(3+r−3)}/2 = ‖kernel‖·2^{−r}/2. ∫₀¹ P(3+r)dr = e^{16/9}·(1/2)∫₀¹2^{−r}dr = e^{16/9}·(1/2)·(1/(2 log2)) = e^{16/9}/(4 log 2). Hmm and before (the dirichletC2 version) I had P(σ) = ‖kernel‖·2^{−(σ−2)}·dirichletC2: ∫₀¹P(3+r) = e^{16/9}·dirichletC2·∫₀¹2^{−(1+r)} = e^{16/9}·dirichletC2·(1/(4 log 2)). So the C3 version: e^{16/9}/(4 log 2) vs C2 version: e^{16/9}·dirichletC2/(4 log 2) — with dirichletC2 ≤ 1 the C3 version gains a factor 2 (the 2^{−(σ−3)}/2 vs 2^{−(σ−2)}·1: at σ = 3: 1/2 vs 1/2·... 2^{−1} = 1/2 — same!). Hmm: 2^{−(σ−2)}·dirichletC2 at σ = 3 is 2^{−1}·1 = 1/2 ✓ same as 2^{0}/2 = 1/2 ✓. And the ratio: C2 version has the zeta halving 1/2 per step (σ → σ+1: 2^{−(σ−1−2)}/2^{−(σ−2)} = 1/2) ✓ same as C3's (2^{−(σ+1−3)}/2)/(2^{−(σ−3)}/2) = 1/2 ✓. IDENTICAL — because dirichletC2 ≤ 1 and dirichletC3 ≤ 1/2 = dirichletC2/2 (the comparison!) — the C3 bound at σ is exactly the C2 bound × 2^{−(σ−3)}·... — they're consistent (dirichletC3 ≤ dirichletC2/2 ✓ the termwise comparison). So R_loose = e^{16/9}/(4(1−q)log2)·dirichletC2 + dirichletC2/(2 log 2) — no gain from C3. Fine: R = dirichletC2·[e^{16/9}/(4(1−q)log2) + 1/(2 log 2)] ≤ [same]·1.\n\nCharge R_DL := e^{16/9}/(4·(1−0.78)·log 2) + 1/(2·log 2) with certified numbers: e^{16/9} ≤ 5.92 (certified: e²/e^{2/9}: 7.3891/1.2489 = 5.9167 ≤ 5.92 ✓), 1−q ≥ 1−0.78 = 0.22, log 2 ≥ 0.6931 (d9). R_DL := 5.92/(4·0.22·0.6931) + 1/(2·0.6931) = 5.92/0.610 + 0.7214 = 9.705+0.7214 = 10.426 → charge 10.43.\n\nHmm — or with q certified ≤ 0.78 from e^{4/9} ≤ 1.56: e^{4/9} ≤ 1.56 ✓ q ≤ 0.78 ✓.\n\nNow the Lean structure for DL-3:\n\n(a) **Kernel ratio step** (the exact 1 − 1/w² identity):\n```\ntheorem one_add_one_div_ratio {w : ℂ} (hw : w ≠ 0) (hw1 : w - 1 ≠ 0) :\n    (1 + 1 / w) / (1 + 1 / (w - 1)) = 1 - 1 / w ^ 2 := by\n  field_simp [hw, hw1]\n  ring\n```\nCheck: (1+1/w)/(1+1/(w−1)) = ((w+1)/w)·((w−1)/w) = (w²−1)/w² = 1−1/w² ✓.\n\nThen the ratio bound: ‖(1+1/w)‖ⁿ ≤ ‖1−1/w²‖ⁿ·‖(1+1/(w−1))‖ⁿ with ‖1−1/w²‖ ≤ 1+1/‖w‖² ≤ 1+1/U²:\n```\ntheorem kernel_step_ratio_le {n : ℕ} {σ U : ℝ} (hU : 0 < U) (hnU : 4 * (n:ℝ) ≤ 9 * U ^ 2) :\n    ‖(1 + 1/((σ:ℝ) + U*I))‖ ^ n ≤ Real.exp (4/9) * ‖(1 + 1/(((σ:ℝ) - 1) + U*I))‖ ^ n := by\n  -- (1+1/w)/(1+1/(w−1)) = 1−1/w²; ‖1−1/w²‖ ≤ 1+1/U² ≤ e^{1/U²}; (e^{1/U²})ⁿ = e^{n/U²} ≤ e^{4/9}\n```\nHmm — the form: better to state as the product form used by the geometric argument:\n‖(1+1/w)ⁿ‖·2^{−(σ+1−2)} ≤ q·(‖(1+1/(w−1))ⁿ‖·2^{−(σ−2)}) — the P-ratio. Actually for the geometric-series integral, the cleanest decomposition:\n\n‖Jlag n (σ+iU)‖ ≤ ‖(1+1/((σ−1)+iU))ⁿ‖·‖ζ′/ζ(σ+iU)‖ + ‖ζ′/ζ(σ+iU)‖\nwith ‖ζ′/ζ(σ+iU)‖ ≤ 2^{−(σ−2)}·dirichletC2 ≤ 2^{−(σ−2)}.\n\nDefine P(σ) := ‖(1+1/((σ−1)+iU))ⁿ‖·2^{−(σ−2)} — the per-step: P(σ+1) ≤ q·P(σ) with q = e^{4/9}/2:\nP(σ+1)/P(σ) = [‖(1+1/(σ+iU))ⁿ‖/‖(1+1/((σ−1)+iU))ⁿ‖]·(1/2) ≤ e^{4/9}/2 ✓ by the kernel ratio.\n\nThe integral bound ∫₃^XR ‖Jlag‖ dσ ≤ ∫₃^XR P(σ)dσ·dirichletC2 + ∫₃^XR 2^{−(σ−2)}dσ·dirichletC2.\n\nFor the geometric series over unit intervals: P(σ) ≤ P(3+r)·q^j for σ = 3+j+r: the Lean form: for j : ℕ, r ∈ [0,1]: P(3+j+r) ≤ q^j·P(3+r) — by induction on j using the step lemma.\n\nThe integral ∫₃^XR P(σ)dσ ≤ Σ_{j=0}^{⌈XR−3⌉} ∫₀¹P(3+j+r)dr ≤ (Σ_j q^j)·max-interval — via interval-integral decomposition: ∫₃^XR = Σ_{j=0}^{N−1}∫_{3+j}^{4+j} + ∫_{3+N}^{XR}. For each unit interval: ∫_{3+j}^{4+j} P ≤ q^j·∫₀¹P(3+r)dr — via the per-point bound P(3+j+r) ≤ q^j P(3+r) and the interval norm bound.\n\nThen Σ_j q^j ≤ 1/(1−q) (geometric tsum: Summable geometric: tsum_geometric_of_lt_1 : ∑' q^j = 1/(1−q) for |q| < 1 ✓ Mathlib).\n\n∫₀¹P(3+r)dr ≤ e^{16/9}·∫₀¹2^{−(1+r)}dr·... — P(3+r) = ‖(1+1/(2+r+iU))ⁿ‖·2^{−(1+r)}: the kernel charge e^{16/9} (needs its own lemma — clone the e⁴+1 kernel lemma's structure at U² ≥ 9n/4: ‖1+1/(2+r+iU)‖ ≤ 1+(3+r)/((2+r)²+U²) ≤ 1+4/(9+U²) ⟹ ⁿ ≤ e^{4n/(9+U²)} ≤ e^{16/9}).\n\n∫₀¹2^{−(1+r)}dr = 1/(4 log 2) — the integral of 2^{−(1+r)}: ∫2^{−(1+r)}dr = −2^{−(1+r)}/log2: evaluated 0→1: (2^{−1}−2^{−2})/log2 = (1/2−1/4)/log2 = 1/(4 log 2). In Lean: the interval integral of a·b^r — via Real.rpow or the 2^r form: 2^{−(1+r)} = (1/2)·(1/2)^r = (1/2)·exp(−r log 2): ∫₀¹ = (1/2)·(1−e^{−log 2})/log 2 = (1/2)·(1/2)/log 2 = 1/(4 log 2) ✓ — the Lean integral: ∫ r in 0..1, (1/2)·Real.exp(−r·log2) — via integral_exp or the FTC (Real.integral_exp?). There are Mathlib lemmas for ∫ exp(cx) — `integral_exp_mul_complex` or for real: use the FTC directly: HasDerivAt (fun r => −exp(−r log 2)/log 2)... — or the LiBasePoints/session-012 patterns for integrals of exponentials. Let me check what's available: `Real.integral_exp` — probably not a direct name; but there's `integral_exp` in Mathlib for complex? For real: the FTC route: ∫₀¹ e^{−r log 2} dr = [−e^{−r log 2}/log 2]₀¹ = (1−e^{−log 2})/log 2 = (1−1/2)/log 2 = 1/(2 log 2). Multiply by 1/2: 1/(4 log 2) ✓.\n\nThe pieces are each small but the assembly is substantial (~300–400 lines). Break DL-3 into sub-chunks:\n- DL-3-i: the zeta 2^{−(σ−2)} bound (termwise LSeries comparison, ~40 lines) + the kernel ratio identity/step (~60 lines) + q certified ≤ 0.78 (~20 lines, e^{4/9} < 2 via e^{4/9} = e/e^{5/9}: e ≤ 2.7183, e^{5/9} ≥ partial sums ≥ 1.7430 ⟹ e^{4/9} ≤ 1.5596 ≤ 1.56 — the partial-sum lower bound on e^{5/9}: Σ₀⁷(0.5556^i/i!) ≥ 1.7430 — norm_num-able ✓) + e^{16/9} certified ≤ 5.92 (e²/e^{2/9}: e² ≤ 7.3891, e^{2/9} ≥ 1.2489 ⟹ ≤ 5.9167 ≤ 5.92 ✓).\n- DL-3-ii: the initial kernel charge e^{16/9} on [3,4] (~50 lines cloning the e⁴ lemma) + the P-step + the unit-interval geometric chain + the geometric tsum + the ∫₀¹ pieces + the final assembly (~250 lines).\n\nThis is a big sub-stage. Let me get going — first the zeta bound + kernel identity + certified constants (the quick wins), then the assembly.\n\nActually — wait. Let me reconsider the assembly strategy to minimize Lean pain. The geometric-series-over-unit-intervals is the fiddly part (induction + interval decomposition + tsum). ALTERNATIVE cleaner route: bound P(σ) by a SINGLE EXPONENTIAL ENVELOPE: P(σ) ≤ P(3)·q^{σ−3−1}·... — no: P(σ) ≤ e^{16/9}·2^{−(σ−2)}·... — hmm — actually here's a much simpler envelope: \n\n‖(1+1/(w−1))ⁿ‖ for σ ≥ 3: by the kernel RATIO applied repeatedly — but the DIRECT bound: ‖1+1/(w−1)‖ ≤ 1+(σ)/((σ−1)²+U²) (norm_one_add_one_div_le with re(w−1) = σ−1: ((σ−1)+1)/((σ−1)²+U²) = σ/((σ−1)²+U²)) — at σ ≥ 3, U² ≥ 9n/4: σ/((σ−1)²+U²) ≤ σ/(σ²/... hmm — simpler: ‖(1+1/(w−1))ⁿ‖ ≤ (1+σ/((σ−1)²+U²))ⁿ ≤ exp(nσ/((σ−1)²+U²)) ≤ exp(nσ/U²) (since (σ−1)²+U² ≥ U²) — for σ ≥ 3 ≤ exp(nσ/U²) — and nσ/U² ≤ 4σ/9: so ‖kernel‖ ≤ e^{4σ/9}. And the product: P(σ) ≤ e^{4σ/9}·2^{−(σ−2)} = e^{4σ/9−(σ−2)log2} = e^{4σ/9}·e^{−(σ−2)log2} = e^{2log2}·e^{−σ(log2−4/9)} = 4·e^{−cσ} with c = log2 − 4/9 = 0.6931−0.4444 = 0.2487 > 0!! Then ∫₃^XR P(σ)dσ ≤ 4·∫₃^∞ e^{−cσ}dσ = 4·e^{−3c}/c = 4·e^{−0.7461}/0.2487 = 4·0.4743/0.2487 = 7.63. \n\nMUCH SIMPLER — a single exponential envelope, no geometric series, no induction! Let me double-check the kernel bound: ‖1+1/(w−1)‖ ≤ 1+(σ)/((σ−1)²+U²) — norm_one_add_one_div_le : ‖1+1/s‖ ≤ 1+(re s+1)/normSq s with s = w−1 = (σ−1)+iU: re s +1 = σ, normSq = (σ−1)²+U² ✓. Then ≤ 1+σ/U² (dropping (σ−1)² ≥ 0) — then ⁿ ≤ exp(nσ/U²) ≤ exp(4σ/9) (n ≤ 4U²/9). And the zeta: 2^{−(σ−2)}. Product (before dirichletC2): e^{4σ/9}·2^{−(σ−2)}.\n\nHmm wait — but there's a subtlety: ‖(1+1/(w−1))ⁿ‖ = ‖1+1/(w−1)‖ⁿ — the exponent: (1+x)ⁿ ≤ e^{nx} with x = σ/((σ−1)²+U²) ≤ σ/U²: so ≤ e^{nσ/U²} ≤ e^{(4/9)σ} ✓.\n\nP(σ) := ‖(1+1/(w−1))ⁿ‖·2^{−(σ−2)} ≤ e^{(4/9)σ}·2^{−(σ−2)} = 4·e^{(4/9−log2)σ}·... : e^{(4/9)σ}·e^{−(σ−2)log2} = e^{2log2}·e^{(4/9−log2)σ} = 4·e^{−cσ}, c := log2 − 4/9.\n\n∫₃^XR P ≤ 4∫₃^XR e^{−cσ}dσ ≤ 4∫₃^∞ e^{−cσ}dσ = 4·e^{−3c}/c.\ne^{−3c} = e^{−3log2+4/3} = 2^{−3}·e^{4/3} = e^{4/3}/8: 4·e^{4/3}/(8c) = e^{4/3}/(2c).\nSo ∫₃^XR P ≤ e^{4/3}/(2c) — with dirichletC2 ≤ 1 for the product... — wait, the ‖Jlag‖ bound: ‖Jlag‖ ≤ ‖(1+1/(w−1))ⁿ‖·‖ζ′/ζ‖ + ‖ζ′/ζ‖ ≤ P(σ)·dirichletC2 + 2^{−(σ−2)}·dirichletC2. Hmm — careful: ‖Jlag‖ = ‖kFun‖·‖ζ′/ζ‖ with kFun = (1+1/(w−1))ⁿ − 1: ‖kFun‖ ≤ ‖(1+1/(w−1))ⁿ‖+1: so ‖Jlag‖ ≤ (‖(1+1/(w−1))ⁿ‖+1)·‖ζ′/ζ‖ = P(σ)·dirichletC2-ish + ‖ζ′/ζ‖. With ‖ζ′/ζ‖ ≤ 2^{−(σ−2)}·dirichletC2:\n‖Jlag(σ+iU)‖ ≤ (e^{(4/9)σ}·2^{−(σ−2)} + 2^{−(σ−2)})·dirichletC2 = (4e^{−cσ} + 4·2^{−σ})·dirichletC2.\n∫₃^XR ‖Jlag‖ ≤ dirichletC2·[e^{4/3}/(2c) + 4·∫₃^∞2^{−σ}dσ] = dirichletC2·[e^{4/3}/(2c) + 4·2^{−3}/log2] = dirichletC2·[e^{4/3}/(2c) + 1/(2 log 2)].\nWith e^{4/3} ≤ 3.794 (e·e^{1/3}: 2.7183·1.3957 = 3.7937 ≤ 3.794 certified), c ≥ 0.2487 (log2 ≥ 0.6931: c = log2−4/9 ≥ 0.6931−0.4445 = 0.2486 — certified: log2 ≥ 0.6931471803 (d9), 4/9 ≤ 0.44445: c ≥ 0.24870 — careful rounding: 0.6931471−0.4444445 = 0.2487026 ≥ 0.2487):\ne^{4/3}/(2·0.2487) = 3.7937/0.4974 = 7.6271; 1/(2·0.6931) = 0.7213. R = 7.6271+0.7213 = 8.3484 → charge R_DL = 8.35 (with dirichletC2 ≤ 1).\n\nvs the geometric-series 10.43 — BETTER (the exponential envelope is tighter AND simpler). vs tight R(1.5) = 5.94 — looser but fold-indifferent (Δ ~ +2.4 per side vs 5.94, ΔBn ~ +5 everywhere — negligible).\n\nCertified constants for the envelope route:\n- c := Real.log 2 − 4/9; c ≥ 0.2487 (log_two_gt_d9).\n- e^{4/3} ≤ 3.7937: e^{4/3} = e·e^{1/3}: e ≤ 2.7182818286 (d9), e^{1/3} ≤ 1.3957: e^{1/3} ≤ Σ-upper via (1−(1/3)/16)⁻¹⁶ = (1−1/48)⁻¹⁶ = (47/48)⁻¹⁶ = (48/47)¹⁶ = 1.39565... — compute: (48/47)^16 = (1.0212766)^16 = e^{16·0.021053} = e^{0.33685} = 1.40061?? hmm that's looser. True e^{1/3} = 1.39561. The (1−x/16)⁻¹⁶ trick at x = 1/3: (1−1/48)⁻¹⁶ = (48/47)¹⁶: ln = 16·ln(48/47) = 16·0.0210533 = 0.336853; e^{0.336853} = 1.40057. So e^{1/3} ≤ 1.4006 via the trick (0.4% fat). e^{4/3} ≤ 2.7182818286·1.4006 = 3.80724 → ≤ 3.8073. Then e^{4/3}/(2·0.2487) = 3.8073/0.4974 = 7.6544; +0.7214 = 8.3758 → charge 8.38. Hmm slightly fatter than the true-arithmetic 8.35 — whatever, charge 8.38 or tighten the e^{1/3} bound via partial sums (e^{1/3} = 1/e^{-1/3}... the trick overshoots; better: e^{1/3} ≤ (partial sum upper?) — for UPPER bounds on e^x with x > 0 the (1−x/16)⁻¹⁶ is the tool; at x = 1/3 it's 0.4% fat — acceptable).\n  Alternative cleaner: e^{4/3} = e/e^{2/3}·... no. Or e^{4/3} ≤ (e^{1/3})⁴... same. Take 3.8073.\n- log 2 ≥ 0.6931471803 (Real.log_two_gt_d9), log 2 ≤ 0.6931471806 (lt_d9) — c ∈ [0.2487026, 0.2487028]: charge c ≥ 0.2487.\n- 1/(2 log 2) ≤ 0.7214 (log2 ≥ 0.6931).\n\nSo R_DL := 3.8073/(2·0.2487) + 0.7214 = 7.6544+0.7214 = 8.3758 → charge **8.38**.\n\nThe Lean structure for DL-3 (envelope route — much simpler):\n(a) zeta halving bound: ‖logDeriv ζ (σ+iU)‖ ≤ 2^{−(σ−2)}·dirichletC2 for σ ≥ 2 (termwise LSeries comparison: Λ(m)/m^σ ≤ 2^{−(σ−2)}·Λ(m)/m² — needs the rpow comparison m^{σ−2} ≥ 2^{σ−2} for m ≥ 2, σ ≥ 2: Real.rpow_le_rpow (base ≥ 1) ✓). ~50 lines cloning the 3-vs-2 comparison.\n(b) kernel envelope: ‖(1+1/((σ−1)+iU))ⁿ‖ ≤ e^{(4/9)σ} for σ ≥ 3, U² ≥ (9/4)n: via norm_one_add_one_div_le + the exp chain (~60 lines cloning the e⁴ lemma).\n(c) the product envelope: ‖Jlag n (σ+iU)‖ ≤ (4·e^{−cσ} + 4·2^{−σ})·dirichletC2 (~30 lines).\n(d) the integrals: ∫₃^XR 4e^{−cσ}dσ ≤ 4·e^{−3c}/c = e^{4/3}/(2c) (FTC for e^{−cσ}: HasDerivAt (fun σ => −e^{−cσ}/c) = e^{−cσ} ✓ + interval FTC + e^{−3c} = e^{4/3}/8 ✓) + ∫₃^XR 4·2^{−σ}dσ ≤ 1/(2 log2) (2^{−σ} = e^{−σ log2}, same FTC) (~120 lines).\n(e) certified constants: c ≥ 0.2487, e^{4/3} ≤ 3.8073, log2 bounds, R_DL = 8.38 assembly (~40 lines).\n(f) capstone: ‖HIntegral (Jlag n) 3 XR U‖ ≤ 8.38 for 3 ≤ XR, U² ≥ (9/4)n, U > 0 (~40 lines).\n\nTotal ~350 lines but each piece is mechanical. The interval-integral side: ‖HIntegral f 3 XR U‖ ≤ ∫₃^XR ‖f‖ — via intervalIntegral.norm_integral_le_of_norm_le (the version at Basic.lean:755: norm_integral_le_of_norm_le (hab : a ≤ b) (h : ∀ᵐ t, t ∈ Ioc a b → ‖f t‖ ≤ g t) (hbound : IntervalIntegrable g μ a b) : ‖∫ f‖ ≤ ∫ g ✓ — the g here is the explicit envelope (integrable: exp/2^{−σ} ✓).\n\nWait — one more check on (b): the kernel envelope at σ ≥ 3 vs the D-073 charge e^{16/9} on [3,4]: the envelope e^{(4/9)σ} at σ = 3 gives e^{4/3} = 3.7937 vs the tight kernel charge e^{16/9} = 5.92 — the envelope is SMALLER?! That can't be right — ‖kernel(3)‖ ≤ e^{16/9} was the (6.11) charge at [3,4]... — the envelope e^{(4/9)·3} = e^{4/3} = 3.79 < 5.92 — CONTRADICTION?? Let me recheck: the kernel charge at σ ∈ [3,4]: ‖(1+1/(w−1))ⁿ‖ ≤ (1+4/(9+U²))ⁿ ≤ e^{4n/(9+U²)} ≤ e^{4n/U²} ≤ e^{16/9} (U² ≥ 9n/4 ⟹ 4n/U² ≤ 16/9). The envelope at σ = 3: ‖(1+1/(w−1))ⁿ‖ ≤ e^{nσ/U²} = e^{3n/U²} ≤ e^{3·4/9} = e^{4/3} ✓ — and e^{4/3} = 3.79 < 5.92 = e^{16/9} ✓ CONSISTENT (the (6.11) charge e^{4n/U²} used the coarse (σ+1)/(σ²+U²) ≤ 4/U² at σ = 3 giving exponent 4n/U² = 16/9; the tighter norm_one_add bound gives σ/U² per unit σ — at σ = 3: 3n/U² = 4/3 < 16/9 ✓ the envelope is tighter near 3 and grows as e^{(4/9)σ} while the (6.11) charge is a constant — the envelope wins for small σ and loses for large σ, but the 2^{−(σ−2)} decay dominates the product anyway ✓).\n\nHmm — wait, but is the envelope valid for ALL σ ≥ 3? ‖1+1/(w−1)‖ ≤ 1+σ/((σ−1)²+U²) ≤ 1+σ/U² ✓ any σ ✓. And (1+σ/U²)ⁿ ≤ e^{nσ/U²} ≤ e^{(4/9)σ} ✓ (n ≤ 4U²/9). ✓ Valid everywhere.\n\nAlso the exponent comparison: (4/9)σ − (σ−2)log2 = 2log2 − σ(log2−4/9) = 2log2 − cσ ✓ c = log2−4/9 > 0 ✓.\n\nNow (d): ∫₃^XR 4e^{−cσ}dσ = 4·[−e^{−cσ}/c]₃^XR = 4(e^{−3c}−e^{−c·XR})/c ≤ 4e^{−3c}/c ✓. In Lean via intervalIntegral FTC: `intervalIntegral.integral_eq_sub_of_hasDerivAt` or `Real.integral_exp...`. The function e^{−cσ} = Real.exp(−c·σ): its antiderivative: −exp(−cσ)/c with HasDerivAt: deriv(−exp(−cσ)/c) = exp(−cσ) ✓ (chain rule: d/dσ[−exp(−cσ)/c] = −exp(−cσ)·(−c)/c = exp(−cσ) ✓). FTC: ∫₃^XR exp(−cσ) = −exp(−c·XR)/c + exp(−3c)/c ≤ exp(−3c)/c (dropping the negative term ✓ nonneg).\ne^{−3c} = e^{−3(log2−4/9)} = e^{−3log2+4/3} = e^{4/3}·e^{−3log2} = e^{4/3}·2^{−3} = e^{4/3}/8 ✓ (Real.exp_nat_mul/ln: −3·log2 = log(2^{−3})... via Real.exp_log (2^3 > 0): e^{log(1/8)} = 1/8: e^{−3 log 2} = e^{log(2^{-3})} = 1/8: −3log2 = log((2³)⁻¹) = log(1/8) ✓).\nSo ∫ ≤ e^{4/3}/(8c)·4 = e^{4/3}/(2c) ✓.\n\n∫₃^XR 4·2^{−σ}dσ: 2^{−σ} = e^{−σ log2} ✓ (Real.rpow? 2^{−σ} as ℝ: (2:ℝ)^{(-σ)} via rpow_def_of_pos: 2^x = e^{x log2} ✓). ∫ ≤ ∫₃^∞ 4e^{−σ log2} = 4·e^{−3log2}/log2 = 4/(8·log2) = 1/(2 log2) ✓ same FTC.\n\nAlright — DL-3 plan is solid. It's a chunky but mechanical build. Let me write it. Given the size, I'll append the DL-3 block to LiDogLeg.lean in two chunks: (a)+(b) first (the pointwise bounds), compile; then (c)+(d)+(e)+(f) (integral assembly + capstone), compile.","signature":""},{"type":"text","text":"DL-2 committed (`b959a31`). Now **DL-3** — and I've found a much simpler route than the geometric-series assembly: a **single exponential envelope** P(σ) ≤ 4·e^{−cσ} with c = log 2 − 4/9 > 0, giving R = e^{4/3}/(2c) + 1/(2 log 2) ≈ 8.38 directly (no induction, no interval decomposition, no geometric tsum). Writing the pointwise bounds first (zeta halving + kernel envelope)."},{"type":"tool_use","id":"TodoWrite_239","name":"TodoWrite","input":{"todos":[{"content":"DL-3a: zeta halving bound ‖ζ′/ζ(σ+iU)‖ ≤ 2^{−(σ−2)}·dirichletC2 (termwise LSeries comparison)","status":"in_progress","activeForm":"Proving the zeta halving bound"},{"content":"DL-3b: kernel envelope ‖(1+1/((σ−1)+iU))ⁿ‖ ≤ e^{(4/9)σ} for σ ≥ 3, U² ≥ (9/4)n","status":"pending","activeForm":"Proving the kernel envelope"},{"content":"DL-3c: product envelope ‖Jlag‖ ≤ (4e^{−cσ} + 4·2^{−σ})·dirichletC2 + certified constants (c ≥ 0.2487, e^{4/3} ≤ 3.8073)","status":"pending","activeForm":"Building the product envelope"},{"content":"DL-3d: integrals (FTC for e^{−cσ} and 2^{−σ}) + capstone ‖HIntegral (Jlag n) 3 XR U‖ ≤ 8.38 + build + audit + commit","status":"pending","activeForm":"Assembling the H_high capstone"}]},"extra_content":null}]