[{"type":"thinking","thinking":"Not malware. I now have everything:\n\n**RectangleIntegral f z w = HIntegral f z.re w.re z.im − HIntegral f z.re w.re w.im + VIntegral f w.re z.im w.im − VIntegral f z.re z.im w.im**\n\nWith z = rectZ T (re = −5/2, im = −T), w = rectW n T (re = 2√n, im = T):\n- Bottom: HIntegral (Jlag n) (−5/2) (2√n) (−T)\n- Top: − HIntegral (Jlag n) (−5/2) (2√n) T\n- Right: + VIntegral (Jlag n) (2√n) (−T) T\n- Left: − VIntegral (Jlag n) (−5/2) (−T) T\n\nThe horizontals split: HIntegral (−5/2) (2√n) (±T) = HIntegral (−5/2) 3 (±T) + HIntegral 3 (2√n) (±T) via intervalIntegral.integral_add_adjacent_intervals (HIntegral_add or whatever). The right tails [3, 2√n] are bounded by dogLegUpper_two_sides. The mid parts [−5/2, 3] need the segment machine.\n\n**ii′-6-c sub-stage plan** (new file LiSidesBounds.lean? or extend LiAssembly). I'll create a new file `LiSideBounds.lean`:\n\n**6-c-i: rectangle decomposition + I_III + I_I**\n1. `rectangleIntegral_Jlag_eq`: RectangleIntegral (Jlag n) (rectZ T) (rectW n T) = [bottom − top + right − left] with the rewrites (rectZ_re etc. — just unfold + rfl? RectangleIntegral is a def with z.re etc; rectZ T).re reduces by rectZ_re — need rw [RectangleIntegral, rectZ_re, rectZ_im, rectW_re, rectW_im]. It's an abbrev + simp-proved rewrites ✓).\n2. Split horizontals: HIntegral f a c y = HIntegral f a b y + HIntegral f b c y — this is `intervalIntegral.integral_add_adjacent_intervals` needs IntervalIntegrable. Jlag is continuous on the segment (differentiable away from 1 and zeros; on the horizontal line im = ±T, T zero-avoiding ⟹ no zeros; s ≠ 1 since im ≠ 0). Need IntervalIntegrable (Jlag n ∘ (+iT)) on [−5/2, 2√n]. Jlag_differentiableAt_dogleg (LiDogLeg:47) — what are its conditions? Probably s ≠ 1 + ζ s ≠ 0. ContinuousOn → IntervalIntegrable (`ContinuousOn.intervalIntegrable`). \n3. **I_III**: `vIntegral_Jlag_left_norm_le` : ‖VIntegral (Jlag n) (−5/2) (−T) T‖ ≤ 4T·((2/3)·Z2hat T + 10.5·log(T+2) + 48) + 40·1.3352, for T ≥ 10 (T ≥ √n ≥ √(10⁵) ≥ 316 ✓ so this is where n ≥ 10⁵ enters — actually n ≥ 10⁵ gives √n ≥ 316.23). \n   - VIntegral f x y1 y2 = I • ∫_{y1}^{y2} f(x + iy) dy. ‖I • v‖ = ‖v‖ (Complex.norm_I = 1, norm_smul). \n   - ∫_{−T}^{T} Jlag n (−5/2 + it) dt. Bound: ‖Jlag n s‖ = ‖kFun n s‖·‖logDeriv ζ s‖ (Jlag def: kFun * (−(deriv/ζ)); −logDeriv: norm_neg ✓; note Jlag uses deriv ζ s / ζ s and logDeriv = deriv/ζ — need logDeriv riemannZeta s = deriv ζ s / ζ s — logDeriv_def ✓ rfl probably).\n   - kFun ≤ 2 (kFun_norm_le_two, re = −5/2).\n   - Split the integral: [−T, −10], [−10, 10], [10, T]. \n     - Middle: MZeroProp: ‖logDeriv ζ (−5/2 + it)‖ ≤ 1.3352 for |t| ≤ 10 ✓ (MZeroProp is stated exactly at −5/2 + t·I ✓).\n     - Tails: for t ∈ [10, T]: tight capstone at s = −5/2 + it, him : s.im = t ✓, hζ: ζ s ≠ 0 — need zero-freeness on the left vertical: re = −5/2... ζ(−5/2 + it) ≠ 0? Hmm! The left vertical passes through re = −5/2. Nontrivial zeros have re ∈ (0,1) ✓ not −5/2. Trivial zeros at −2, −4, ... — −2 is not −5/2 ✓. But could ζ vanish at −5/2 + it for some t? zeta_zero_classification: every zero is nontrivial ∪ {0} ∪ {−2n}. re = −5/2 excludes all: nontrivial re ∈ (0,1); 0; −2n even integers. So ζ ≠ 0 on the whole line re = −5/2 ✓.\n     - The capstone gives ‖logDeriv − nearsum‖ ≤ 10.5 log(t+2) + 48. And ‖nearsum‖ = ‖Σ mult/(s−ρ)‖ ≤ Σ mult/‖s−ρ‖ ≤ (2/3)·Σ mult (‖s−ρ‖ ≥ |re s − re ρ| = 5/2 + re ρ ≥ 5/2 > 3/2... wait ‖s−ρ‖ ≥ |re(s−ρ)| = |−5/2 − β| = 5/2 + β ≥ 5/2 (β > 0). So 1/‖s−ρ‖ ≤ 2/5 ≤ 2/3 ✓ actually even better. D-071 used 3/2 (re ρ ≤ 1: |−5/2 − β| ≥ 5/2 − ... no: β ∈ (0,1): −5/2 − β ∈ (−7/2, −5/2), |·| ∈ (5/2, 7/2) ≥ 5/2 ⟹ ≤ 2/5. Either way ≤ 2/3 ✓.\n     - Σ_{nearZerosSub t} mult ≤ Z2hat t: bridge nearZerosSub t ⊆ zeroAbsWindow t (|γ−t| < 1 ⟹ ≤ 1 ✓) + ZeroCountProp2 (t ≥ 10 ✓) + monotone: Z2hat t ≤ Z2hat T for t ≤ T — Z2hat monotone (log, loglog increasing). Need a Z2hat_mono lemma (probably exists from marginTilde_convex machinery? there's C0hat_mono ✓; Z2hat has same shape — check).\n     - For t ∈ [−T, −10]: the conj trick or direct: the capstone is stated for t ≥ 10 (ht : 10 ≤ t, him : s.im = t). For negative t: apply capstone at conj s with im = −t ≥ 10: ‖logDeriv ζ(conj s) − Σ_{nearZerosSub (−t)} mult/(conj s − ρ)‖. And logDeriv ζ (conj s) = conj (logDeriv ζ s) (logDeriv_riemannZeta_conj? — exists? LiTightR has zeroMult_conj via analyticOrderAt_riemannZeta_conj via iteratedDeriv_riemannZeta_conj. Is there a logDeriv conj? deriv_riemannZeta_conj? iteratedDeriv at 1 = deriv ✓ `iteratedDeriv_riemannZeta_conj 1` was used in DL-1's Jlag_conj — Jlag_conj already proves the whole integrand is conj-symmetric! So for the negative tail, instead of the capstone at −t, use: ‖Jlag n (conj s)‖ = ‖Jlag n s‖ via Jlag_conj + norm_conj. So ∫_{−T}^{−10} ‖Jlag(−5/2+it)‖ dt = ∫_{10}^{T} ‖Jlag(−5/2+it)‖ dt by substitution t → −t (intervalIntegral.integral_comp_neg or similar). That avoids duplicating the R-bound for negative t. \n     \n     So: ∫_{-T}^{T} ‖J‖ = ∫_{-T}^{-10} + ∫_{-10}^{10} + ∫_{10}^{T} = 2·∫_{10}^{T} ‖J‖ + ∫_{-10}^{10} ‖J‖ (by the substitution + Jlag_conj). Then bound each.\n     \n     In Lean: intervalIntegral.integral_comp_neg : ∫ x in a..b, f (−x) = ∫ x in −b..−a, f x. So ∫_{-T}^{-10} ‖J(−5/2+it)‖ dt — write ‖J(−5/2 + it)‖ = ‖J(−5/2 + i(−(−t)))‖... define g(t) := ‖Jlag n (−5/2 + t·I)‖. g(−t) = ‖Jlag n (−5/2 − t·I)‖ = ‖Jlag n (conj(−5/2 + t·I))‖ = ‖(starRingEnd)(Jlag n (−5/2+t·I))‖ (Jlag_conj, needs s ≠ 1 ✓ re −5/2) = ‖Jlag n (−5/2+t·I)‖ = g(t). So g is even. ∫_{-T}^{-10} g = ∫_{10}^{T} g(−u) du (u = −t, integral_comp_neg) = ∫_{10}^{T} g(u) du ✓.\n\n   - Assembly: ∫_{-T}^{T} ‖J‖ ≤ 2·∫_{10}^{T} 2·((2/3)Z2hat T + 10.5 log(t+2) + 48) dt + ∫_{-10}^{10} 2·1.3352 dt ≤ 2·2·(T−10)·((2/3)Z2hat T + 10.5 log(T+2)+48) + 20·2·1.3352 ≤ 4T·(...) + 40·1.3352 ✓ (T − 10 ≤ T, log(t+2) ≤ log(T+2) monotone ✓).\n\n   Integration machinery: the bound on ∫_{10}^{T} ‖J‖ — need ∫ ≤ ∫ of bounds: `intervalIntegral.norm_integral_le_of_norm_le` (for bound depending on t: needs IntegrableOn of the majorant — the majorant (2/3)Z2hat T + 10.5 log(t+2) + 48 is continuous in t ✓) or bound by constant after monotone reduction: ‖J(−5/2+it)‖ ≤ 2·((2/3)Z2hat T + 10.5 log(T+2) + 48) on [10, T] (const in t!) — then `norm_integral_le_of_norm_le_const`. Simpler: reduce to a CONSTANT majorant per segment first, then norm_integral_le_of_norm_le_const. But wait — the capstone gives the R-bound with the near-sum SUBTRACTED, not ‖logDeriv‖ directly. ‖logDeriv‖ ≤ ‖nearsum‖ + ‖R‖ (norm sub). So per t: ‖J(t)‖ = ‖kFun‖·‖logDeriv‖ ≤ 2·(‖nearsum(t)‖ + (10.5 log(t+2)+48)) ≤ 2·((2/3)Z2hat T + 10.5 log(T+2) + 48) = const ✓. Then ∫_{10}^{T} ≤ (T−10)·const. \n\n   Need: logDeriv = deriv ζ / ζ — Jlag n s = kFun n s * (−(deriv riemannZeta s / riemannZeta s)). logDeriv f = f'/f. So −(deriv ζ/ζ) = −logDeriv ζ ✓ definitional (logDeriv_def). ‖−x‖ = ‖x‖ ✓.\n\n4. **I_I**: `vIntegral_Jlag_right_vertical_norm_le` : ‖VIntegral (Jlag n) (2√n) (−T) T‖ ≤ IIMaj n.\n   - ‖VIntegral‖ = ‖∫_{-T}^{T} J(2√n + it) dt‖ ≤ ∫_{-T}^{T} ‖J‖ (norm_integral_le_of_norm_le with the constant majorant or norm_integral_le_of_norm_le_const).\n   - Per t: ‖kFun n (2√n+it)‖ ≤ e^{√n/2}+1 — which lemma? kFun_shift_norm_le_exp_sqrt_half_add_one (LiContour, ii′-4): \"right vertical, 2√n ≤ re s\". Check its exact hypotheses. Or DL-4's kFun_right_vertical_norm_le_exp_sqrt_half_add_one {n} {t} (hn : 16 ≤ n) ... — DL-4 is for the dog-leg's V_right at height T..U; here t ∈ [−T, T] with |t| ≤ T ≤ √n+1 — DL-4's lemma might require t ≥ something. The ii′-4 kFun_shift_norm_le_exp_sqrt_half_add_one: (hs : 2√n ≤ s.re) (hn : n ≤ s.im²)? That would FAIL for small t! Hmm — \"right vertical, 2√n ≤ re s\" from the checklist: `kFun_shift_norm_le_exp_sqrt_half_add_one` (right vertical, 2√n ≤ re s). Kernel |1 − (s/(s−1))ⁿ|: |s/(s−1)| = |1 + 1/(s−1)| ≤ 1 + 1/|s−1|. |s−1| ≥ re(s) − 1 ≥ 2√n − 1. (1+1/(2√n−1))ⁿ ≤ e^{n/(2√n−1)} ≤ e^{√n/2} (n/(2√n−1) ≤ √n/2 ⟺ 2n ≤ 2n − √n ⟺ 0 ≤ −√n — FALSE! n/(2√n−1) = √n/(2−1/√n) ≈ √n/2·(1+1/(2√n)) > √n/2. Hmm so e^{n/(2√n−1)} ≤ e^{√n/2 + something}. Let me just check the lemma statement directly.\n   - Zeta: norm_logDeriv_zeta_le_iimZeta (n ≥ 5): ‖ζ′/ζ(2√n+it)‖ ≤ 0.57·2^{−(2√n−2)} ✓ any t.\n   - So ‖I_I‖ ≤ 2T·(e^{√n/2}+1)·0.57·2^{−(2√n−2)} ≤ 2(√n+1)·(...)·0.57·2^{−(2√n−2)} = IIMaj n ✓ definitional.\n\n**6-c-ii: mid horizontals** (the long pole)\n- `hIntegral_Jlag_mid_norm_le` : ‖HIntegral (Jlag n) (−5/2) 3 T‖ ≤ (e⁴+1)·(2·Z2hat T·log(16.5·9·C0hat(√n+2)) + 5.5·(10.5·log(T+2)+48)).\n  - Per σ ∈ [−5/2, 3]: ‖J(σ+iT)‖ ≤ (e⁴+1)·‖logDeriv ζ(σ+iT)‖ (kFun_shift_norm_le_exp_four_add_one: needs re ≤ 3 ✓ and n ≤ T² ✓ from T ≥ √n).\n  - ∫_{-5/2}^{3} ‖logDeriv‖ dσ ≤ ∫ ‖nearsum‖ + ∫ ‖R‖.\n  - ‖R(σ+iT)‖ ≤ 10.5 log(T+2) + 48 const ⟹ ∫ ≤ 5.5·(...) via norm_integral_le_of_norm_le_const. Wait — need hζ: ζ(σ+iT) ≠ 0 on the whole segment: T zero-avoiding-wide gives clearance from zeros with γ ∈ (√n−1, √n+2). Zeros with γ outside that window: |T−γ| ≥ ... if γ ≥ √n+2 then γ − T ≥ √n+2−(√n+1) = 1 > 0 ✓ not on the path (path has im exactly T). If γ ≤ √n−1: T − γ ≥ √n − (√n−1) = 1 > 0 ✓. Inside the window: clearance ≥ 1/(9Ĉ₀) > 0 ✓. So no zero on the horizontal ✓ (needed both for the capstone hζ and integrability).\n  - The near-sum integral: ∫_{-5/2}^{3} ‖Σ_{ρ ∈ nearZerosSub T} mult/(s−ρ)‖ dσ ≤ Σ mult·∫_{-5/2}^{3} dσ/‖σ+iT−ρ‖.\n    - Swap: the sum is finite; need ∫ ‖Σ‖ ≤ ∫ Σ‖·‖ = Σ ∫‖·‖: norm_sum_le inside the integral + intervalIntegral.integral_finset_sum (needs each IntegrableOn: 1/‖s−ρ‖ continuous in σ since ‖·‖ > 0 ✓).\n    - Per-zero: ρ = β+iγ, β ∈ (0,1), δ := |T−γ| ≥ c := 1/(9·C0hat(√n+2)) (zeros in nearZerosSub T have |γ−T| < 1 ⟹ γ ∈ (T−1, T+1) ⊆ (√n−1, √n+2) ✓ the wide clearance applies).\n      ∫_{-5/2}^{3} dσ/√((σ−β)²+δ²) ≤ 2 + 2·log(5.5/δ)?? via the split at β:\n      - The antiderivative route: FTC with arcsinh or log(σ−β+√((σ−β)²+δ²)). \n      - The crude split route: ∫_{[β−δ, β+δ]} ≤ 2δ·(1/δ) = 2; ∫_{outer} ≤ ∫_{outer} dσ/|σ−β| = [log] = log((3−β)/δ) + log((β+5/2)/δ) ≤ 2·log(5.5/δ).\n      For the outer integral: ∫ dσ/|σ−β| over [−5/2, β−δ] ∪ [β+δ, 3]. On the right part: 1/(σ−β), antiderivative log: log(3−β) − log(δ) ✓ `intervalIntegral.integral_one_div`? or `integral_deriv_eq_sub'` with HasDerivAt log. On the left: 1/(β−σ), antiderivative −log(β−σ): = log(β+5/2) − log δ ✓.\n      Then total ≤ 2 + log((3−β)(β+5/2)/δ²) ≤ 2 + 2·log(5.5/δ) (each factor ≤ 5.5: 3−β ≤ 3 ≤ 5.5, β+5/2 ≤ 7/2 ≤ 5.5 ✓... wait need (3−β)/δ · (β+5/2)/δ ≤ (5.5/δ)² — each ≤ 5.5/δ ✓ product ≤ (5.5/δ)² ✓ log ≤ 2 log(5.5/δ) ✓).\n      Then 2 + 2·log(5.5/δ) ≤ 2·log(16.5/δ): 2·log(16.5/δ) − 2·log(5.5/δ) = 2·log 3 ≥ 2 ✓ (log 3 ≥ 1 — certified: log 3 ≥ 1.0986 — exists in LiTightR: log 3 ≤ 1.0987 upper; lower bound? e ≥ 2.718... log 3 ≥ 1 ⟺ 3 ≥ e ⟺ certified via Real.exp_one_lt_d9: e ≤ 2.7182818286 ≤ 3 ✓).\n      And 2·log(16.5/δ) ≤ 2·log(16.5/c) since δ ≥ c ⟹ 16.5/δ ≤ 16.5/c (log monotone, 16.5/δ ≥ ... need positivity ✓).\n      So per zero: ∫ ≤ 2·log(16.5·9·C0hat(√n+2)).\n    - Total near: ≤ (Σ_{nearZerosSub T} mult)·2·log(16.5/c) ≤ Z2hat T·2·log(16.5/c) = NI(T) ✓.\n      Σ mult ≤ Z2hat T: nearZerosSub T (|γ−T| < 1) ⊆ zeroAbsWindow T (≤ 1) + ZeroCountProp2 (T ≥ 10 ✓ since T ≥ √n ≥ √(10⁵)... wait n here: the side bounds apply for n ≥ 10⁵ (the SfBoundProp range). T ≥ √10⁵ = 316.2 ✓ ≥ 10 ✓).\n      nearZerosSub is a subtype finset; zeroAbsWindow is a set→toFinset of ℂ. The bridge: Σ_{nearZerosSub T} zeroMult ρ.1 ≤ Σ_{zeroAbsWindow T toFinset} zeroMult — map nearZerosSub T into ℂ via Finset.map/attach... nearZerosSub t is defined as (finite_subtype_norm_lt (|t|+3)).toFinset.filter ... — a Finset of the SUBTYPE. There's probably already a bridge lemma (the 5f assembly must convert to ℂ-valued sums — near_sum_refPoint_le or similar). Let me check how 5f's near_sum_refPoint_le bridges to ZeroCountProp2 — it proves ‖Σ_{nearZerosSub t} mult/(s₀−ρ)‖ ≤ 0.6L + 0.886LL + 2.7? That would be EXACTLY the bridge I need (with the denominator removed — |s₀−ρ| ≥ 1 at the reference point). Let me look at near_sum_refPoint_le: if it shows Σ mult·‖1/(s₀−ρ)‖ ≤ Z2hat t using ‖s₀−ρ‖ ≥ 1, then inside it must have the Σ mult ≤ Z2hat bridge. Reusable.\n\n  - The negative horizontal (−T): conj trick (Jlag_conj + intervalIntegral_conj) like DL-5 — but the mid machine is built at +T; conj gives the same norm ✓.\n\n- Total horizontals: HIntegral (−5/2) (2√n) (±T) = HIntegral (−5/2) 3 (±T) + HIntegral 3 (2√n) (±T) (adjacent intervals) ⟹ ‖full‖ ≤ mid-bound + DogLegRight. Both sides: 2·(e⁴+1)·NI-charge + 2·DogLegRight. Then the pinch NI + 5.5(...) ≤ 7Hhat T ⟹ ≤ 2(e⁴+1)(7Ĥ) + 2·DogLegRight ✓ Bn's horizontal charge.\n\n**The pinch** (NI + 5.5·(10.5 log + 48) ≤ 7·Hhat T): Hhat T = 3Ĉ₀(T)² + 10.5 log(T+2) + 48. Need 2·Z2hat(T)·log(148.5·Ĉ₀(√n+2)) ≤ 21·Ĉ₀(T)² + 1.5·(10.5 log(T+2)+48)... since 5.5·X ≤ 7·X − 1.5·X: suffices 2·Z2hat T·log(148.5·Ĉ₀(√n+2)) ≤ 21·Ĉ₀(T)² + 1.5·(10.5 log(T+2) + 48). Actually simpler: 7Hhat − 5.5·(10.5 log+48) = 21Ĉ₀² + 1.5·(10.5 log+48) ≥ 21Ĉ₀². Suffices: 2·Z2hat(T)·log(148.5·Ĉ₀(√n+2)) ≤ 21·Ĉ₀(T)².\n  With T ∈ [√n, √n+1]: Ĉ₀(√n+2) ≤ Ĉ₀(T+2) ≤ Ĉ₀(T)·(1+small). And Z2hat T = 0.6L + 0.886LL + 2.7, Ĉ₀ T = 0.433L + 0.886LL + 2.9 where L = log(T+2), LL = log L.\n  21·Ĉ₀² ≥ 21·(0.433L)² = 3.94·L². LHS ≈ 2·(0.6L + 0.886LL + 2.7)·(log 148.5 + log Ĉ₀(√n+2)) ≈ 2·(0.6L)·(5 + log(0.433L)) ≈ 1.2·L·(5 + LL). Need 1.2·L·(5+LL) ≤ 3.94·L² ⟺ 1.2(5+LL) ≤ 3.94·L ⟺ true for L ≥ ~2.5-ish. At the base n = 10⁵: L = log(√10⁵+1+2) = log(319.2) ≈ 5.766, LL ≈ 1.75: LHS 1.2·(6.75) = 8.1 vs RHS 3.94·5.77 = 22.7 ✓ huge margin.\n  Lean proof: pinch-lemma style — both sides functions of T ∈ [√n, ∞); prove at the left endpoint T₀ = √10⁵... but T ranges over [√n, √n+1] for n ≥ 10⁵ ⟹ T ≥ √10⁵. Show f(T) := 21Ĉ₀(T)² − 2·Z2hat(T)·log(148.5·Ĉ₀(T+2)) ≥ 0 for T ≥ √10⁵. Via: certified endpoint value at T₀ = √10⁵ (rational interval bounds: √10⁵ ≈ 316.227, L₀ = log(318.23)... ) + growth: f′ ≥ 0 or a monotone-ratio argument. The clean way (per D-071: \"certified endpoint evaluation + growth-direction argument\"): \n  - Ĉ₀(T)²/L² ≥ 0.433² etc. Actually simplest: 21·Ĉ₀(T)² ≥ 21·(0.433·L)² = 3.94·L² requires dropping the LL and const terms (they're positive for T ≥ √10⁵: LL = log log(T+2) ≥ log log 318 ≥ log 5.76 ≥ 1.75 > 0 ✓).\n  - Z2hat(T) ≤ 0.6L + 0.886·(L/e)?? No — log log x ≤ log x/e... Actually log L ≤ L/e for L > 0 (log x ≤ x/e). So Z2hat ≤ 0.6L + 0.886L/e + 2.7 ≤ (0.6 + 0.326)L + 2.7 = 0.926L + 2.7. And 2.7 ≤ 0.468·L for L ≥ 5.77 (2.7/5.77 = 0.468) ⟹ Z2hat ≤ 1.394·L.\n  - log(148.5·Ĉ₀(T+2)): Ĉ₀(T+2) = 0.433·log(T+4) + 0.886·log log(T+4) + 2.9. log(T+4) ≤ L·(1+ε): log(T+4) = log(T+2) + log(1 + 2/(T+2)) ≤ L + 2/(T+2) ≤ L + 0.0063 (T+2 ≥ 318). So Ĉ₀(T+2) ≤ 0.433(L+0.0063) + 0.886·log(L+0.0063) + 2.9 ≤ 0.433L + 0.886·(log L + 0.0011) + 2.903. ≤ Ĉ₀(T) + 0.0037. Hmm — and Ĉ₀(T) ≤ 0.433L + 0.886·(L/e) + 2.9 = 0.759L + 2.9 ≤ 0.759L + 0.503L = 1.262·L (L ≥ 5.76). So 148.5·Ĉ₀(T+2) ≤ 148.5·1.262·(L+0.0063) ≈ 187.4·L. log(187.4·L) = log 187.4 + log L ≤ 5.234 + LL... hmm log 187.4 ≈ 5.233. And LL ≤ L/e ≤ 0.368L. So log(148.5·Ĉ₀(T+2)) ≤ 5.234 + 0.368·L ≤ 0.908·L + 0.368L?? For L ≥ 5.76: 5.234 ≤ 0.908·L ✓ ⟹ ≤ 1.276·L.\n  - Then LHS = 2·Z2hat·log ≤ 2·(1.394L)·(1.276L) = 3.558·L². vs RHS 21·(0.433L)² = 3.940·L² ✓ fits with margin 0.38·L². \n  - All steps are elementary log/LL comparisons with certified constants (log 187.4 ≤ 5.234 ⟺ 187.4 ≤ e^{5.234} — exp-machine certified; log x ≤ x/e via Real.log_le_sub_one_of_pos? log x ≤ x − 1 — that gives log L ≤ L − 1 which is worse. log x ≤ x/e: from Real.log_le_sub_one: log(x/e) ≤ x/e − 1 ⟹ log x ≤ x/e − 1 + 1 = x/e ✓ since log(x/e) = log x − 1. There's `Real.log_le_self`? The clean one: Real.log_le_sub_one_of_pos (log y ≤ y − 1) applied at y = x/e: log x − 1 ≤ x/e − 1 ⟹ log x ≤ x/e ✓).\n  \n  This pinch is 6-d territory per D-071 (the fold). But the per-side bounds in 6-c should produce the NI-form bound, and 6-d folds with the pinch. Actually — cleaner division: 6-c proves the four side bounds in the *explicit charged form* (I_III ≤ 4T((2/3)Z2hat+10.5 log+48) + 40·1.3352, mid horizontal ≤ (e⁴+1)(NI + 5.5(10.5 log+48)), right tails ≤ DogLegRight (done), I_I ≤ IIMaj), and 6-d does: horizontal pinch + total assembly + RectangleIntegral' 2π factor + sfBoundProp. \n\nn-range: SfBoundProp needs n ∈ [10⁵, N₁]. The side bounds need: n ≥ 16 (dog-leg), T ≥ 10 (capstone/Z2 — n ≥ 10⁵ gives T ≥ 316 ✓), n ≤ N₁ for the bridge (T ≤ √N₁ + 1 = 3×10¹² ✓ hTle).\n\nWhere to put the code: new file `LiSideBounds.lean` importing LiAssembly + LiDogLeg. Root-import it.\n\nOrder of build:\n- 6-c-i: scaffolding (rectangle decomposition, horizontal split, Jlag integrability on the paths, logDeriv = Jlag factor rfl-bridges, the even-symmetry g(−t) = g(t) helper, Z2hat mono).\n- 6-c-ii: I_III bound.\n- 6-c-iii: I_I bound.\n- 6-c-iv: mid horizontal machine (per-zero segment integral + near-sum swap + R-part).\n- Then 6-d.\n\nThis is a big stage (D-071 estimates 1–2 sessions). Let me set up the todo list and start with 6-c-i scaffolding.\n\nFirst, let me check some signatures I'll need:\n1. kFun_shift_norm_le_exp_four_add_one (LiContour) — exact hyps.\n2. kFun_shift_norm_le_exp_sqrt_half_add_one (LiContour) — exact hyps.\n3. norm_logDeriv_zeta_le_iimZeta — exact hyps (n ≥ 5, any t? check).\n4. near_sum_refPoint_le (LiTightR) — the Z2hat bridge.\n5. Z2hat mono — exists?\n6. intervalIntegrable machinery for Jlag on the horizontal/vertical paths.\n7. intervalIntegral.integral_comp_neg.\n\nLet me grep these.","signature":""},{"type":"text","text":"I have the full map now. The pieces: RectangleIntegral = bottom − top + right − left (Zeta23:52–54); tight capstone at σ∈[−5/2,3], t≥10 (LiTightR:4299); nearZerosSub with |γ−t|<1; ZeroCountProp2 = Z2hat form. Setting up the ii′-6-c plan and checking the last signatures."},{"type":"tool_use","id":"TodoWrite_26","name":"TodoWrite","input":{"todos":[{"content":"6-c-i: scaffolding (rectangle decomposition, path integrability, symmetry helpers, Z2hat mono)","status":"in_progress","activeForm":"Building 6-c-i scaffolding"},{"content":"6-c-ii: I_III left-vertical bound ≤ 4T((2/3)Z2hat+10.5 log+48) + 40·1.3352","status":"pending","activeForm":"Proving the I_III left-vertical bound"},{"content":"6-c-iii: I_I right-vertical bound ≤ IIMaj n","status":"pending","activeForm":"Proving the I_I right-vertical bound"},{"content":"6-c-iv: mid-horizontal segment machine ≤ (e⁴+1)(NI + 5.5(10.5 log+48))","status":"pending","activeForm":"Building the mid-horizontal segment machine"},{"content":"6-c-v: full horizontal assembly (mid + dog-leg tails, both sides)","status":"pending","activeForm":"Assembling the full horizontal bounds"},{"content":"ii′-6-d: the fold (pinch + 2π factor + sfBoundProp)","status":"pending","activeForm":"Folding into sfBoundProp"}]},"extra_content":null}]