[{"type":"thinking","thinking":"Now I see the H(T) derivation (D-036 §2):\n\nLine 55-60: \"Zeros in [√n, √n+1]: ≤ C₀(√n+1). Pigeonhole: some gap ≥ 1/(C₀+1); choose T at a gap center ⟹ d_min ≥ 1/(3C₀(√n+1)). Then on the horizontal segments: |ζ′/ζ(s)| ≤ C₀(T)/d_min + A log(T+2) + B₀ ≤ 3C₀(T)² + A log(T+2) + B₀ =: H(T).\"\n\nSo the near sum at the chosen T is bounded C₀(T)/d_min where d_min = 1/(3C₀(√n+1)) — and C₀(T) is used as the count of |γ−T|<1. This is the SAME convention: one C₀ for the |γ−T|<1 window.\n\nHmm, wait — the pigeonhole as stated: zeros in [√n, √n+1] counted by C₀(√n+1); T chosen in [√n, √n+1] at a gap center with d_min ≥ 1/(3C₀) — but only from zeros IN [√n, √n+1]. A zero at √n+1+ε (just outside the window) is at distance ε from the window boundary — T could be near √n+1 and the zero just outside could be at distance < d_min from T!\n\nHmm, unless the pigeonhole is applied to the LARGER window. Let me look at how ii′-4's L3 (exists_zero_avoiding_T) was actually stated and used: \"∃ T ∈ [a, a+1], ∀ ρ zero with a ≤ im ρ ≤ a+1: |ρ.im − T| ≥ 1/(3·C0hat(a+1))\". Only window zeros. So the clearance is only guaranteed vs window zeros.\n\nBut the near sum at height T runs over |γ − T| < 1 which includes zeros in (a−1, a) and (a+1, a+2) — those have NO clearance guarantee!\n\nHmm, wait. But actually — is that a problem in the PAPER's accounting? The near sum Σ_{|γ−T|<1} 1/(s−ρ): for the horizontal contour at height T, s = σ + iT, |s − ρ| ≥ |T − γ| ≥ d_min only for γ in the window. For γ just outside the window (say γ = a+1+ε), |T−γ| could be tiny if T is near a+1... \n\nBUT: does the R-bound's near/far split save it? R(s) = ζ′/ζ(s) − Σ_{|γ−T|<1} 1/(s−ρ) — the R-bound |R(s)| ≤ A log + B₀ holds everywhere (no clearance needed). Then |ζ′/ζ(s)| ≤ |R(s)| + Σ_{|γ−T|<1} 1/|s−ρ|. The near sum needs BOTH the count AND the per-term clearance 1/|s−ρ| ≥ ... for s on the horizontal at height T: |s−ρ| ≥ |T−γ|. For γ ∈ window: ≥ 1/(3C₀). For γ outside the window but within |γ−T|<1: γ ∈ (a−1, a) ∪ (a+1, a+2) with T ∈ [a, a+1]: |T − γ| can be arbitrarily small!! \n\nHmm, hold on — but if |T − γ| < 1/(3C₀) for an out-of-window zero, then γ is within 1/(3C₀) of T... T ∈ [a, a+1], γ ∈ (a+1, a+2): |γ−T| ≥ γ − (a+1)... if T is at distance ≥ δ from BOTH endpoints a and a+1, then out-of-window zeros (which are ≥ 0 from the boundary... no — an out-of-window zero can be AT a+1+ε for any ε > 0, so its distance to T ≤ a+1 is ≥ (a+1) − T. If the pigeonhole placed T in the MIDDLE of the window (distance ≥ 1/4 from each endpoint), then out-of-window zeros have |γ − T| ≥ 1/4 − ... hmm: γ > a+1 (outside [a, a+1]) and T ≤ a+1: |γ − T| = γ − T ≥ γ − (a+1) + (a+1) − T ≥ (a+1) − T ≥ (window − midpoint distance). If T ∈ [a+1/4, a+3/4] then |γ−T| ≥ 1/4 for γ ∉ (a−... wait γ could also be in (a−1, a): |γ−T| ≥ T − a ≥ 1/4. And window zeros: ≥ 1/(3C₀) ≤ 1/4-ish. So with T centered, ALL |γ−T|<1 zeros have clearance ≥ min(1/(3C₀), 1/4) = 1/(3C₀) (C₀ ≥ 2). So the near sum ≤ count·3C₀ where count ≤ 3·C₀ (three unit windows) → 9·C₀². But D-036 wrote 3·C₀² — using count ≤ C₀ for the near window.\n\nHmm OK. So there are TWO accounting gaps between the paper sketch (D-036) and a fully honest Lean assembly:\n(i) the near-window count is really 2–3 unit-window counts, not one;\n(ii) the pigeonhole clearance only covers window zeros (need T centered or a two-sided pigeonhole).\n\nBUT — wait. These are the PAPER-side accounting for ii′-6 (the L0 assembly), not 5f! 5f is just the R-bound: |R(s)| ≤ 10.5 log + 48. The R-bound's D-056 proof has only ONE place where the count enters with a tight constant: piece 2 (the near sum at the reference point s₀). Everything else (pieces 1, 3–6) is count-free or uses the count with room (piece 3's per-interval counts).\n\nSo for 5f specifically, the question is whether the honest piece-2 count (2·C₀(t) for the two-unit window) breaks the 10.5/48 fold. From my computation: with 2C₀ for piece 2, total = 14.73·C₀(t) + 7.97 ≤ 14.73·(0.433 log + 0.886 loglog + 2.9) + 7.97 = 6.38 log + 13.05 loglog + 42.72 + 7.97 = 6.38 log + 13.05 loglog + 50.69. Fold loglog ≤ log/e: ≤ (6.38 + 13.05/e)·log + 50.69 = (6.38 + 4.80)·log + 50.69 = 11.18 log + 50.69. The baked constants: 10.5/48. 11.18 > 10.5 and 50.69 > 48. BREAKS.\n\nHmm. But wait — is the paper's piece-2 one-C₀ convention actually DEFENSIBLE? Let me think again... |γ − t| < 1. Hmm, what if the near-sum convention in the paper is |γ − t| ≤ 1 with the count C₀(t) being the count of |γ−t| ≤ 1 — i.e., the paper's C₀(t) was ALWAYS meant as the two-unit-window count? D-036 §0 line 20 defines n(t) := N(t+1) − N(t) (one unit) — but maybe D-056's C₀(t) := F(t+1) − F(t) + S_b(t+1) + S_b(t)... that's N(t+1)−N(t) — ONE unit. So no, one unit.\n\nHmm, unless the two-unit count really is ≤ C₀(t) via... N(t+1) − N(t−1) ≤ F(t+1) − F(t−1) + S(t+1) + S(t−1). F(t+1)−F(t−1) ≈ (2/2π)·log(t/2π) + ... ≈ 2 × (one-unit F-difference). So the two-unit count ≈ 2·C₀(t) − adjustments. Definitely 2×.\n\nSo D-056's assembly has a genuine factor-2 gap at piece 2. What are the options?\n\nOption 1: Re-fold with honest constants and check the margin still works. The honest fold gives ≈ 11.2 log + 50.7 — exceeds the baked 10.5/48. The margin would need re-verification with the new constants: B(n)'s leading coefficient 4·(0.1443 + A/2): A = 11.2 → 4·(0.1443+5.6) = 22.97 vs the old 21.6 — a ~6% increase in the leading √n log n coefficient. The margin at N₀ = 80000 had huge slack (margiñ(8×10⁴) ≥ 8001 certified vs the base requirement...) — actually the margin trail: margin(10⁵) ≈ 9.3×10⁴ measured. A 6% increase in the leading coefficient reduces the margin by... at n = 10⁵, √n log n ≈ 316·11.5 ≈ 3634; ×(22.97−21.6) ≈ ×1.37/21.6... the margin is ~9.3×10⁴ and the B-side grows by maybe ~5%: margin shrinks by ~5-10% — still hugely positive. The N₀ crossover might move slightly. This is doable but changes the baked constants everywhere (Hhat, marginTilde, the certified base points margiñ(8×10⁴) ≥ 8001, the paper text). COSTLY + freeze-sensitive (paper edits forbidden until ii′-7... the constants are baked in LiSkeleton which is proof-relevant — margiñ base points were CERTIFIED against the current constants).\n\nOption 2: Tighten piece 2's INPUT — the near-window count — via a tighter split: |γ−t| < 1 is (t−1, t+1). Bound N(t+1) − N(t−1) DIRECTLY via Trudgian: F(t+1)−F(t−1) + S(t+1) + S(t−1) — this is the honest 2-unit count ≈ 2·C₀(t) − 2.9-ish? Let me compute: F-difference over 2 units ≈ (1/π)·log(t/2π) ≈ 2·(0.433 log(t+2) − 2.9-ish F-part)... the S-pair: S(t+1)+S(t−1) ≈ 2·(0.137 log + 0.443 loglog + 1.588). The honest 2-unit count = 2·C₀(t) − small. No real savings.\n\nOption 3: Sharpen piece 2's PER-TERM bound: |s₀ − ρ| ≥ √(1 + (t−γ)²) (since |re(s₀−ρ)| = 2−β ≥ 1). So 1/|s₀−ρ| ≤ 1/√(1+(t−γ)²) — for the near window, the terms with |t−γ| close to 1 are smaller. Split the near window into sub-intervals: |t−γ| ≤ 1/2 and 1/2 < |t−γ| < 1: the inner ≤ C₀(t)-ish (one unit window!) × 1, the outer ≤ 2·C₀... hmm — inner window |t−γ| ≤ 1/2 ⊂ one unit window ≤ C₀(t); outer (1/2 < |t−γ| < 1): two half-windows, count ≤ 2·C₀... per-term ≤ 1/√(1+1/4) = 2/√5 ≈ 0.894. So piece 2 ≤ C₀(t)·1 + 2·C₀(t)·0.894?? — worse than... no wait, outer count is ≤ 2 unit windows MINUS... ugh, the outer annulus (1/2, 1) around t is contained in (t−1, t+1) — two windows — count ≤ 2C₀(t) − ... this gives ≤ C₀ + 0.894·2C₀ = 2.79·C₀ — worse than 2C₀. No.\n\nHmm, actually: |t−γ|<1 window: count ≤ 2·C₀(t) is the ONLY honest bound (without fancier density input). So piece 2 ≤ 2·C₀(t) honestly.\n\nOption 4: Reduce piece 3's coefficient to compensate. Piece 3 currently 12.73·C₀ + 7.06 (from 4.5√2·[2C₀ + 1.11]). Can it be tightened? The 4.5 = |s₀−s| ≤ |2−σ| ≤ 4.5 (σ ∈ [−5/2, 3]). The σ range: why −5/2? D-036's contour has σ₀ = −5/2 (left vertical). For the R-bound used at the CONTOUR (the horizontals at height T), σ ∈ [−5/2, 2√n]... The R-bound is applied on the horizontal segments σ ∈ [−5/2, 2√n] and the left vertical σ = −5/2. Hmm, σ up to 2√n — D-056's σ ≤ 3?! The right part σ ∈ [3, 2√n] uses the stepping argument (D-036 §3 II/IV) not the R-bound... Actually the R-bound for σ ∈ [−5/2, 3] + the stepping for σ > 3. So |s₀−s| ≤ 4.5 is needed at σ = −5/2.\n\nTighten the far-sum per-interval accounting: D-056 used |s₀−ρ| ≥ (1+|t−γ|)/√2 and |s−ρ| ≥ |t−γ|, giving 4.5√2/(k(k+1)). Alternative: |s−ρ| = √((σ−β)²+(t−γ)²) ≥ √((t−γ)²) = |t−γ| ✓; |s₀−ρ| ≥ √(1+(t−γ)²) ✓ (2−β ≥ 1 exactly? β < 1 ⟹ 2−β > 1; β ≤ 1 ⟹ ≥ 1 ✓). Term ≤ 4.5/(|t−γ|·√(1+(t−γ)²)). For k ≤ |t−γ| < k+1: ≤ 4.5/(k·√(1+k²)) ≤ 4.5/(k²). Σ_{k≥1} 4.5·2·C₀/k² = 9·C₀·π²/6 = 14.8·C₀ — WORSE than 12.73. D-056's (1+|t−γ|)/√2 trick is better.\n\nHmm — actually D-056's term: 4.5√2/(|t−γ|(1+|t−γ|)) ≤ 4.5√2/(k(k+1)) for |t−γ| ≥ k ✓ (x(1+x) ≥ k(k+1) for x ≥ k ✓). Sum over intervals: left side intervals k=1..~t, right side k=1..~t plus tail. ≤ 4.5√2·C₀(t)·[Σ_{k≤t} 1/(k(k+1)) + Σ_{k≤t, right} C₀(2t)/C₀(t)/(k(k+1)) + tail] = 4.5√2·[C₀(t)·(1−1/(t+1)) + C₀(2t)·(1−...) + 0.53]. ≈ 6.364·[C₀ + C₀(2t) + 0.53] ≈ 6.364·[2C₀ + 0.58 + 0.53]. To tighten: C₀(2t) ≤ C₀(t) + 0.58 — already used. The 4.5√2 factor: |s₀−s| = 2−σ ≤ 4.5 only at σ = −5/2; could split by σ? The R-bound is needed uniformly on σ ∈ [−5/2, 3]. The extreme σ = −5/2 drives 4.5. If we split the contour usage: on the horizontals σ ∈ [−5/2, 3]... the horizontal integral bounds use sup over the whole segment — need the σ = −5/2 endpoint. Hmm.\n\nAlternatively — reduce piece 3 by using |s−ρ| ≥ |t−γ| AND |s₀−ρ| ≥ max(1, |t−γ|)... that's what (1+x)/√2 does.\n\nOK this constant-tightening spiral is exactly the kind of thing E-028's 26× slack says is unnecessary. The measured max |R| = 4.75 at t up to 1000 (E-021) vs the bound 10.5·log(1002)+48 ≈ 120. The traced assembly is lossy by ~25×. The honest fix for the factor-2: RE-FOLD the assembly with honest constants and re-verify the margin. But the margin constants are baked in LiSkeleton (10.5/48 in Hhat/marginTilde) with CERTIFIED base points...\n\nHmm wait, actually — hold on. Let me re-examine whether piece 2's 2× is really needed, ONE more time. The near sum Σ_{|γ−t|<1} 1/|s₀−ρ|. |s₀−ρ| ≥ 1... but actually MORE: |s₀−ρ|² = (2−β)² + (t−γ)² ≥ (2−β)² ≥ 1. Yes ≥ 1. And the count of |γ−t|<1... \n\nHmm — actually WAIT. Is the count of |γ − t| < 1 really 2·C₀? The window (t−1, t+1) — 2 units. But C₀(t) as DEFINED in D-056 is F(t+1)−F(t) + S_b(t+1) + S_b(t) — hmm, what if D-056 intended C₀(t) as the count of the TWO-unit window |γ−t|≤1, i.e., N(t+1)−N(t−1) ≤ F(t+1)−F(t−1) + S_b(t+1)+S_b(t−1), and the \"F(t+1)−F(t)\" in the text is a typo for F(t+1)−F(t−1)? Let me check the numeric value: F(t+1)−F(t−1) at t=10: F(x) = (x/2π)log(x/2π) − x/2π + 7/8. F(11)−F(9): F'(x) ≈ (1/2π)log(x/2π) ≈ 0.159·log(1.6) ≈ 0.075 per unit at x=10... so F(11)−F(9) ≈ 0.15. Plus S_b pair ≈ 2·(0.137·2.3 + 0.443·0.83 + 1.588) ≈ 2·2.27 = 4.54. Total ≈ 4.7 ≈ matches C₀(10) ≈ 4.78 (0.433·2.48+0.886·0.907+2.9 = 4.78). And the ONE-unit version: F(11)−F(10) ≈ 0.075 + S pair 4.54 ≈ 4.6 — nearly the same because the S_b pair dominates!! The F-difference is tiny compared to the S_b slack. So the two-unit count ≈ the one-unit C₀ to within ~0.1!\n\nOH. That's the resolution. The C₀(t) majorant is DOMINATED by the S_b pair (2·1.588 = 3.18 of the ~4.7 total), and the F-difference for one vs two units differs by only ~0.075. So C₀(t) as a CLOSED-FORM majorant (0.433 log(t+2) + 0.886 loglog(t+2) + 2.9) can absorb the two-unit window count — IF the closed form honestly majorizes the two-unit Trudgian count. Let me check: two-unit count ≤ F(t+1)−F(t−1) + S_b(t+1) + S_b(t−1). Need ≤ 0.433·log(t+2) + 0.886·loglog(t+2) + 2.9?\n\nF(t+1)−F(t−1) = ∫_{t−1}^{t+1} F'(x) dx where F'(x) = (1/2π)log(x/2π). At t=10: ≈ 2·0.159·log(10/6.28) ≈ 0.318·0.466 ≈ 0.148. S_b(t+1)+S_b(t−1) = 0.137·(log 11 + log 9) + 0.443·(loglog 11 + loglog 9) + 2·1.588 = 0.137·(2.398+2.197) + 0.443·(0.874+0.788) + 3.176 = 0.629 + 0.736 + 3.176 = 4.54. Total: 4.69 ≤ 4.78 ✓ (margin 0.09 at t=10). Hmm — TIGHT (2% margin). At larger t it should improve (the closed form's 0.433 log vs the F-part's (1/π)log = 0.318 log... wait: the two-unit F-difference ≈ (1/π)·log(t/2π) ≈ 0.318·log(t)−0.586 and the closed form has 0.433·log(t+2) for the F+log parts... S_b pair: 0.137·2·log t + 0.443·2·loglog t + 3.176 = 0.274 log t + 0.886 loglog t + 3.176 vs closed form 0.433 log(t+2) + 0.886 loglog(t+2) + 2.9. Difference: (0.433−0.318)·log + (0.274·... hmm let me redo: two-unit honest = F-diff + S-pair = (1/π)log(t/2π)-ish + 0.274 log t + 0.886 loglog t + 3.176. Total log coefficient: 0.318+0.274 = 0.592 vs closed form 0.433. The closed form UNDERCOUNTS the two-unit log coefficient (0.433 < 0.592)! At large t, the honest two-unit count EXCEEDS the closed form 0.433 log + ...!\n\nWait, that can't be right — let me recompute the one-unit version: one-unit count ≤ F(t+1)−F(t) + S_b(t+1)+S_b(t) ≈ (1/2π)·log(t/2π)·1 + 0.274 log + 0.886 loglog + 3.176 ≈ 0.159·log + 0.274·log + ... = 0.433·log + 0.886·loglog + 3.176-ish. AH — there it is: 0.433 = 0.159 (one-unit F-difference coefficient) + 0.274 (the S-pair log coefficient). So C₀(t)'s 0.433 log coefficient is exactly the ONE-unit honest count's log coefficient. The TWO-unit honest count has log coefficient ≈ 0.318 + 0.274 = 0.592 > 0.433. So the two-unit window count is NOT ≤ C₀(t) — it exceeds it at large t (break-even when 0.159·log t ≈ the constant slack ~ −0.3...: (0.592−0.433)·log t vs (2.9 − 3.176 − F-consts...) — the closed form's constant 2.9 vs honest 3.176: already negative; so the two-unit count exceeds C₀(t) essentially everywhere). \n\nCONCLUSION: D-056's piece 2 (and D-036's §1 near-sum and §2's H(T) count) genuinely need the two-unit window count ≈ 2·C₀(t)−ish, and the one-C₀ convention is an undercount by ~0.16·log t + 0.3 in the count, propagating to ~14.73·C₀+7.97 vs 13.73·C₀+7.97 in the R-bound fold. This is a REAL (if small) accounting slip in D-056's assembly — of the D-054-review class (this is exactly what the adversarial gauntlet is for — and it slipped through).\n\nHmm wait — but E-028 verified the R-bound numerically (26× slack) — so the THEOREM (10.5/48 bound) is true; it's the TRACED PROOF that has a gap. For the Lean 5f, I need a PROOF of the 10.5/48 bound — and the traced assembly with honest counting gives 11.2 log + 50.7, which does NOT imply 10.5 log + 48 (at t=10: 11.18·2.48+50.7 = 78.4 vs 10.5·2.48+48 = 74.0 — exceeds!). So the honest assembly as-is does NOT prove the baked bound. \n\nOptions:\n(A) Tighten the assembly to honestly fit 10.5/48. The slack analysis: the far-sum piece 3 (12.73·C₀ + 7.06) dominates. Can it be tightened enough? We need to save ~1·C₀ + 2.7 (to absorb the extra C₀ in piece 2 and the constant growth): target total ≤ 10.5 log + 48 with C₀ ≤ 0.433L + 0.886LL + 2.9:\n   Need 13.73·C₀ + 7.97 + extra-C₀ ≤ A·L + 48... currently 14.73·C₀ + 7.97 ≤ 14.73·(0.433L + 0.886LL + 2.9) + 7.97 = 6.38L + 13.05LL + 50.7. To fit 10.5L + 48: need to save 13.05·LL + 2.7 + (6.38+13.05/e−10.5)·L = 13.05LL + 0.68L + 2.7. From piece 3's 4.5√2·(2C₀+1.11): the per-term bound 4.5√2/(k(k+1)) is lossy: the actual term is 4.5/(x√(1+x²)) with x = |t−γ|; 4.5√2/(x(1+x)) vs 4.5/(x√(1+x²)): ratio √2·√(1+x²)/(1+x) → √2·x/(1+x) → √2 ≈ 1.414 as x→∞. So D-056's far bound is ≤ √2 × the true sum — the loss is up to 41%. Tightening piece 3 to 4.5·Σ C₀/(k·√(1+k²))... per-interval: term ≤ 4.5/(k·√(1+k²)); Σ_{k≥1} 1/(k√(1+k²)) = ? ≈ 1/1.414 + 1/(2·2.236) + 1/(3·3.16) + ... ≈ 0.707 + 0.224 + 0.105 + 0.062 + ... ≈ Σ ≈ 1.32-ish? vs Σ1/(k(k+1)) = 1. Hmm — 1.32 > 1, so the per-interval sharpened sum is BIGGER than the (1+x)/√2 form?? No wait: (1+x)/√2 ≤ √(1+x²)? (1+x)²/2 = (1+2x+x²)/2 vs 1+x²: (1+x)² ≤ 2(1+x²) ⟺ 1+2x+x² ≤ 2+2x² ⟺ 0 ≤ 1−2x+x² = (1−x)² ✓. So (1+x)/√2 ≤ √(1+x²), i.e., 1/√(1+x²) ≤ √2/(1+x) — the sharpened term 4.5/(x√(1+x²)) ≤ 4.5√2/(x(1+x)) ✓ D-056's is an upper bound of the sharpened one. The sharpened sum: Σ_k 4.5·count_k/(k√(1+k²)) where count_k ≤ C₀ for each unit interval (both sides: 2 intervals per k) — ≤ 4.5·C₀·[2·Σ_{k≥1} 1/(k√(1+k²))]·... but the C₀(2t) for the right side... the sum Σ 1/(k√(1+k²)): numerically ≈ let me estimate: k=1: 0.707, k=2: 0.2236, k=3: 0.1054, k=4: 0.0606, k=5: 0.0392, k=6: 0.0277, k=7: 0.0206, k=8: 0.0158, k=9: 0.0125, k=10: 0.0101, tail ≈ Σ_{k>10} 1/k² ≈ 0.1. Total ≈ 0.707+0.224+0.105+0.061+0.039+0.028+0.021+0.016+0.012+0.010+0.10 ≈ 1.32. Hmm so 2-sided: 2·1.32·4.5·C₀ = 11.9·C₀ vs D-056's 12.73·C₀ — saves only 0.8·C₀. Not enough (need ~1.7·C₀ + constants).\n\n(B) Accept the honest constants and RE-FOLD the whole margin: A = 11.2, B₀ = 50.7 (say A = 11.5, B₀ = 52 with rounding). This changes Hhat (10.5→11.5, 48→52), marginTilde's baked numbers, and re-runs the base-point certification + the margin convexity (D-057's proof is structural — the constants A/B₀ enter as parameters? Let me check: marginTilde's def has 10.5 and 48 HARDCODED (line: `(2 / 3) * C0hat T + 10.5 * Real.log (T + 2) + 48`). Changing them touches: marginTilde_convex (proved in session 011 — the 8-block ψ-table with specific constants!), sInfty_lower_bound (no), LiBasePoints (the certified interval bounds margiñ(8×10⁴) ≥ 8001, margiñ(10⁵) ≥ 85501 — the CERTIFIED numbers would drop ~5–10% but remain positive), lambda_pos_finite_height_verified (the assembly — constant-agnostic if the hypotheses are about marginTilde). The convexity proof (session 011) used specific numeric constants — its IIMaj″ ≤ 1.316 < 2 bound and the ψ-table blocks — would need re-verification with 11.5/52. The paper's §3 has the 10.5/48 trail in text (margin trail footnote) — frozen until ii′-7, but at ii′-7 the paper's appendix gets updated anyway. The COST: re-verify convexity + re-certify base points + paper text touch at ii′-7. The GAIN: honesty (the current 10.5/48 traced assembly is unprovable as it stands).\n\n(C) Hmm — wait. Actually, let me reconsider. Is there a way to keep 10.5/48 by being smarter about the near window in piece 2? The near sum Σ_{|γ−t|<1} 1/|s₀−ρ|: split into |γ−t| ≤ 1/2 and 1/2 < |γ−t| < 1... no — count issue remains.\n\nHmm, actually — WAIT. What about the reference point trick applied differently: instead of bounding Σ_near 1/|s₀−ρ| ≤ count (each term ≤ 1), note that this sum is part of the DIFFERENCE and could be paired with... no, it's a standalone absolute bound.\n\nActually actually actually. Hold on. Let me recompute the two-unit count bound more carefully. The honest two-unit count: N(t+1) − N(t−1) — but for the MULT-weighted near sum we need Σ_{|γ−t|<1} m. Via the perimeter (mult-weighted ZeroCountProp): window counts for (t−1, t] and (t, t+1): Σ ≤ C0hat(t) + C0hat(t+1) ≤ 2·C0hat(t+1). With C0hat(t+1) = 0.433 log(t+3) + 0.886 loglog(t+3) + 2.9.\n\nSo piece 2 ≤ 2·C0hat(t+1). And piece 3's per-interval counts: left intervals (t−k−1, t−k]: ≤ C0hat(t−k+1) ≤ C0hat(t); right intervals (t+k, t+k+1]: ≤ C0hat(t+k+1) ≤ C0hat(2t+1) for k ≤ t. Etc. The full honest fold will give ≈ 14.73·C0hat(t+1) + 7.97 ≤ 6.38L + 13.05LL + 50.7 (L = log(t+3)-ish). vs target 10.5 log(|t|+2) + 48. At t=10: honest ≈ 6.38·2.56 + 13.05·0.94 + 50.7 = 16.3+12.3+50.7 = 79.3 vs target 74.0. Exceeds. So (A) [tightening] would need to save ~5.3+ at t=10 and the LL/L terms at ∞ — from piece 3's √2 slack (up to 29% of 12.73·C₀ ≈ 3.7·C₀ ≈ 18–25 at these heights) — actually the available slack in piece 3 IS enough if fully harvested: 12.73·C₀+7.06 → ~9.2·C₀+const would save 3.5·C₀ ≈ 17+. But harvesting the √2 slack requires the per-interval sum Σ 1/(k√(1+k²)) ≈ 1.32 vs 1 — wait that's WORSE per unit... I'm confusing myself. Let me just compute D-056's piece-3 exactly vs the sharpened version:\n\nD-056: term ≤ 4.5√2/(x(1+x)), x = |t−γ|; per interval k ≤ x < k+1: ≤ 4.5√2/(k(k+1)). Two-sided Σ ≤ 4.5√2·[C₀·Σ_{k=1}^{~t} 1/(k(k+1)) (left) + C₀(2t)·Σ (right) + tail] ≈ 6.364·[C₀·1 + C₀(2t)·1 + 0.53].\n\nSharpened: term = 4.5/(x√(1+x²)) ≤ 4.5/(k·√(1+k²)) on the interval... but WAIT — x ≥ k gives 1/(x√(1+x²)) ≤ 1/(k√(1+k²)) ✓. Σ_{k≥1} 1/(k√(1+k²)) ≈ 1.32 (computed above) vs Σ 1/(k(k+1)) = 1. So per-interval sharpened: 4.5·1.32 = 5.94 vs D-056's 6.364·1 = 6.364 per side. Saves ~7%. Total piece 3: 5.94·[2C₀ + 1.11] ≈ 11.88·C₀ + 6.6 vs 12.73·C₀ + 7.06. Saves 0.85·C₀ + 0.5 ≈ 5–6.5 at these heights. New total: 0.57 + 2C₀ + 11.88C₀ + 6.6 + 0.38 = 13.88·C₀ + 7.55 ≤ 13.88·(0.433L + 0.886LL + 2.9) + 7.55 = 6.01L + 12.3LL + 40.3 + 7.55 = 6.01L + 12.3LL + 47.8 ≤ (6.01 + 12.3/e)L + 47.8 = (6.01+4.52)L + 47.8 = 10.53L + 47.8. vs 10.5L + 48 — 10.53 > 10.5 STILL breaks (barely!). Hmm. And at t=10: 6.01·2.56+12.3·0.94+47.8 = 15.4+11.6+47.8 = 74.8 vs 74.0 — still barely over. GRRR.\n\nMore tightening? The per-interval count on the LEFT at interval k is C₀(t−k+1) ≤ C₀(t) — could weight: Σ_k C₀(t−k)/(k√(1+k²)) — for small k (dominant terms), C₀(t−k) ≈ C₀(t); savings negligible. The 4.5 factor (σ = −5/2): if the R-bound's σ range is actually only used on [−5/2, 3]... what if we split: for σ ∈ [−3/2, 3], |s₀−s| ≤ 3.5; the σ ∈ [−5/2, −3/2] strip handled via FE-reflection (5d machinery) with its own constants? That's a different proof structure — D-056 chose the direct route precisely to avoid that. Hmm.\n\nHonestly, the cleanest is (B): re-fold with honest constants A = 11.5, B₀ = 52 (round up from 11.18/50.7 with margin) — or even A = 12, B₀ = 55 for comfort — and re-verify the downstream. Let me quantify the downstream impact:\n\nThe R-bound enters the margin via the H-majorant on the contour: Hhat T = 3·C0hat² + A·log(T+2) + B₀. The margin's B-side: 4T·((2/3)·C0hat + A·log + B₀) + 2(e⁴+1)(7·Hhat + 3.3) + ... The leading √n log n coefficient: from D-056 §3: 4·(0.1443 + A/2). A: 10.5 → 11.5: coefficient 21.6 → 23.6 (+9%). Margin at n = 10⁵: measured margin(10⁵) ≈ 9.3×10⁴ (D-056 §3); the B-side grows by ~4·√n·(ΔA/2)·log n ≈ 4·316·0.5·11.5 ≈ 7272... hmm that's ~8% of 9.3×10⁴. New margin(10⁵) ≈ 8.6×10⁴ — still hugely positive. N₀ crossover: was ~32 871 traced / N₀ adopted 80 000 — with the bigger B-side the crossover moves up maybe 10–20%: ~40 000; adopted N₀ = 80 000 still covers it (and the certified base points margiñ(8×10⁴) ≥ 8001 would become ~... the 8001 was the certified lower bound with the OLD constants; with new constants the margin drops ~8%: ~7300 — still positive ✓ but the CERTIFIED interval proof (LiBasePoints) is constant-specific and would need re-running. The convexity proof (D-057, session 011 Lean) is structural but has baked numeric comparisons (1.316 < 2 etc.) that shift slightly — need re-checking. The paper §3 text has the constants (frozen until ii′-7).\n\nCost estimate for (B): LiSkeleton constant edits + re-run session-011 convexity proof (may need block re-tuning) + LiBasePoints re-certification + paper text at ii′-7. ~1–2 sessions of rework, all mechanical.\n\nCost estimate for (A) [fully tighten to keep 10.5/48]: the piece-3 sharpening to per-interval 1/(k√(1+k²)) sums (the Σ = 1.32 constant needs a Lean-provable closed form — a digamma/trig value or an integral bound) + MORE sharpening elsewhere (~0.03·L + small constants — very tight) — likely fails without a structurally different route (FE-reflection split). Risky, multi-session, and even then 10.53 vs 10.5 is knife-edge — likely impossible with this assembly shape.\n\nThere's also (D): pick the near window SMARTER — define R(s) with the near sum over |γ−t| < 1 but split the count as C₀(t−1)+C₀(t) ≤ 2C₀(t)... no saving.\n\nHmm — hmm, hold on, wait. Let me reconsider option (A) once more, because there might be more slack in piece 2 itself: Σ_{|γ−t|<1} 1/|s₀−ρ| with |s₀−ρ| = √((2−β)² + (t−γ)²) ≥ √(1 + (t−γ)²). The terms with |t−γ| near 1 contribute ≤ 1/√2. Per-interval sharpening on the NEAR sum: |t−γ| ≤ 1/2: count ≤ C₀(t) (one unit window (t−1/2, t+1/2] ⊂ ... hmm — (t−1/2, t+1/2] is a unit window ✓ count ≤ C₀(t)); per-term ≤ 1. Outer: 1/2 < |t−γ| < 1: two half-unit windows ⊂ two unit windows; count ≤ 2·C₀(t) − [inner overlap]... honestly ≤ 2C₀(t); per-term ≤ 1/√(1.25) = 0.894. Total: C₀ + 0.894·2C₀ = 2.79·C₀ — worse than the straight 2C₀. The straight 2C₀ is better. OK.\n\nWhat about |s₀−ρ| ≥ √(1+x²) per interval in the OUTER annulus: x ∈ (1/2, 1): per-term ≤ 1/√(1+1/4) = 0.894 — same. No.\n\nSo piece 2 honest = 2·C₀(t) is optimal with the Trudgian input. TOTAL honest minimum ≈ 13.88·C₀ + 7.55 ≈ 10.53·L + 47.8 — JUST over 10.5/48. The 10.5/48 constants are genuinely unprovable from this assembly shape (they were derived FROM the faulty one-C₀ piece 2). \n\nWait, actually — one more idea for (A): the digamma-difference piece 6 (0.29) and pieces 4–5 (0.045 each) and piece 1 (0.57) have slack: piece 1's Z₂ = 0.57 is exact-ish. Constants: 0.57 + 7.06 + 0.09 + 0.29 = 8.01 vs the folded 7.97 + ... The L-side: 13.88·0.433 = 6.01. To hit 10.5: need 6.01 + 12.3/e ≤ 10.5 ⟺ 6.01 + 4.524 = 10.534 > 10.5. Off by 0.034·L. The loglog fold loglog u ≤ (1/e)·log u is lossy for small u... at t=10: loglog(12) = 0.91 vs (1/e)log(12) = 0.914 — nearly tight there. Alternatively fold loglog ≤ c·log with a better constant on a restricted range? loglog u ≤ (1/e) log u is exact-optimal globally (equality at u = e^e). At u = t+2 = 12: LL/L = 0.91/2.48 = 0.367 vs 1/e = 0.368. No gain.\n\nReduce piece 3's per-interval sum constant: Σ 1/(k√(1+k²)) — could push the first interval's exact value: k=1: 1/√2 = 0.7071; the D-056 form gives 1/(1·2) = 0.5 — wait, D-056's per-interval bound 4.5√2/(k(k+1)) at k=1: 4.5·1.414/2 = 3.182; sharpened: 4.5·0.7071 = 3.182 — SAME (equality at k=1: √2/(1·2) = 1/√2 ✓). At k=2: D-056: 4.5√2/6 = 1.0607; sharpened: 4.5/(2√5) = 1.0062. Sum over k of the ratio → the 7% computed. To do better, use the EXACT term 4.5/(x√(1+x²)) with x per-interval lower bound k: already did. Use x·(1+x²)^{1/2} ≥ (k+1)/... no, lower bound is k. Alternatively parametrize intervals by midpoints? Diminishing.\n\nThe real slack: the right-side intervals use C₀(2t) (count up to height 2t) — C₀(2t) ≈ C₀(t) + 0.433·log 2 ≈ C₀(t) + 0.30. And the tail 0.53. Piece 3 total ≈ 4.5·1.32·(2C₀ + 0.3 + 0.53)-ish. Fine.\n\nSo: honest best ≈ 10.53L + 47.8 vs baked 10.5L + 48. SO CLOSE. But over. And any further tightening (0.03·L ≈ 0.08 at t=10) is within the rounding noise of these estimates — it might actually fit with fully careful bookkeeping! E.g., piece 3's tail 0.53 → sharper; the C₀(2t) ≤ C₀(t)+0.58 → +0.30 actual; pieces 4–6 exact: 0.045+0.045+0.29 → maybe 0.30 total; Z₂ = 0.57 → 0.56996. Marginal gains ≈ 0.2–0.3 — comparable to the 0.08–0.5 gap. NOT robust. Knife-edge. Not the way.\n\nDECISION LEAN: (B) re-fold with honest constants. But this has real downstream cost and touches baked constants — ANOTHER user decision point. OR — actually, wait. Let me reconsider the whole thing once more.\n\nHmm — hold on. Let me re-examine D-056's piece 2 once more. \"2. Near at s₀: |s₀−ρ| ≥ 2 − β ≥ 1 ⟹ Σ_{|γ−t|<1} 1/|s₀−ρ| ≤ C₀(t).\"\n\nHmm wait — what if the intended reading is that C₀(t) denotes the count of |γ−t|≤1 throughout D-056 (a DIFFERENT C₀ than D-036's)? D-056 says \"The zero-count input is the HONEST Trudgian form (D-036 §0 erratum): C₀(t) := F(t+1)−F(t) + S_b(t+1) + S_b(t)\". F(t+1)−F(t) is the one-unit F-difference. So C₀(t) is the one-unit count. UNLESS F(t+1)−F(t) is a typo for F(t+1)−F(t−1)... As computed, the closed form 0.433 log + 0.886 loglog + 2.9 matches the ONE-unit honest count (0.159+0.274 = 0.433 ✓). So D-056's C₀ = one-unit count, and piece 2's use for the two-unit window is a genuine gap. CONFIRMED.\n\nAlso D-036 §2's H(T): \"|ζ′/ζ(s)| ≤ C₀(T)/d_min + A log + B₀ ≤ 3C₀(T)² + A log + B₀\" — the near sum at height T: count(C₀(T)) × clearance(1/d_min = 3C₀(√n+1)) — TWO gaps: (i) count should be the two/three-unit count (the |γ−T|<1 window with T ∈ [√n, √n+1] spans (T−1, T+1) ⊂ (√n−1, √n+2) — THREE unit windows, or two if T-centered... T ∈ [√n, √n+1] ⟹ (T−1, T+1) ⊂ (√n−1, √n+2) — 3 units! unless the window is |γ−T|<1 ∩ wherever); (ii) the clearance d_min is only against window zeros — zeros in (√n+1, √n+2) have no clearance guarantee. Hmm — but wait: actually the pigeonhole as implemented in ii′-4 (exists_zero_avoiding_T) gives clearance 1/(3·C0hat(a+1)) vs zeros in [a, a+1] only. For the H(T) bound we need clearance vs ALL zeros with |γ−T|<1. A zero at γ = a+1+ε (just above the window): |γ−T| ≥ γ−T > (a+1)−T ≥ 0 — can be < 1/(3C₀)! E.g. T = a+0.9, γ = a+1.05: |γ−T| = 0.15 < 1/(3·5) = 0.067? 0.15 > 0.067 OK — but γ = a+1.02, T = a+0.98: |γ−T| = 0.04 < 0.067. So yes, an out-of-window zero CAN be closer than the clearance. GAP in the D-036 H(T) derivation as well (this is ii′-6 territory, not 5f — but the SAME C0hat²-accounting feeds Hhat which is baked in marginTilde).\n\nHmm — OK wait, but this one has an easy honest fix: apply the pigeonhole to the EXTENDED window [a−1, a+2] (three unit windows, count ≤ 3·C0hat): get T ∈ [a, a+1]... no — the midpoint pigeonhole on [a−1, a+2] with 3·C0hat zeros gives a gap of length ≥ 3/(3C₀+1) — T at the center of a sub-gap within [a, a+1]... the gaps within [a, a+1] that are far from out-of-window zeros: choose T ∈ [a, a+1] avoiding ALL zeros in (a−1, a+2) by 1/(9C₀)-ish (pigeonhole with 3C₀ zeros in the 3-unit window — midpoints in [a, a+1]... need the midpoint grid within [a, a+1] with ≥ 3C₀+1 points ⟹ spacing 1/(3C₀+1) ⟹ clearance 1/(6C₀+2)...). Anyway: honest clearance 1/(c·C₀) vs all |γ−T|<1 zeros, count ≤ 3C₀ ⟹ near sum ≤ 3c·C₀² vs the baked 3·C₀². With c = 6–9: 18–27·C₀² vs baked 3·C₀². Hhat's 3·C0hat² would become ~18–27·C0hat². That's a 6–9× increase in the (log T)⁴-ish term of the margin B-side... The margin's C0hat² term: 2(e⁴+1)·7·3·C0hat² ≈ 2·55.6·7·3·(0.433L+..)² ≈ 2335·(0.433L+0.886LL+2.9)². At n = 10⁵ (T ≈ 317): C0hat ≈ 0.433·5.76+0.886·1.75+2.9 ≈ 2.49+1.55+2.9 = 6.94; C0hat² ≈ 48.2; ×2335 ≈ 112 600 — hmm that's COMPARABLE to the margin 9.3×10⁴! Increasing the C0hat² coefficient 6× would add ~5.6×10⁵ to the B-side — EXCEEDING the margin at 10⁵?! Let me recompute the margin formula: margiñ(n) = S(n) − B̃(n) + 1 where the B-side includes `2 * (Real.exp 4 + 1) * (7 * Hhat T + 3.3)`. Hhat T = 3·C0hat² + 10.5·log(T+2) + 48. At T = √n+1, n = 10⁵: T ≈ 317.2, C0hat(317.2) ≈ 0.433·log(319.2) + 0.886·loglog(319.2) + 2.9 = 0.433·5.766 + 0.886·1.752 + 2.9 = 2.497 + 1.552 + 2.9 = 6.95. 3·C0hat² = 3·48.3 = 144.9. 10.5·log(319.2) = 60.5. Hhat ≈ 144.9+60.5+48 = 253.4. 7·Hhat+3.3 ≈ 1777. ×2·(e⁴+1) = 2·55.6 = 111.2: ≈ 197 600. Hmm — and the margin at 10⁵ is 9.3×10⁴?!? That means the B-side's horizontal-integral term ALONE (197 600) exceeds... wait, margin(10⁵) = S(10⁵) − B(10⁵) + 1 ≈ 9.3×10⁴ requires B(10⁵) ≈ S(10⁵) − 9.3×10⁴. S(n) ≈ (n/2)·log n + (c₁−γ/2)·n − 4 ≈ 0.5·10⁵·11.51 + (0.0231)·10⁵ ≈ 575 650 + 2310 ≈ 578 000. B-side: 2FT + 4T((2/3)C₀ + 10.5 log + 48) + 40·1.3352 + 2(e⁴+1)(7H+3.3) + IIMaj + 1: 2FT ≈ 2·(317/6.28·log(317/6.28))·... F(317) ≈ (317/6.28)·log(50.5) − 50.5 + 0.875 ≈ 50.5·3.92 − 49.6 ≈ 148.4; 2F·T ≈ 2·148.4·317 ≈ 94 100. 4T((2/3)·6.95 + 60.5 + 48) = 4·317·113.1 ≈ 143 400. The (e⁴+1) term ≈ 197 600. 40·1.3352 ≈ 53. IIMaj tiny. Total B ≈ 94 100 + 143 400 + 197 600 + 53 ≈ 435 200. Margin ≈ 578 000 − 435 200 ≈ 142 800. Hmm — I misremembered 9.3×10⁴ (that was margin at a different n or with different constants; D-056 §3 says margin(10⁵) = 9.3×10⁴ — close enough order). Anyway the C0hat²-piece of B at 10⁵ is ~2(e⁴+1)·7·3·48.3 ≈ 111.2·7·144.9/7... let me just: 2(e⁴+1)·(7·Hhat) with Hhat's C0hat² part = 144.9: 111.2·7·144.9 ≈ 112 800. If C0hat²'s coefficient triples (3→18): 111.2·7·869 ≈ 676 000 — EXCEEDS the entire margin! So an 18·C0hat² Hhat would DESTROY the margin at 10⁵ (B-side ≈ 1M > S ≈ 578K). Whoa.\n\nHmm wait, so how did the original assembly survive with 3·C0hat²? Because the near sum's count×clearance = C₀·3C₀ = 3C₀² — the one-unit count convention AND the window-only clearance. The honest accounting (3-unit count 3C₀, full-neighborhood clearance 1/(6–9C₀)) gives 18–27·C₀². The margin survives only if the C0hat² coefficient stays ≤ ~6-ish. Let me see what's actually provable:\n\nNear sum ≤ count × clearance. Honest count for |γ−T|<1 with T ∈ [a, a+1]: (T−1, T+1) ⊂ (a−1, a+2): 3 units ⟹ 3·C0hat(a+2). Honest clearance: extend the pigeonhole — the midpoint pigeonhole over [a, a+1] against ALL zeros in (a−1, a+2): ≤ 3C₀ zeros; place ⌈3C₀⌉+1 midpoints in [a+1/4, a+3/4] (say) with spacing ≥ (1/2)/(3C₀) ⟹ clearance ≥ (1/4)/(3C₀+1)-ish ≥ 1/(13·C₀)-ish. Then near sum ≤ 3C₀ · 13C₀ = 39·C₀². vs baked 3·C₀². 13× WORSE. The margin dies (as computed: 13×112 800 ≈ 1.5M > margin).\n\nUNLESS the clearance/count split is smarter: Cauchy-Schwarz? Σ 1/|T−γ| over the near zeros — with the pigeonhole giving clearance d vs ALL near zeros, Σ ≤ count/d. Alternatively use the EXPLICIT sum structure: Σ_{|γ−T|<1} 1/|T−γ| — the zeros are 1D points; if T has clearance d from ALL zeros and the count in each unit sub-window is ≤ C₀, then Σ 1/|T−γ| ≤ count(|γ−T|<d... none) + Σ over dyadic shells d ≤ |γ−T| < 1: shell [2^{-j}, 2^{-j+1}) has count ≤ 2·2^{-j+1}-unit windows... Σ ≤ Σ_j C₀·2^j·(shell width 2^{-j+1} → count ≤ C₀·(2 windows per shell...)) — hmm: shell {2^{-j} ≤ |γ−T| < 2^{-j+1}} has width 2^{-j+2}, count ≤ 2^{-j+2}·C₀ per unit... count ≤ C₀·2^{-j+2}/1 = C₀·2^{-j+2} windows?? — no: count per UNIT window ≤ C₀; shell width w = 2^{-j+2} units... for j ≥ 2 the shell is < 1 unit wide: count ≤ C₀ (one window covers it). Σ_j: shells j=1..~log(1/d): count_j ≤ C₀ (each shell ⊂ 1–2 unit windows); per-term ≤ 2^j. So Σ ≤ Σ_{j=1}^{J} C₀·2^j ≈ C₀·2^{J+1} = C₀·(2/d). With d = 1/(3C₀): Σ ≤ 6·C₀². Hmm — 6C₀², better than 39 but still 2× the baked 3C₀². Actually more carefully: Σ_{|γ−T|<1} 1/|T−γ|: split at 1/2: inner |γ−T|<1/2 ⊂ one unit window: count ≤ C₀; terms ≤ 1/d ≤ 3C₀... inner ≤ C₀·3C₀ = 3C₀². Outer 1/2 ≤ |γ−T| < 1: terms ≤ 2; count ≤ 2C₀ (two windows): outer ≤ 4C₀. Total ≤ 3C₀² + 4C₀ — CLOSE to the baked 3C₀²! The extra 4C₀ is lower-order (C₀ vs C₀²). So the near sum ≤ 3·C₀² + 4·C₀ honestly IF the clearance d = 1/(3C₀) holds against ALL zeros within distance 1/2 of T (i.e., the pigeonhole must cover (T−1/2, T+1/2) ⊂ (a−1, a+2)... — extend L3: pigeonhole on the 3-unit window (a−1, a+2) (count ≤ 3C₀) with midpoints in [a, a+1]... hmm, the midpoint spacing: window [a, a+1], 3C₀ forbidden points (the zeros in (a−1, a+2) — wait we only need clearance vs zeros in (T−1/2, T+1/2) ⊂ (a−1/2, a+3/2) since T ∈ [a, a+1]: zeros in (a−1/2, a+3/2): count ≤ 2C₀. Pigeonhole: 2C₀+1 midpoints in [a, a+1] at spacing 1/(2C₀+1), each zero blocks ≤ 1 midpoint ⟹ a midpoint T with clearance ≥ 1/(2(2C₀+1)) ≥ 1/(6C₀) from all zeros within (a−1/2, a+3/2). Then near sum: inner |γ−T| < 1/2 (all such zeros are in the clearance range): count ≤ C₀(2 units... (T−1/2, T+1/2) = 1 unit ✓ ≤ C₀); terms ≤ 6C₀ ⟹ ≤ 6C₀². Outer: 1/2≤|γ−T|<1: count ≤ 2C₀, terms ≤ 2 ⟹ ≤ 4C₀. Total ≤ 6C₀² + 4C₀. vs baked 3C₀²: 2× + lower order. Margin impact: the C0hat² coefficient doubles: 112 800 → 225 600 extra at n=10⁵: B-side +112 800 — margin 142 800 → 30 000 — SURVIVES (barely, and the crossover N₀ moves up, maybe past 80 000?!). Ugh — actually the margin at the certified base point 8×10⁴ was ≥ 8001 with the old constants; doubling the C0hat² term would flip it negative... \n\nOK. This is all ii′-6 territory (the H(T)/contour assembly), NOT 5f. Let me SCOPE BACK to 5f: the R-bound |R(s)| ≤ 10.5 log(|t|+2) + 48 for σ ∈ [−5/2, 3], |t| ≥ 10. The ONLY count input is piece 2 (2× gap) + piece 3 (per-interval, honest as written). Honest fold: 14.73·C₀ + 7.97 ≤ 11.18·L + 50.7 (vs baked 10.5/48). With piece-3 sharpening (per-interval 1/(k√(1+k²))): 13.88·C₀ + 7.55 ≤ 10.53·L + 47.8 — STILL barely over 10.5/48.\n\nSo for 5f, the honest options:\n(B1) Prove the R-bound with honest constants A = 11.5, B₀ = 52 (comfortable rounding of 11.18/50.7) and re-fold downstream (margin constants change: Hhat's 10.5/48 → 11.5/52; the 3C0hat² stays as-is for now — its own honesty issue is ii′-6's to face). Downstream cost: marginTilde def constants, convexity re-verification, base-point re-certification, paper text at ii′-7. AND the margin at 8×10⁴/10⁵ must be re-checked (impact ~5–8% — survives per my estimates, but the CERTIFIED proofs need re-running).\n\n(B2) Prove a sharper assembly that fits 10.5/48 — appears knife-edge/impossible with this shape.\n\nHmm hold on, wait. Before spiraling further, let me double-check the D-056 piece-2 claim by looking at what E-028 actually verified and what the paper's §3 (R-004 assembly) uses. If E-028's V-R verified |R(s)| ≤ 10.5 log + 48 numerically (26× slack), the BOUND is fine — it's the traced PROOF that's gappy. For the Lean 5f, I need a PROOF. The cleanest provable-from-assembly statement has the honest constants.\n\nHmm — actually, WAIT. One more idea for keeping 10.5/48 exactly: the reference-point difference for the NEAR sum doesn't need to bound Σ_near 1/|s₀−ρ| by the count — the near sum at s₀ can be paired with the far difference at the SAME zeros? No — the split is near vs far, disjoint.\n\nAlternatively: sharpen piece 2 using the per-term √(1+x²): Σ_{|γ−t|<1} 1/√(1+(t−γ)²): inner |t−γ| ≤ 1/2: ≤ C₀(t)·1; outer 1/2<|t−γ|<1: count ≤ 2C₀ − hmm. ≤ C₀(t) + 0.894·(2C₀(t) − ...) — the outer annulus (1/2,1) count is ≤ 2C₀(t) (two windows) minus nothing provable. 2.79·C₀ — worse.\n\nWhat about THREE-way split: |t−γ| ≤ 1/2 (≤ C₀, ×1), 1/2 < |t−γ| ≤ 3/4... the count of the annulus (1/2, 3/4]: ⊂ (t−3/4, t+3/4] — 1.5 units — count ≤ 2C₀... ugh, the annuli counts don't sharpen below 2C₀ for the two-sided window. FUNDAMENTAL: the two-sided near window count is 2·C₀·(1+o(1))-ish — no, wait, is it? (t−1, t+1] = two unit windows = 2·C₀(t) with C₀(t) ≈ 5. True count ≈ 2·(average density) ≈ 2·(log t)/2π·... the Trudgian bound per unit is C₀ ≈ 5 (vs true ~1.1 at t=50) — the SLACK is in the S_b constants (Trudgian's S bound is uniform, not tight per-window). The two-unit honest count is 2·C₀ − (F-overlap...) ≈ 2·C₀ − 2.6 (the constant 2.9 is per-window... C₀(t) = 0.433L + 0.886LL + 2.9; two-unit = F(t+1)−F(t−1) + S(t+1)+S(t−1) ≤ 0.318L + 0.886LL + (3.176 − ...) hmm: S_b pair for two-unit = S(t+1)+S(t−1) = 0.137(2 log t) + 0.443(2 loglog t) + 3.176 = 0.274L + 0.886LL + 3.176. F-diff-2unit = (1/π)L + c ≈ 0.318L. Total ≈ 0.592L + 0.886LL + 3.176−ish. vs 2·C₀ = 0.866L + 1.772LL + 5.8. So the honest two-unit count (0.592L + 0.886LL + 3.2) is MUCH better than 2·C₀ (0.866L + 1.77LL + 5.8)!! Because the F-difference over 2 units only doubles the 0.159 coefficient, while C₀'s constant 2.9 and LL 0.886 don't double in the honest form!! \n\nRECOMPUTE piece 2 with the honest two-unit Trudgian form: piece 2 ≤ N(t+1)−N(t−1) ≤ [F(t+1)−F(t−1)] + S_b(t+1)+S_b(t−1) ≤ (0.318·L + 0.886·LL + 3.176 + small) where L = log(t+2)-ish. Hmm — but our LEAN perimeter is ZeroCountProp with C0hat — the mult-weighted UNIT-window count ≤ C0hat(t+1). The two-unit count via the perimeter = C0hat(t) + C0hat(t+1) ≤ 2·C0hat(t+1) — we DON'T have the honest F/S-pair two-unit form in Lean (the perimeter is the closed-form C0hat, not the F/S-pair). The closed form 2·C0hat(t+1) = 0.866L + 1.77LL + 5.8. Piece 2 ≤ 2·C0hat(t+1).\n\nFold with piece 3 sharpened (11.88·C₀ + 6.6): total = 0.57 + 2C₀ + 11.88C₀ + 6.6 + 0.38 ≈ 13.88·C₀ + 7.55. With C₀ = C0hat(t+1) = 0.433L' + 0.886LL' + 2.9, L' = log(t+3): ≤ 6.01L' + 12.3LL' + 40.3 + 7.55 = 6.01L' + 12.3LL' + 47.85. ≤ (6.01 + 12.3/e)L' + 47.85 = 10.53·L' + 47.85. The target: 10.5·log(|t|+2) + 48. L' = log(t+3) > log(t+2) — slight overshoot both sides. 10.53 > 10.5: BREAKS by 0.03·L + (47.85 + 10.53·log((t+3)/(t+2)) − 48) ≈ 0.03L + 0.1. Knife-edge negative.\n\nTo close the last 0.03·L + 0.1: piece 3's tail 0.53 → exact ~0.3?; C₀(2t) ≤ C₀+0.58 → +0.3; pieces 4–6: 0.045+0.045+0.29 = 0.38 → could sharpen to ~0.2; Z₂ = 0.57 → 0.56997. Piece 3's Σ constant 1.32 → exact ≈ 1.316? (Σ 1/(k√(1+k²)) — numerically: k=1: 0.70711, k=2: 0.22361, k=3: 0.10541, k=4: 0.06063, k=5: 0.03922, k=6: 0.02774, k=7: 0.02058, k=8: 0.01578, k=9: 0.01249, k=10: 0.01010, Σ_{k>10} ≤ ∫_10^∞ dx/x² = 0.1: total ≈ 1.3225 + ... let me sum: 0.70711+0.22361 = 0.93072; +0.10541 = 1.03613; +0.06063 = 1.09676; +0.03922 = 1.13598; +0.02774 = 1.16372; +0.02058 = 1.18430; +0.01578 = 1.20008; +0.01249 = 1.21257; +0.01010 = 1.22267; tail Σ_{k≥11} 1/(k√(1+k²)) ≤ Σ 1/k² ≤ 1/10 = 0.1 → ≈ 1.32267+... hmm ≈ 1.32. And 4.5·1.32 = 5.94/side.\n\nTotal constant: 0.56997 + 5.94·(2·0.58+0.53)... this is getting extremely fiddly. The gap is 0.03·L + ~0.15 — honestly too tight to close robustly without redoing the whole assembly at higher precision. And EVEN IF closed, it leaves ii′-6's H(T) near-sum issue (the 3C₀² clearance/count problem — which is a SEPARATE, bigger honesty gap that WILL need facing at ii′-6 and likely moves the constants anyway!).\n\nSTEPPING BACK. Strategic view: the 10.5/48 constants came from D-056's assembly which has the one-C₀-piece-2 gap. The margin constants baked in LiSkeleton inherit from that. The honest re-fold moves A from 10.5 to ~11.2–11.5 and B₀ from 48 to ~51–52 (or a bit more with room). The margin has ~25× slack at the theorem level (E-028) but the CERTIFIED Lean artifacts (convexity proof, base-point bounds) are constant-specific and will need re-verification. That's the honest cost of a genuine fix — and it SHOULD be done now (at 5f) rather than at ii′-6, because 5f is where the R-bound constants enter Lean.\n\nBUT — the ii′-6 H(T) issue (3C₀² → 6C₀²+ clearance coverage) will move the constants AGAIN. If I re-fold now for 5f and again at ii′-6, double rework. ALTERNATIVE: face BOTH issues now — i.e., design 5f + the ii′-6 contour assembly constants together, re-fold ONCE.\n\nHmm, wait — is the ii′-6 issue real? Let me double check the H(T) near-sum against the ii′-4 L3 statement. exists_zero_avoiding_T: T ∈ [a, a+1], clearance 1/(3·C0hat(a+1)) vs zeros with im ∈ [a, a+1]. The horizontal contour at height T: near sum Σ_{|γ−T|<1} 1/|s−ρ|, |s−ρ| ≥ |T−γ|. Zeros with γ ∈ (a+1, a+2) and |γ−T|<1: clearance NOT covered by L3. So the H(T) bound C₀/d_min is NOT justified as stated. The honest version needs clearance vs all |γ−T|<1 zeros: extend the pigeonhole to the 3-unit window (count 3C₀, clearance 1/(9C₀+3)-ish → near sum ≤ 3C₀·(9C₀+3) ≈ 27C₀²) OR the smarter split (≤ 6C₀² + 4C₀ as computed). Either way Hhat's 3·C0hat² is undercounted.\n\nHmm wait, actually — one clean fix for the clearance: choose T in [a+1/4, a+3/4] (the central half) via the pigeonhole on the FULL window [a, a+1]... no: out-of-window zeros sit just outside a or a+1: γ = a − ε or a+1+ε; T ∈ [a+1/4, a+3/4] ⟹ |T−γ| ≥ 1/4 − ... γ > a+1: |T−γ| > (a+1) − T ≥ 1/4. γ < a: |T−γ| > T − a ≥ 1/4. So out-of-window zeros are ≥ 1/4 away if T is in the central half! And in-window zeros: clearance 1/(3C₀) via the pigeonhole (needs the pigeonhole to place T in the central half: use ~2C₀+1 midpoints in [a+1/4, a+3/4]: spacing (1/2)/(2C₀+1)... hmm — the pigeonhole: k zeros in window, k+1 midpoints in [a+1/4, a+3/4] spaced 1/(2(k+1)) apart, each zero blocks ≤ 1 ⟹ T with clearance 1/(4(k+1)) ≥ 1/(4(C₀+1)) ≥ 1/(5C₀)... Combined clearance vs ALL zeros: min(1/(5C₀), 1/4) = 1/(5C₀) (C₀ ≥ 2). Near sum: inner |γ−T| < 1/2: count ≤ C₀ (1 unit); terms ≤ 5C₀ ⟹ ≤ 5C₀². Outer 1/2 ≤ |γ−T| < 1: count ≤ 2C₀, terms ≤ 2 ⟹ ≤ 4C₀. Total ≤ 5C₀² + 4C₀. vs baked 3C₀²: coefficient 5 vs 3 (+67% on the C0hat² term) + 4C₀ lower-order.\n\nMargin impact at n = 10⁵: the C0hat² term in B: 2(e⁴+1)·7·(5·48.3) vs (3·48.3): 111.2·7·2·48.3 = +75 200 extra ⟹ margin 142 800 → ~67 600 — SURVIVES. At n = 8×10⁴ (T ≈ 283.8): C0hat(284.8) ≈ 0.433·5.65+0.886·1.73+2.9 ≈ 2.45+1.53+2.9 = 6.88; C0hat² ≈ 47.3; extra 2·47.3·111.2·7 ≈ ... the increment is 2(e⁴+1)·7·2·C0hat² ≈ 1556.8·47.3 ≈ 73 600. Old margiñ(8×10⁴) ≥ 8001 certified (true ~15 764 per the margin trail). 15 764 − 73 600 < 0?!? Hmm wait — that can't be right. Let me recompute the C0hat²-piece at 8×10⁴ with the OLD constants: 111.2·7·3·47.3 ≈ 110 400. But the total B-side at 8×10⁴ was ≈ S − margin ≈ ... margin(8×10⁴) ≈ 15 764 (true) — S(8×10⁴) ≈ 0.5·80000·11.29 + 0.0231·80000 ≈ 451 600 + 1850 ≈ 453 450; B ≈ 437 700. The C0hat² piece 110 400 is 25% of B. Doubling adds 73 600 ⟹ B ≈ 511 300 > S ≈ 453 450 — MARGIN NEGATIVE at 8×10⁴. The crossover moves WAY up (maybe n ~ 2×10⁵?). And N₀ is capped by the finite verification 5×10⁵... margin at 5×10⁵ was 2.0×10⁶ — with the extra ~2·C0hat²·778: at n = 5×10⁵, T ≈ 708: C0hat ≈ 0.433·6.56+0.886·1.88+2.9 ≈ 2.84+1.67+2.9 = 7.41; C0hat² ≈ 54.9; extra ≈ 1556.8·... wait the increment coefficient: 2(e⁴+1)·7·(5−3)·C0hat² = 111.2·14·54.9 ≈ 85 500. margin(5×10⁵) = 2.0×10⁶ − 85 500 ≈ 1.9M ✓ fine. The crossover: where does margin become positive? B's leading √n log n grows by Δ ≈ 1556.8·C0hat²(T)-ish/√n-log-n units... The crossover was ~33 000 (traced). With the C0hat² doubling, the crossover might move to ~60 000–150 000 — DANGEROUSLY close to or past N₀ = 80 000 and the certified base points!!\n\nHmm wait, I should just compute the crossover honestly... this is getting deep into ii′-6 redesign. STOP. Scope discipline: 5f is the R-bound. The H(T) issue is ii′-6's. But the CONSTANTS decision couples them. \n\nGiven the coupling, the RIGHT move per the fork rule and the careful-governance norms: present the finding to the user NOW — D-056's assembly has a genuine factor-2 gap at piece 2 (one-C₀ for the two-unit window), so the baked 10.5/48 is not provable from that assembly as written; options: (B) re-fold with honest constants (A ≈ 11.5, B₀ ≈ 52) + downstream re-verification, or investigate harder. Also flag the ii′-6 H(T) clearance/count issue discovered in the same review (near sum honestly 5C₀²+4C₀ vs baked 3C₀² — or 6C₀²+4C₀ with the current pigeonhole + window extension).\n\nHmm, wait. Actually — let me reconsider whether E-028's numerical verification already settles these questions in a way the Lean proof could use... no — the Lean proof needs the ASSEMBLY, not numerics (the margin is a uniform statement to N₁ = 9×10²⁴).\n\nHold on, hold on. Let me re-examine the piece-2 gap ONE more time, because everything hinges on it. D-056:\n\n\"2. Near at s₀: |s₀−ρ| ≥ 2 − β ≥ 1 ⟹ Σ_{|γ−t|<1} 1/|s₀−ρ| ≤ C₀(t).\"\n\nHmm — is C₀(t) here possibly the count of |γ−t| ≤ 1 = N(t+1)−N(t−1) ≤ F(t+1)−F(t−1) + S(t+1)+S(t−1), and the \"F(t+1)−F(t)\" in the C₀ definition line a typo for F(t+1)−F(t−1)? If C₀(t) were DEFINED as the two-unit count, then the closed form 0.433 log(t+2) + 0.886 loglog(t+2) + 2.9 would need to majorize the two-unit honest form 0.592L + 0.886LL + 3.176: 0.433L + 2.9 vs 0.592L + 3.176 — fails for large L (0.433 < 0.592). So no — the closed form matches the one-unit definition. The gap is real.\n\nHmm, although — wait, actually let me redo the two-unit F-difference: F(x) = (x/2π)(log(x/2π) − 1) + 7/8. F(t+1) − F(t−1): F'(x) = (1/2π)log(x/2π). ∫_{t−1}^{t+1} (1/2π)log(x/2π) dx ≈ (2/2π)·log(t/2π) = (1/π)·(L − log(2π))·... = (1/π)·L − (1/π)·1.838 ≈ 0.318L − 0.585. And the closed form's log coefficient is 0.433 with constant 2.9. The honest two-unit: 0.318L − 0.585 + 0.274L + 0.886LL + 3.176 = 0.592L + 0.886LL + 2.59. vs C₀ closed form 0.433L + 0.886LL + 2.9. Crossover: 0.592L + 2.59 vs 0.433L + 2.9 ⟺ 0.159L = 0.31 ⟺ L ≈ 1.95 ⟺ t ≈ 5.2. For t ≥ 10 (L ≥ 2.4): the two-unit honest form EXCEEDS the C₀ closed form. Confirmed: at t=10, honest-2unit ≈ 0.592·2.48+0.886·0.907+2.59 ≈ 1.47+0.80+2.59 = 4.86 vs C₀(10) = 4.78. So piece 2 honestly ≤ 4.86-ish > 4.78. Tiny but real overage, growing as 0.159·L.\n\nOK so it's definitively a (small) gap in D-056's traced assembly. The bound is numerically fine (26× slack) but the traced constants 10.5/48 can't be reached from that assembly. The Lean 5f must re-fold. Given the coupling to ii′-6's (bigger) H(T) issue, and that BOTH will move the baked constants, the clean path is:\n\n**Re-fold the R-bound AND the H(T)/Hhat accounting honestly NOW, then re-verify the margin artifacts (convexity + base points) with the new constants, then continue.** This is a significant but mechanical rework — and it MUST be done before ii′-6 regardless.\n\nActually — hmm, wait. Let me reconsider the scale of the H(T) fix once more. The central-half trick gives clearance 1/(5C₀) with the SAME pigeonhole count C₀ (window zeros), and near sum ≤ 5C₀² + 4C₀. Even simpler: the L3 statement as PROVED in Lean (exists_zero_avoiding_T) gives T ∈ [a, a+1] with clearance 1/(3·C0hat(a+1)) vs window zeros only. To get the central-half version I'd need a modified pigeonhole (midpoints in [a+1/4, a+3/4]) — the exists_avoiding_midpoint lemma takes (a, S, card bound) and returns a midpoint in [a, a+1]... it could be INSTANTIATED at the sub-window? The zeros to avoid = those in (a−1/4, a+5/4)-ish... Actually exists_avoiding_midpoint a' S' with a' = a+1/4 on window [a+1/4, a+5/4] (width 1): gives T ∈ [a+1/4, a+5/4] avoiding zeros in [a+1/4, a+5/4]... then T could be up to a+5/4 — out-of-[a+1/4,a+5/4] zeros (γ just below a+1/4 or above a+5/4) within |γ−T|<1: γ = a+1/4−ε, T ≤ a+5/4: |γ−T| ≥ (a+1/4−ε) − ... no wait γ < a+1/4 ≤ T: |T−γ| = T−γ ≥ T−(a+1/4) ≥ 0 if T = a+1/4. Hmm — need T in the central half of the AVOIDED window. exists_avoiding_midpoint places T as one of k+1 midpoints spanning the whole window — no centrality guarantee. To force centrality: apply the midpoint pigeonhole on window [a', a'+1] but only to midpoints in the central half... the existing lemma: \"k+1 midpoints a + (2j+1)/(2(k+1))\" — j spans 0..k — the midpoints span [a + 1/(2(k+1)), a + 1 − 1/(2(k+1))] — nearly the full window. For centrality, need a variant: midpoints in [a+1/4, a+3/4], spacing (1/2)/(k+1), k = card bound on the 1.5-unit window (a−1/4, a+5/4)... count ≤ 2C₀. Then T central ⟹ out-of-(a−1/4, a+5/4) zeros ≥ 1/4 away; in-window zeros ≥ 1/(4(2C₀+1)) ≥ 1/(12C₀)... near sum ≤ C₀·(12C₀) [inner 1 unit] + 2C₀·2 [outer] = 12C₀² + 4C₀. Hmm — 12 vs the earlier 5 estimate: the inner window (T−1/2, T+1/2) count... I conflated. Let me redo cleanly:\n\nGoal: bound Σ_{|γ−T|<1} 1/|T−γ|. Given: T ∈ [a+1/4, a+3/4] (central half), clearance d vs ALL zeros with |γ−T| < 5/4 (i.e., in (a−1/2, a+2) ⊂ 3 unit windows, count ≤ 3C₀; pigeonhole with 3C₀+1 midpoints in [a+1/4, a+3/4], spacing (1/2)/(3C₀+1), clearance ≥ (1/4)/(3C₀+1) ≥ 1/(13C₀)). Then:\n- |γ−T| < 1/4: all such zeros are within the cleared neighborhood ⟹ each term ≤ 13C₀; count ≤ C₀ (one unit window (T−1/4, T+1/4]... width 1/2 ≤ 1 ✓ ≤ C₀). Contribution ≤ 13·C₀².\n- 1/4 ≤ |γ−T| < 1: terms ≤ 4; count ≤ 2C₀ ⟹ ≤ 8C₀.\n- Total ≤ 13C₀² + 8C₀.\nvs the earlier rougher 12C₀²+4C₀ / 5C₀²+4C₀ estimates — depends on the geometry choices. Anyway: the honest H(T) C0hat² coefficient lands ~5–13 vs baked 3. \n\nOK — decision time for real. This is a significant finding (a second constants-level gap in the R-004 traced chain — D-056's piece 2 — PLUS the H(T) clearance-coverage gap for ii′-6), and the remediation path (re-fold constants + re-verify margin artifacts) has multiple viable parameter choices. Per the project's governance (fork rule, careful plan changes, user owns the research direction), I should present this to the user with a clear analysis and options before spending sessions on the wrong re-fold.\n\nActually — hmm, wait. Before going to the user, let me make sure the H(T) issue is REAL and not already handled by the D-037 assembly. Let me check D-037's use of H(T). Actually, from LiSkeleton's marginTilde: the B-side has `2 * (Real.exp 4 + 1) * (7 * Hhat T + 3.3)` — the 7·Hhat matches D-036 §3's \"|I_II| = |I_IV| ≤ (e⁴+1)·[7H(T) + e·|ζ′/ζ(2)|·2] ≤ (e⁴+1)·[7H(T)+3.3]\" — the horizontals use H(T) = 3C₀² + A log + B₀ with the near-sum-at-T inside. And the I_III left-vertical term: `4 * T * ((2 / 3) * C0hat T + 10.5 * Real.log (T + 2) + 48)` — the (2/3)·C0hat(T) is the left-vertical near sum (|σ−β| ≥ 1.5 ⟹ terms ≤ 2/3... Σ_{|γ−T|<1} (2/3) ≤ (2/3)·count — with the ONE-C₀ convention again: (2/3)·C₀(T) — honest would be (2/3)·2C₀ = (4/3)C₀). So the baked constants embed the one-C₀ convention in THREE places (R-bound's A/B₀ via piece 2, Hhat's 3C₀², I_III's (2/3)C₀).\n\nSo the honest re-fold touches: A/B₀ (R-bound), the C0hat² coefficient (3 → 5–13), the (2/3) → (4/3) C₀ coefficient in I_III. All in marginTilde's baked arithmetic. The margin slack: ~25× at the theorem level but the CERTIFIED crossover/base-points move. This is exactly a D-054-class repair (like 4.5a–d in session 009).\n\nGiven all this, the honest path forward:\n1. File the finding as a documented repair item (D-069: 5f design + the D-056 piece-2 gap + the H(T) clearance-coverage gap).\n2. Re-derive the honest constants: A/B₀ for the R-bound; the H(T) near-sum coefficient; I_III's C₀ coefficient.\n3. Re-verify the margin (convexity — structural, constants parametric? need to check session-011's proof sensitivity; base points — re-certify by interval bounds; crossover/N₀ — re-run E-023-style numerics to pick N₀... N₀ = 80 000 might no longer have positive margin! Need to recompute. If the new crossover exceeds 80 000, N₀ moves up (≤ 5×10⁵ finite verification cap — actually the finite verification is to 5×10⁵, and N₀ must be ≤ 5×10⁵ AND have positive margin + convexity bridge to N₁).\n4. Re-bake LiSkeleton constants + re-run the Lean margin artifacts.\n\nThis is genuinely a 2–4 session repair arc, and it REPLACES the simple \"5f ~1 session\" plan. The user should decide: (i) full honest re-fold now (recommended — it's required for ii′-6/7 anyway); or (ii) attempt the knife-edge tightening to keep 10.5/48 (my assessment: fails); or (iii) park 5f and re-scope.\n\nHmm — wait, actually, one more consideration before presenting: maybe I'm wrong about the margin going negative at 8×10⁴. My back-of-envelope B-side recomputations are rough. The clean way: recompute the margin numerically with the honest constants (E-023/E-028 machinery exists — the assembly script). That's a 30-min numerics job that would settle the crossover/margin positivity question EXACTLY before any Lean rework. THAT should be step 1 of the repair arc regardless.\n\nLet me now also sanity-check my claim about piece 2 against the ACTUAL near-sum values: at t = 50, near window (49, 51): zeros at 49.77 (4th zero? zeros: 14.13, 21.02, 25.01, 30.42, 32.94, 37.59, 40.92, 43.33, 48.01, 49.77, 52.97, ...) — γ₉ = 48.01, γ₁₀ = 49.77 — in (49, 51): just 49.77: count 1. C₀(50) = 0.433·3.95+0.886·1.37+2.9 = 1.71+1.21+2.9 = 5.83. So 1 ≤ 5.83 hugely — the SLACK per window is ~5×. The honest two-unit Trudgian bound at t=50: 0.592·3.95+0.886·1.37+2.59 ≈ 2.34+1.21+2.59 = 6.14 vs one-unit C₀ 5.83 — overage 0.31. The FOLD impact: piece 2 honest 6.14 vs traced 5.83 — the R-bound total: pieces 1+2+3+4+5+6 = 0.57 + 6.14 + 12.73·5.83·(hmm — piece 3 uses C₀ per interval...). Let me just recompute the honest total at t=50: 0.57 + 6.14 + (12.73·5.83 + 7.06) + 0.38 = 0.57+6.14+74.2+7.06+0.38 = 88.35. Baked bound: 10.5·log(52)+48 = 10.5·3.95+48 = 89.5. 88.35 ≤ 89.5 ✓ FITS at t=50! At t=10: honest: piece2 ≤ 4.86 (computed above), piece 3: 12.73·4.78+7.06 = 60.85+7.06 = 67.91; total: 0.57+4.86+67.91+0.38 = 73.72 vs baked 10.5·2.48+48 = 74.04 ✓ FITS (by 0.3)! At t=1000: piece2: 0.592·6.91+0.886·1.93+2.59 = 4.09+1.71+2.59 = 8.39; C₀(1000) = 0.433·6.91+0.886·1.93+2.9 = 2.99+1.71+2.9 = 7.60; piece 3: 12.73·7.60+7.06 = 96.75+7.06 = 103.8; total: 0.57+8.39+103.8+0.38 = 113.1 vs baked: 10.5·6.91+48 = 120.6 ✓ FITS (by 7.5). At t=10⁶: L = 13.82: piece2: 0.592·13.82+0.886·2.63+2.59 = 8.18+2.33+2.59 = 13.1; C₀ = 0.433·13.82+0.886·2.63+2.9 = 5.98+2.33+2.9 = 11.21; piece3: 12.73·11.21+7.06 = 149.8; total: 0.57+13.1+149.8+0.38 = 163.85; baked: 10.5·13.82+48 = 193.1 ✓ FITS (by 29).\n\nWAIT. It FITS?! Let me recheck my earlier \"breaks\" claim. Earlier I folded piece2 = 2·C₀ (the crude 2× unit count) — but the HONEST two-unit Trudgian form is 0.592L + 0.886LL + 2.59 (NOT 2·C₀!). The key: the two-unit window count via the F-difference has log coefficient 0.318+0.274 = 0.592, NOT 2·0.433 = 0.866 — because the S_b pair does NOT double (it's S(t+1)+S(t−1), still TWO S-terms, same as the one-unit form's S(t+1)+S(t)!). So the honest piece-2 count ≈ C₀(t) + 0.159·L − 0.3 — only slightly MORE than C₀(t). And the fold:\n\n|R| ≤ Z₂ + [C₀(t) + 0.159L] + [12.73·C₀(t) + 7.06] + 0.38 = 13.73·C₀(t) + 0.159L + 8.01\n   ≤ 13.73·(0.433L + 0.886LL + 2.9) + 0.159L + 8.01\n   = 5.945L + 12.16LL + 39.82 + 0.159L + 8.01\n   = 6.104L + 12.16LL + 47.83\n   ≤ (6.104 + 12.16/e)·L + 47.83 = (6.104 + 4.474)·L + 47.83 = 10.578·L + 47.83.\n\nvs 10.5L + 48: 10.578 > 10.5 — STILL over by 0.078·L − 0.17. At L = 2.48 (t=10): over by 0.19−0.17 = 0.02. At L = 6.91: over by 0.54−0.17 = 0.37. Hmm — but my per-t computation above said it FITS at t=10/50/1000?! Because I used the exact honest piece-2 (4.86 at t=10) vs the folded 0.159L-term... At t=10: my fold gives 10.578·2.48 + 47.83 = 26.23+47.83 = 74.06 vs baked 74.04 — over by 0.02. The direct computation gave 73.72 (fits by 0.32). The difference: the loglog≤L/e fold is lossy at small t, and my 0.159L+8.01 vs the exact piece-2... The truth is at the knife-edge: ±0.3 at t=10, and the ASYMPTOTIC coefficient 10.578 > 10.5 breaks it for large t... at t=10⁶: fold says 10.578·13.82+47.83 = 146.2+47.8 = 194.0 vs baked 193.1 — over by 0.9. Direct: 163.85 vs 193.1 — fits by 29!! The discrepancy: the direct per-t computation uses the exact LL term (LL(10⁶) = log 13.82 = 2.63, while L/e = 5.08 — the LL≤L/e fold loses 12.16·(5.08−2.63) = 29.8 at t=10⁶!!). So the fold loglog ≤ (1/e)·log is HUGELY lossy for t ≫ e^e ≈ 15.15. The bound 10.5L + 48 might actually hold via the assembly with a BETTER loglog fold!\n\nThe loglog fold: want c₁L + c₂LL + c₃ ≤ 10.5L + 48 with c₁ = 6.104, c₂ = 12.16, c₃ = 47.83. I.e., need 12.16·LL ≤ (10.5−6.104)·L + (48−47.83) = 4.396·L + 0.17. LL ≤ (4.396/12.16)·L + 0.014 = 0.3615·L + 0.014. Is loglog(t+2) ≤ 0.3615·log(t+2) + 0.014 for t ≥ 10? Let x = log(t+2) ≥ log 12 = 2.485: need log x ≤ 0.3615·x + 0.014. The max of log x / x is 1/e = 0.3679 at x = e — 0.3615 < 0.3679! At x = e (t+2 = e^e = 15.15, t = 13.15): log x = 1, need 1 ≤ 0.3615·e + 0.014 = 0.9825 + 0.014 = 0.9965 — 1 ≤ 0.9965 FALSE! So at t ≈ 13.15, the inequality 12.16LL ≤ 4.396L + 0.17 FAILS by ~0.0035!! KNIFE-EDGE FAILURE at t ≈ 13.\n\nThe failure is by 0.0035 at exactly one spot (t ≈ 13.15) — the assembly with the honest piece-2 misses 10.5/48 by 0.004 THERE. But wait — my constants are rough (0.159L for the piece-2 overage, the piece-3 constants 12.73/7.06, the 0.38 for pieces 4–6, Z₂ = 0.57). The TRUE assembly values (exact piece-3 interval sums, exact piece-2 two-unit form, exact piece-6) could easily absorb 0.004. E.g., Z₂ = 0.56996 not 0.57 (−0.00004... too small). Piece 3's 12.73 = 4.5√2·2: 4.5√2 = 6.36396; the tail 0.53→?; C₀(2t) ≤ C₀(t)+0.58→0.30 — saves 6.364·0.28 ≈ 1.78 — WAY more than 0.004. So with slightly sharper bookkeeping, 10.5/48 is reachable. BUT the bookkeeping must be Lean-provable — every constant needs a machine-checkable derivation. A knife-edge fit at t ≈ 13.15 (by ~0.01) is fragile but POSSIBLE with exact interval arithmetic (like LiBasePoints' certified bounds). Hmm — but \"fragile at one point\" for a UNIFORM bound over t ≥ 10... the pointwise near-miss at t ≈ 13 means the proof must be exact there — certified interval evaluation of the assembly at the worst point. Doable (LiBasePoints machinery exists) but delicate.\n\nALTERNATIVELY — change the fold: don't fold LL ≤ L/e globally; keep the honest three-term form 6.104L + 12.16LL + 47.83 and prove THAT ≤ 10.5L + 48 for t ≥ 10... which fails at t ≈ 13 by 0.004 as shown. So the assembly's own constants must improve by ≥ 0.01 at t = 13 before the fold. Options: piece-3 right-side C₀(2t) → C₀(t)+0.433·log 2 exactly (saves 6.364·(0.58−0.30) = 1.8); the piece-3 tail 0.53 → exact (t=13: Σ_{k>t} C₀(2t)/(k(k+1)) + ... ≤ C₀(2t)/(t+1) + 0.433/t ≈ 5.9/14 + 0.03 ≈ 0.45 → saves 0.08); pieces 4–6: 0.38 → 0.36. Piece-2's overage 0.159L−0.31 → exact two-unit F/S form. These save ~1.9 total at t=13 — the 0.004 gap closes 400×. So YES, 10.5/48 is provable with careful bookkeeping — the D-056 assembly was lossy, not wrong-headed.\n\nCONCLUSION: 5f is feasible at the baked 10.5/48 constants, but requires a TIGHTER assembly than D-056's text (piece-2 two-unit form, piece-3 sharper right-side/tail accounting), with the t ≈ 13 near-miss discharged by certified interval evaluation (the LiBasePoints pattern). The Lean work: (i) two-unit window count from the mult-weighted ZeroCountProp: Σ_{(t−1,t]} + Σ_{(t,t+1]} ≤ C0hat(t) + C0hat(t+1) — hmm WAIT. The Lean perimeter gives the closed-form C0hat window counts, NOT the F/S-pair Trudgian form! The honest two-unit form 0.592L + 0.886LL + 2.59 was derived from F/S-pair directly. From the Lean perimeter (C0hat per unit window), the two-unit count ≤ C0hat(t) + C0hat(t+1) = 0.433(L₁+L₂) + 0.886(LL₁+LL₂) + 5.8 where L₁ = log(t+1), L₂ = log(t+2)... = 0.866L + 1.772LL + 5.8 — the CRUDE doubling! The F/S-pair refinement (0.592L+...) is NOT available from the perimeter as declared (ZeroCountProp gives per-unit C0hat bounds; the two-unit sum is two applications).\n\nHmm!! So in Lean, piece 2 ≤ C0hat(t) + C0hat(t+1) ≤ 2·C0hat(t+1) = 0.866L' + 1.772LL' + 5.8 (L' = log(t+3)). The fold: 0.57 + 2C₀' + 12.73C₀' + 7.06 + 0.38 where C₀' = C0hat(t+1) — wait no: piece 3's per-interval counts also come from the perimeter: left intervals ≤ C0hat(t−k+1) ≤ C0hat(t); right ≤ C0hat(t+k+1) ≤ C0hat(2t+1). So piece 3 ≤ 4.5√2·[C0hat(t)·1 + C0hat(2t+1)·1 + tail]. C0hat(2t+1) ≤ C0hat(t+1) + 0.433·log 2 + 0.886·(LL(2t+1)−LL(t+1)) ≤ C0hat(t+1) + 0.31+0.27-ish. So the fold in Lean: pieces: 0.57 + 2·Ĉ + 6.364·[Ĉ + Ĉ+0.58 + 0.53] + 0.38 = 0.57 + 2Ĉ + 12.73Ĉ + 7.06 + 0.38 = 14.73·Ĉ + 8.01 where Ĉ = C0hat(t+1) ≈ 0.433L' + 0.886LL' + 2.9. Total = 14.73·(0.433L'+0.886LL'+2.9) + 8.01 = 6.378L' + 13.05LL' + 42.72 + 8.01 = 6.378L' + 13.05LL' + 50.73. Fold LL ≤ L/e: (6.378 + 13.05/e)L' + 50.73 = (6.378+4.80)L' + 50.73 = 11.18L' + 50.73 vs 10.5L + 48. BREAKS (as computed before: at t=10: 11.18·2.56+50.73 = 79.3 vs 74.0).\n\nSo with the Lean perimeter's per-unit closed-form counts, the assembly CANNOT reach 10.5/48 (breaks by ~5 at t=10 and 0.68·L asymptotically). To keep 10.5/48, the piece-2 two-unit count must use the F/S-pair form (0.592L + 0.886LL + 2.59) — which is a DIFFERENT perimeter declaration (the two-unit Trudgian form), OR ZeroCountProp could be declared with the two-unit form built in... but ZeroCountProp's C0hat IS the one-unit closed form. The F/S-pair form is a genuinely sharper/different declared input.\n\nHmm — OR: strengthen ZeroCountProp's CONTENT: declare the count bound for the two-unit window |γ−t|<1 directly as a C0hat-shaped bound: #{|γ−t|≤1} ≤ Ĉ₀⁽²⁾(t) := 0.6·log(t+2) + 0.886·loglog(t+2) + 2.7 (the honest two-unit closed form: 0.592L + 0.886LL + 2.59 rounded up). This is still Trudgian N(t+1)−N(t−1) + S-pair — same declared source! Just a different specialization. Then piece 2 ≤ Ĉ₀⁽²⁾(t), and the fold: 0.57 + (0.6L + 0.886LL + 2.7) + 12.73·(0.433L + 0.886LL + 2.9) + 7.06 + 0.38 = [0.6 + 12.73·0.433]L + [0.886 + 12.73·0.886]LL + [0.57+2.7+12.73·2.9+7.06+0.38] = [0.6+5.512]L + [0.886+11.28]LL + [47.13] = 6.112L + 12.17LL + 47.13. Fold LL ≤ L/e: (6.112 + 4.478)L + 47.13 = 10.59L + 47.13 vs 10.5L + 48: 10.59 > 10.5 — STILL over asymptotically by 0.09L!! At t=10: 10.59·2.48+47.13 = 73.4 vs 74.04 ✓ fits by 0.6; at t=13.15 (the loglog pinch): L = log 15.15 = 2.718, LL = 1.0: LHS pieces: 6.112·2.718 + 12.17·1.0 + 47.13 = 16.61+12.17+47.13 = 75.91 vs 10.5·2.718+48 = 76.54 — fits by 0.63 ✓; asymptotically: (10.59−10.5)L vs (48−47.13) = 0.87: 0.09L > 0.87 for L > 9.7 ⟺ t > 16 000!! At t = 10⁵: 0.09·11.5 = 1.04 > 0.87 — BREAKS for t ≳ 2×10⁴. And the contour goes to T = √N₁ = 3×10¹²!! So the asymptotic overage 0.09·L is fatal at the top of the range. \n\nHmm!!! So even the two-unit-form piece 2 + piece-3 as-is breaks at large t. The asymptotic log coefficient budget: 10.5 − (piece-2's L-coefficient 0.592 + piece-3's 12.73·0.433 = 5.512 + ...) let me recompute the minimal achievable: pieces: Z₂ (0.57, no L) + piece2 (0.592L + 0.886LL + 2.59) + piece3 (4.5√2·[C₀(t)·1 + C₀(2t)·1 + tail]: L-coefficient 6.364·(0.433+0.433) = 5.512, LL-coefficient 6.364·(0.886+0.886) = 11.28, constants 6.364·(2.9+2.9+0.53·..)...) — the RIGHT side intervals use C₀(t+k+1) — for k up to t — C₀(t+k+1) ≤ C₀(2t+1) — with L-coefficient 0.433. So piece-3 L-coefficient: 6.364·(0.433 + 0.433) = 5.512. TOTAL L-coefficient: 0.592 + 5.512 = 6.104; LL: 0.886 + 11.28 = 12.17. The LL-fold at best gives LL/L ≤ 1/e (equality at t = 13.15): total effective L-coefficient ≤ 6.104 + 12.17/e = 6.104 + 4.478 = 10.582 > 10.5. ASYMPTOTICALLY the assembly's minimum with this structure is 10.582 — over 10.5 by 0.082. For the bound to hold for ALL t ≥ 10 up to 3×10¹², we need the total ≤ 10.5L + 48 at the top: at L = 28.7 (t = 3×10¹²): 10.582·28.7 = 303.7 vs 10.5·28.7+48−... wait the LL fold: at t = 3×10¹², LL = log(28.7) = 3.36, L/e = 10.56 — the LL≤L/e fold loses 12.17·7.2 = 87 there! So the UNFOLDED assembly: 6.104L + 12.17LL + 47.13 at t = 3×10¹²: 6.104·28.7 + 12.17·3.36 + 47.13 = 175.2 + 40.9 + 47.1 = 263.2 vs 10.5·28.7 + 48 = 349.4 — FITS by 86!! The unfolded form fits comfortably at large t; the pinch is only near t ≈ 13 (where LL/L peaks at 1/e). At t = 13.15: 6.104·2.718 + 12.17·1.0 + 47.13 = 16.59 + 12.17 + 47.13 = 75.89 vs 10.5·2.718 + 48 = 76.54 — fits by 0.65 ✓!! \n\nSo the UNFOLDED honest assembly 6.104L + 12.17LL + 47.13 ≤ 10.5L + 48 holds: need 12.17·LL ≤ 4.396·L + 0.87. At the LL/L max (x = e, LL = 1, L = e): 12.17 ≤ 4.396·2.718 + 0.87 = 11.95 + 0.87 = 12.82 ✓ (by 0.65). For x ≥ e: LL grows slower; the worst point IS x = e. So the two-sided inequality 6.104L + 12.17LL + 47.13 ≤ 10.5L + 48 ⟺ 12.17LL − 4.396L ≤ 0.87 — the LHS max over t ≥ 10: d/dL[12.17 log L − 4.396 L] = 12.17/L − 4.396 = 0 at L = 2.769 (t+2 = 15.97, t = 13.97): value 12.17·1.019 − 4.396·2.769 = 12.40 − 12.17 = 0.23 ≤ 0.87 ✓. And at L = log 12 = 2.485 (t=10): 12.17·0.910 − 4.396·2.485 = 11.07 − 10.92 = 0.15 ✓. So the max of (12.17LL − 4.396L) over t ≥ 10 is ≈ 0.23 ≤ 0.87 ✓✓ COMFORTABLE (4× margin). \n\nSo the honest assembly DOES prove 10.5 log(|t|+2) + 48 — with:\n- piece 2 via the honest two-unit Trudgian form (0.592L + 0.886LL + 2.59-ish closed form — call it Ĉ₀⁽²⁾(t));\n- piece 3 as in D-056 (12.73·C₀ + 7.06 — maybe slightly sharpened);\n- the UNFOLDED loglog comparison (NOT LL ≤ L/e — instead prove 12.17·LL + const ≤ 4.396·L + 0.87 by calculus: max at L ≈ 2.77, value 0.23).\n\nBut the Lean perimeter gives per-UNIT C0hat counts — piece 2's two-unit form 0.592L + 0.886LL + 2.59 is NOT derivable from 2·C0hat (that's 0.866L + 1.77LL + 5.8 — too big). So the perimeter declaration needs a two-unit variant. Options: (i) change ZeroCountProp AGAIN to give the two-unit form (ZeroCountProp2: #{|γ−t|≤1, mult-weighted} ≤ C0hat2(t) := 0.6·log(t+2) + 0.886·loglog(t+2) + 2.7 — needs verification that the honest form 0.592L + 0.886LL + 2.59 ≤ that closed form for t ≥ 9-ish ✓ plausible); the one-unit form follows? NO — one-unit ≤ two-unit form ✓ (one-unit window ⊂ two-unit window... zeroWindow t = [t, t+1] ⊂ |γ−t| ≤ 1? [t, t+1] ⊂ [t−1, t+1] ✓). So declaring the two-unit form SUBSUMES the one-unit form (the gap-circle and L3 consumers use [t, t+1] windows — the two-unit bound applies). Hmm — but the one-unit count ≤ two-unit closed form 0.6L + 0.886LL + 2.7 vs the OLD C0hat(t+1) = 0.433L + 0.886LL + 2.9 — the two-unit form is BIGGER in L-coefficient (0.6 > 0.433) but the existing consumers (gap circles, L3) only use C0hat qualitatively (clearances 1/(16·C0hat), 1/(3·C0hat)) — a bigger C0hat gives SMALLER clearances — do the proofs still go through? exists_zero_avoiding_T: the pigeonhole k = card ≤ C0hat — a bigger bound still works (k+1 midpoints, clearance 1/(2(k+1)) ≥ 1/(3·C0hat) — the constants 2(k+1) vs 3·C0hat: needs 3·C0hat ≥ 2(k+1) ⟸ C0hat ≥ 2, k ≤ C0hat ✓ structural). The gap circles: similar structural use. So swapping C0hat's VALUE to the two-unit form propagates... but wait, C0hat is ALSO used in LiSkeleton's marginTilde/Hhat (the baked margin!) — changing C0hat's value changes the margin computation and all certified artifacts!!! NO — don't touch C0hat. ADD a separate declared form for the two-unit window.\n\nSo: new perimeter item ZeroCountProp2 (two-unit, mult-weighted, closed form 0.6L + 0.886LL + 2.7 — verify constants) — declared under the SAME Trudgian source (it's literally N(t+1)−N(t−1) + S-pair). This GROWS the declared perimeter by a specialization of an existing item (justified in the journal + ii′-7 paper appendix note).\n\nHmm, hold on — is the two-unit closed form honestly derivable from the one-unit C0hat? NO (shown: 2·C0hat too big). Is it honestly derivable from Trudgian's F/S theorems? YES (N(t+1)−N(t−1) ≤ F(t+1)−F(t−1) + S_b(t+1)+S_b(t−1) — published). But our perimeter doesn't have F and S_b separately — only the C0hat specialization. So declaring the two-unit specialization is declaring ANOTHER consequence of the same published theorem. Honest — but it's a perimeter GROWTH (needs user sign-off).\n\nALTERNATIVE: prove the two-unit closed form from the one-unit perimeter + monotonicity cleverness? #{|γ−t|≤1} = #{(t−1, t]} + #{(t, t+1]} ≤ C0hat(t) + C0hat(t+1) — the only route from the current perimeter. 0.866L + 1.77LL + 5.8. Too big. No.\n\nSo the choice:\n(α) Declare the two-unit form (perimeter growth, same Trudgian source) ⟹ 5f provable at 10.5/48 with the unfolded LL treatment (max-at-L≈2.77 calculus lemma + the certified endpoint checks).\n(β) Keep per-unit perimeter ⟹ honest constants become A ≈ 11.2, B₀ ≈ 51 ⟹ re-bake marginTilde/Hhat + re-verify convexity + re-certify base points + (ii′-6 will face the H(T) clearance issue separately, possibly moving constants AGAIN).\n\n(α) is strictly better: keeps ALL baked constants (no downstream rework), same declared source, and the calculus lemma (12.17·LL ≤ 4.396·L + 0.87 for L ≥ log 12) is a clean one-variable real fact (max at an interior point, value comparison — provable via deriv + the two-point method already in Lean).\n\nWait — but I should double-check the (α) fold arithmetic once more, carefully, with the EXACT piece constants, because 5f will need to reproduce them in Lean:\n\nPiece 1: ‖logDeriv ζ (2+it)‖ ≤ dirichletC2. What IS dirichletC2 in Lean? Need to check — if it's 0.57-ish ✓. (Check the def.)\nPiece 2: Σ_near m/|s₀−ρ| ≤ Σ_near m ≤ Ĉ₀⁽²⁾(t) := 0.6·log(t+2) + 0.886·loglog(t+2) + 2.7 — VERIFY this honest form: N(t+1)−N(t−1) ≤ F(t+1)−F(t−1) + S_b(t+1) + S_b(t−1):\n  F(t+1)−F(t−1) = (1/2π)·∫_{t−1}^{t+1} log(x/2π) dx ≤ (2/2π)·log((t+1)/2π) = (1/π)·(log(t+2) − log 2π + log((t+1)/(t+2))·...) ≤ (1/π)·log(t+2) − (1/π)·log(2π) + (1/π)·log((t+1)/(t...)) hmm just ≤ (1/π)·log(t+2) for t+1 ≤ 2π·(t+2)-ish?? (1/π)log((t+1)/2π) ≤ (1/π)log(t+2) ⟺ (t+1)/2π ≤ t+2 ✓ always. But we need to be careful: (1/π)·log((t+1)/(2π)) could be NEGATIVE-small... For t ≥ 10 it's ≥ (1/π)·log(11/6.28) = (1/π)·0.561 = 0.179. Bound: (1/π)·log((t+1)/2π) ≤ (1/π)·log(t+1) − (1/π)·log 2π ≤ (1/π)·log(t+2) − 0.585. So F-part ≤ 0.3183·L − 0.585 where L = log(t+2).\n  S-pair: S_b(t+1)+S_b(t−1) = 0.137·(log(t+1)+log(t−1)) + 0.443·(loglog(t+1)+loglog(t−1)) + 3.176 ≤ 0.274·log(t+2)... hmm log(t−1) < log(t+1) < log(t+2) ✓; loglog similarly (t−1 ≥ 9 > e ✓). So S-pair ≤ 0.274·L + 0.886·LL + 3.176.\n  Total: ≤ (0.3183 + 0.274)·L + 0.886·LL + (3.176 − 0.585) = 0.5923·L + 0.886·LL + 2.591. So Ĉ₀⁽²⁾(t) := 0.6·L + 0.886·LL + 2.7 has slack: 0.0077·L + 0.109 ≥ 0 ✓ (for L ≥ 0). ✓ SAFE closed form.\n  [This is a NEW declared specialization of Trudgian; needs the F(t+1)−F(t−1) + S_b pair bound — from the same Trudgian 2014 Thm 1. Justification: same source, different window.]\nPiece 3: as D-056: ≤ 4.5√2·[C₀(t)·Σ_left 1/(k(k+1)) + C₀(2t)·Σ_right + tail] ≤ 4.5√2·[C₀(t) + C₀(2t) + 0.53]·... hmm wait — D-056: \"left side ≤ C₀(t), right side k ≤ t ≤ C₀(2t) ≤ C₀(t) + 0.58; the k > t tail ≤ C₀(2t)/(t+1) + 0.433/t ≤ 0.53\". With C₀ = C0hat: C0hat(2t) ≤ C0hat(t+1) + 0.433·log 2 + 0.886·[LL(2t+2) − LL(t+2)]·... ≤ C0hat(t+1) + 0.31 + 0.886·(log 2)/(L)... eh — D-056's 0.58 covers it. So piece 3 ≤ 4.5√2·[C0hat(t+1) + C0hat(t+1) + 0.58 + 0.53] = 4.5√2·[2·C0hat(t+1) + 1.11] = 12.7279·C0hat(t+1) + 7.063. (4.5√2 = 6.36396; ×2 = 12.7279; ×1.11 = 7.064.)\n  In Lean, the per-interval count: the interval (t−k−1, t−k] for k = 1..⌈t⌉: these are unit windows at heights t−k−1 ≥ ... hmm — for k close to t, the window is at LOW height (t−k−1 could be < 2, where ZeroCountProp doesn't apply!). D-056's left side: intervals down to height ~0... the count C₀(t−k) for windows at height < 2 — ZeroCountProp requires t ≥ 2. The near-window |γ−t|<1 with t ≥ 10: intervals (t−k−1, t−k] for k ≥ 1: heights ≥ t−k−1; for k ≤ t−3: height ≥ 2 ✓; for k > t−3: heights < 2 — the zeros with |γ| < 3-ish: there are NONE (first zero at 14.13!). So for t ≥ 10, the far sum's intervals with k > t − 14 are EMPTY (no zeros below 14.13). In Lean: use the first-zero fact (Zeta23 has a zero-free region to 14.13? or the IsNontrivialZero definition gives 0 < re < 1 only — the 14.13 lower bound on |γ| needs a zero-free input! Does Zeta23/our package have |γ| ≥ 14? Hmm — Zeta23 might have a zero-free disc or the classical |γ| ≥ 14 via... not sure. ALTERNATIVELY: use the A0count-style unconditional count for the low windows? The A0count bridges in LiCircleBound count windows at ALL heights (mult-weighted, unconditional: Ncount_le_of_interval...). Those give ~A₀·log — for the few low intervals the A₀ constant is fine (bounded number of intervals below height 2... actually the intervals (t−k−1, t−k] with t−k−1 < 2 means k > t−3: heights from ~−1 to 2 — but also NEGATIVE heights (γ < 0 symmetric side). The far sum over ALL zeros with |γ−t| ≥ 1: γ ranges over all ordinates — positive and negative. For γ < 0 with t ≥ 10: |γ−t| = t + |γ| ≥ t — those are the \"k > t\" tail on the negative side. D-056's accounting: \"left side ≤ C₀(t)\" (γ < t side: intervals k=1..~t, i.e., γ ∈ (0, t−1)), \"right side\" γ ∈ (t+1, 2t]: k ≤ t, count C₀(2t); \"k > t tail\": γ > 2t AND the negative side?? D-056's \"k > t tail ≤ C₀(2t)/(t+1) + 0.433/t ≤ 0.53\" — hmm this doesn't obviously include γ < 0. Actually by the symmetry γ → −γ (conjugate zeros — isNontrivialZero_conj in Lean), the γ < 0 side mirrors... no wait — for t ≥ 10 and γ < 0: |t−γ| = t−γ = t+|γ| which is LARGE — these are in the k > t tail: Σ_{γ<0} 4.5√2/(|t−γ|(1+|t−γ|)) = Σ_{γ' > 0} 4.5√2/((t+γ')(1+t+γ')) ≤ Σ_k C₀(k)/((t+k)(1+t+k))-ish ≤ C₀(∞)... D-056's tail bound \"C₀(2t)/(t+1) + 0.433/t\" might be exactly this (the far tail dominated by intervals at height ~t+k with count C₀(t+k) ≤ ...). The details need care in Lean — the negative side via conjugation symmetry.\n\nOK — the design is getting long but the shape is clear. Let me now also double check piece 3's left-side: \"left side ≤ C₀(t)\": the intervals (t−k−1, t−k] for k = 1, 2, ... down to height 0: counts C0hat(t−k+1) ≤ C0hat(t) for k ≥ 1 ✓ (mono, needs t−k ≥ 1 for the perimeter's t ≥ 2 — intervals with t−k ∈ [1, 2): partially... ugh, ZeroCountProp requires the window START ≥ 2. For windows starting in [0, 2): no zeros (14.13) — needs the zero-free input OR the A0count bridges. In LiCircleBound, `lowZeroConst` handles exactly this (the low zeros — from session 031: \"lowZeroConst\" — the finite ball count). Let me check its value: lowZeroConst is presumably 0 (no zeros below 14.13!) or a small finite count. From session-031/032 notes: \"lowZeroConst\" used in the series bound shell_low (2·lowZeroConst). Let me check its definition.\n\nI need to stop designing in my head and check these Lean facts. Let me look at:\n1. dirichletC2's definition/value (piece 1).\n2. lowZeroConst (the low-zero count — is it 0?).\n3. Does the package have a |γ| ≥ 14-ish zero-free fact?\n4. A0count's role for low windows.\n\nThen write D-069 (the 5f design doc) and present the perimeter-growth decision (the two-unit form declaration) to the user together with the piece-2 gap finding.","signature":""},{"type":"text","text":"The piece-2 accounting question is resolved — but it reveals a real gap. Let me verify the key Lean-side values before finalizing the design: `dirichletC2`, `lowZeroConst`, and any zero-free input."},{"type":"tool_use","id":"Bash_115","name":"Bash","input":{"command":"cd D:/Python/Quantum/research/lean/NguyenRH1/NguyenRH1; sed -n '200,215p' LiCircleBound.lean; echo ===LOW===; sed -n '330,360p' LiCircleBound.lean | grep -n \"lowZero\\|theorem\\|def\\|:=\" | head -12; echo ===ZF===; grep -rn \"14\\|zeroFree\\|zero_free\\|first zero\" LiSkeleton.lean | grep -i \"zero\\|14\" | head -8","description":"Check dirichletC2, lowZeroConst, zero-free inputs"},"extra_content":null}]