← Session 21 — Tier ii′ planning + launch: close SfBoundProp in Lean (D-064)
thinking (5348 chars)
KEY LINE from D-032: "Thm 6.1 (unconditional, finite part): S_f(n) = λ_n(√n) + O(√n log n)".
So Lagarias's Thm 6.1 states S_f(n) = λ_n(√n) + O(√n log n) where λ_n(T) is the TRUNCATED zero sum λ_n(T) := Σ_{|γ|≤T}′ [1−(1−1/ρ)ⁿ]! And the contour bounds the DIFFERENCE S_f(n) − λ_n(√n) = O(√n log n), and separately |λ_n(√n)| ≤ 2N(√n) + window slack (via RH-to-T₀ + the e-bound for off-line in the window). So the B(n) accounting (4.1): |S_f| ≤ |λ_n(T)| + |S_f − λ_n(T)| ≤ [2N(T) or 2N(√n) + 4C₀] + [sides + triv + ...]. That's why B(n) has 2F(T) AND the sides but NO Res₁ and NO tail: the tail and Res₁ are both inside the "S_f − λ_n(T) = contour remainder" which is bounded by the sides + triv + 1...
Hmm wait, but that still leaves the question: what IS S_f(n) mathematically (so that Sf(Lean) = S_f)? From BL Thm 2 it's DEFINED as S_∞ + 1 − λ_n. And Lagarias proves S_f(n) − λ_n(√n) = O(√n log n) — the difference between the full-finite-part and the truncated zero sum. So the contour computes/bounds S_f − λ_n(T), NOT the truncated sum itself. And that difference must involve: tail(T) − Res₁ + triv... let me redo with correct algebra:
Sf = S_∞ + 1 − λ_n = S_∞ + 1 − λ_n(T) − tail(T) where λ_n(T) = Σ_{|γ|≤T}[1−(1−1/ρ)ⁿ] (truncated, and by reindexing = Σ_{|γ|≤T}[1−(ρ/(ρ−1))ⁿ] up to the reflect symmetry — careful: reflect maps |γ|≤T to itself ✓ so the truncated set is reflect-invariant and reindexing works exactly).
Sf − λ_n(T)?? No: Sf = S_∞ + 1 − λ_n, so S_f − λ_n(T) is not natural; what Lagarias means: S_f(n) = S_∞ + 1 − λ_n. And the contour gives:
λ_n − λ_n(T) = tail(T), and separately from (∗):
λ_n(T) = Σ_{|γ|<T}[1−(ρ/(ρ−1))ⁿ] = sides − triv − Res₁.
So λ_n = sides − triv − Res₁ + tail.
Sf = S_∞ + 1 − sides + triv + Res₁ − tail.
|Sf| ≤ |λ_n(T)| + |Sf − λ_n(T)|? Lagarias's Thm 6.1: S_f = λ_n(√n) + O(√n log n). So the bound: |S_f| ≤ |λ_n(√n)| + |S_f − λ_n(√n)|, where:
- |λ_n(√n)| ≤ 2N(√n) + 4C₀-ish (RH bridge + window) — the "2F(T)" B(n) term.
- S_f − λ_n(√n) = [S_∞ + 1 + Res₁ + triv] − sides − tail + [λ_n(T) − λ_n(√n)] — hmm the bracket [S_∞+1+Res₁+triv] is still there!
UNLESS the bracket vanishes identically. At n=1: bracket = −1.554120+1−0.577216+0.333333 = −0.798003. And sides(T=2) at n=1 =? and λ_n(2) = 0 (no zeros below 2). S_f(1) − λ_1(2) = −0.577216 − 0 = −0.577216. My formula: S_f − λ_n(T) = bracket − sides − tail + ... let me recompute: S_f = bracket_A − sides − tail where bracket_A = S_∞+1+Res₁+triv = −0.798003. S_f(1) = −0.577216. So −0.577216 = −0.798003 − sides(2) − tail(2) ⟹ sides(2) + tail(2) = −0.220787. tail(2) = λ_1 − λ_1(2) = λ_1 = 0.023096. sides(2) = −0.243883. Consistency can't be eyeballed, fine.
The point: bracket_A ≠ 0, so the decomposition "Sf = bracket_A − sides − tail" is exact but the bracket is a specific O(1)-ish number at n=1... at general n: bracket_A(n) = S_∞(n) + 1 + Res₁(n) + triv(n). How big is it? At n=2: −1.874539 + 1 − 0.894071 + 0.555556 = −1.213054. Sf(2) = −0.966922 = bracket_A − sides − tail ⟹ sides + tail = −0.246132.
Hmm so bracket_A is O(1)-scale at n=1,2 (−0.798, −1.213). Is bracket_A identically small/bounded? What IS bracket_A asymptotically? S_∞(n) ~ ½n log n; Res₁(n) = Σ_j C(n,j)c_{j−1}: leading behavior? c_k are Stieltjes-related; the sum Σ_j C(n,j)c_{j−1} is a binomial transform — if bracket_A stays O(n) or smaller, then S_∞ + Res₁ must cancel the ½n log n term. This is EXACTLY the identification: S_∞(n) + Res₁(n) + 1 + triv(n) = small. Lagarias's (4.11) identity says S_∞(n) = Σ_j (−1)^j C(n,j) a_j with a_j archimedean; and Res₁ = Σ_j C(n,j) c_{j−1}; the identification needed: Σ_j C(n,j)[(−1)^j a_j + c_{j−1}] = −1 − triv(n) + bracket_A(n) with bracket_A SMALL (bounded by the B(n) constant term — e.g. ≤ a few units, absorbed into the "+1"-style constants). Is bracket_A(n) maybe EXACTLY 0 for all n? At n=1: −0.798 ≠ 0. So not zero. Is it maybe −λ_n + λ_n(T)+... no...
Hmm, hold on — maybe I have the sign of Res₁ wrong. Let me recompute the residue at w=1 of k_n(w−1)(−ζ′/ζ). Res of a pole of order n+1: the product k_n(w−1)·(−ζ′/ζ(w)): k_n(w−1) = Σ_{j=1}^n C(n,j) u^{−j} (u = w−1), −ζ′/ζ = Σ_{k≥−1} c_k u^k with c_{−1} = 1, c_0 = −γ. Product: Σ_j Σ_k C(n,j)c_k u^{k−j}. Residue = coeff of u^{−1}: k − j = −1 ⟹ k = j−1: Σ_{j=1}^n C(n,j) c_{j−1} ✓ as I had.
At n=1: c_0 = −γ ✓. So Res₁(1) = −γ = −0.577216 = S_f(1)!! And bracket_A(1) = S_∞(1)+1+Res₁(1)+triv(1) = S_f(1) + 1 + triv(1) − λ_1... = −0.577 + 1 + 0.333 − 0.0231·... wait bracket_A = S_∞+1+Res₁+triv = −1.554120+1−0.577216+0.333333 = −0.798003. And S_f(1) = −0.577216. So S_f ≠ bracket stuff... but S_f(1) = Res₁(1) EXACTLY (both −γ). Interesting!!
At n=2: S_f(2) = −0.966922 vs Res₁(2) = −0.894071. NOT equal. Difference −0.072851. Hmm so S_f(1) = Res₁(1) but S_f(2) ≠ Res₁(2).
What's triv(2)? = 1−(2/3)² = 0.5556. Res₁(2) + triv-ish... −0.894071 + 0.072816(γ₁)... hmm.
What if S_f(n) = Res₁(n) + Σ_{trivial zeros ρ_t}[1−(ρ_t/(ρ_t−1))ⁿ] with the trivial sum understood via ITS OWN archimedean regularization... The trivial sum Σ_k[1−(2k/(2k+1))ⁿ] diverges, but its "finite part"... At n=1 the finite part of Σ 1/(2k+1) relates to log 2-ish not −γ...
I'm clearly not going to rediscover the exact BL bookkeeping by numerology. The right move: READ BL Thm 2's actual statement (we have "BL-1999-fulltext.txt" and "Theorem-2.txt" in research/paper/!). Let me read those.
D-032 gives the key: "Thm 6.1: S_f(n) = λ_n(√n) + O(√n log n)". Let me read the actual BL Thm 2 statement from the archived text to pin the decomposition exactly.
tool: Bash
input
{
"command": "wc -l /d/Python/Quantum/research/paper/BL-1999-fulltext.txt /d/Python/Quantum/research/paper/Theorem-2.txt 2>/dev/null; grep -n \"S_\\\\\\\\infty\\|S_f\\|Theorem 2\" /d/Python/Quantum/research/paper/Theorem-2.txt | head -20",
"description": "Check BL text files and Theorem 2 content"
}
raw content_json (database row)
[{"type":"thinking","thinking":"KEY LINE from D-032: \"Thm 6.1 (unconditional, finite part): S_f(n) = λ_n(√n) + O(√n log n)\".\n\nSo Lagarias's Thm 6.1 states S_f(n) = λ_n(√n) + O(√n log n) where λ_n(T) is the TRUNCATED zero sum λ_n(T) := Σ_{|γ|≤T}′ [1−(1−1/ρ)ⁿ]! And the contour bounds the DIFFERENCE S_f(n) − λ_n(√n) = O(√n log n), and separately |λ_n(√n)| ≤ 2N(√n) + window slack (via RH-to-T₀ + the e-bound for off-line in the window). So the B(n) accounting (4.1): |S_f| ≤ |λ_n(T)| + |S_f − λ_n(T)| ≤ [2N(T) or 2N(√n) + 4C₀] + [sides + triv + ...]. That's why B(n) has 2F(T) AND the sides but NO Res₁ and NO tail: the tail and Res₁ are both inside the \"S_f − λ_n(T) = contour remainder\" which is bounded by the sides + triv + 1...\n\nHmm wait, but that still leaves the question: what IS S_f(n) mathematically (so that Sf(Lean) = S_f)? From BL Thm 2 it's DEFINED as S_∞ + 1 − λ_n. And Lagarias proves S_f(n) − λ_n(√n) = O(√n log n) — the difference between the full-finite-part and the truncated zero sum. So the contour computes/bounds S_f − λ_n(T), NOT the truncated sum itself. And that difference must involve: tail(T) − Res₁ + triv... let me redo with correct algebra:\n\nSf = S_∞ + 1 − λ_n = S_∞ + 1 − λ_n(T) − tail(T) where λ_n(T) = Σ_{|γ|≤T}[1−(1−1/ρ)ⁿ] (truncated, and by reindexing = Σ_{|γ|≤T}[1−(ρ/(ρ−1))ⁿ] up to the reflect symmetry — careful: reflect maps |γ|≤T to itself ✓ so the truncated set is reflect-invariant and reindexing works exactly).\n\nSf − λ_n(T)?? No: Sf = S_∞ + 1 − λ_n, so S_f − λ_n(T) is not natural; what Lagarias means: S_f(n) = S_∞ + 1 − λ_n. And the contour gives:\nλ_n − λ_n(T) = tail(T), and separately from (∗):\nλ_n(T) = Σ_{|γ|<T}[1−(ρ/(ρ−1))ⁿ] = sides − triv − Res₁.\nSo λ_n = sides − triv − Res₁ + tail.\nSf = S_∞ + 1 − sides + triv + Res₁ − tail.\n\n|Sf| ≤ |λ_n(T)| + |Sf − λ_n(T)|? Lagarias's Thm 6.1: S_f = λ_n(√n) + O(√n log n). So the bound: |S_f| ≤ |λ_n(√n)| + |S_f − λ_n(√n)|, where:\n- |λ_n(√n)| ≤ 2N(√n) + 4C₀-ish (RH bridge + window) — the \"2F(T)\" B(n) term.\n- S_f − λ_n(√n) = [S_∞ + 1 + Res₁ + triv] − sides − tail + [λ_n(T) − λ_n(√n)] — hmm the bracket [S_∞+1+Res₁+triv] is still there!\n\nUNLESS the bracket vanishes identically. At n=1: bracket = −1.554120+1−0.577216+0.333333 = −0.798003. And sides(T=2) at n=1 =? and λ_n(2) = 0 (no zeros below 2). S_f(1) − λ_1(2) = −0.577216 − 0 = −0.577216. My formula: S_f − λ_n(T) = bracket − sides − tail + ... let me recompute: S_f = bracket_A − sides − tail where bracket_A = S_∞+1+Res₁+triv = −0.798003. S_f(1) = −0.577216. So −0.577216 = −0.798003 − sides(2) − tail(2) ⟹ sides(2) + tail(2) = −0.220787. tail(2) = λ_1 − λ_1(2) = λ_1 = 0.023096. sides(2) = −0.243883. Consistency can't be eyeballed, fine.\n\nThe point: bracket_A ≠ 0, so the decomposition \"Sf = bracket_A − sides − tail\" is exact but the bracket is a specific O(1)-ish number at n=1... at general n: bracket_A(n) = S_∞(n) + 1 + Res₁(n) + triv(n). How big is it? At n=2: −1.874539 + 1 − 0.894071 + 0.555556 = −1.213054. Sf(2) = −0.966922 = bracket_A − sides − tail ⟹ sides + tail = −0.246132.\n\nHmm so bracket_A is O(1)-scale at n=1,2 (−0.798, −1.213). Is bracket_A identically small/bounded? What IS bracket_A asymptotically? S_∞(n) ~ ½n log n; Res₁(n) = Σ_j C(n,j)c_{j−1}: leading behavior? c_k are Stieltjes-related; the sum Σ_j C(n,j)c_{j−1} is a binomial transform — if bracket_A stays O(n) or smaller, then S_∞ + Res₁ must cancel the ½n log n term. This is EXACTLY the identification: S_∞(n) + Res₁(n) + 1 + triv(n) = small. Lagarias's (4.11) identity says S_∞(n) = Σ_j (−1)^j C(n,j) a_j with a_j archimedean; and Res₁ = Σ_j C(n,j) c_{j−1}; the identification needed: Σ_j C(n,j)[(−1)^j a_j + c_{j−1}] = −1 − triv(n) + bracket_A(n) with bracket_A SMALL (bounded by the B(n) constant term — e.g. ≤ a few units, absorbed into the \"+1\"-style constants). Is bracket_A(n) maybe EXACTLY 0 for all n? At n=1: −0.798 ≠ 0. So not zero. Is it maybe −λ_n + λ_n(T)+... no...\n\nHmm, hold on — maybe I have the sign of Res₁ wrong. Let me recompute the residue at w=1 of k_n(w−1)(−ζ′/ζ). Res of a pole of order n+1: the product k_n(w−1)·(−ζ′/ζ(w)): k_n(w−1) = Σ_{j=1}^n C(n,j) u^{−j} (u = w−1), −ζ′/ζ = Σ_{k≥−1} c_k u^k with c_{−1} = 1, c_0 = −γ. Product: Σ_j Σ_k C(n,j)c_k u^{k−j}. Residue = coeff of u^{−1}: k − j = −1 ⟹ k = j−1: Σ_{j=1}^n C(n,j) c_{j−1} ✓ as I had.\n\nAt n=1: c_0 = −γ ✓. So Res₁(1) = −γ = −0.577216 = S_f(1)!! And bracket_A(1) = S_∞(1)+1+Res₁(1)+triv(1) = S_f(1) + 1 + triv(1) − λ_1... = −0.577 + 1 + 0.333 − 0.0231·... wait bracket_A = S_∞+1+Res₁+triv = −1.554120+1−0.577216+0.333333 = −0.798003. And S_f(1) = −0.577216. So S_f ≠ bracket stuff... but S_f(1) = Res₁(1) EXACTLY (both −γ). Interesting!!\n\nAt n=2: S_f(2) = −0.966922 vs Res₁(2) = −0.894071. NOT equal. Difference −0.072851. Hmm so S_f(1) = Res₁(1) but S_f(2) ≠ Res₁(2).\n\nWhat's triv(2)? = 1−(2/3)² = 0.5556. Res₁(2) + triv-ish... −0.894071 + 0.072816(γ₁)... hmm.\n\nWhat if S_f(n) = Res₁(n) + Σ_{trivial zeros ρ_t}[1−(ρ_t/(ρ_t−1))ⁿ] with the trivial sum understood via ITS OWN archimedean regularization... The trivial sum Σ_k[1−(2k/(2k+1))ⁿ] diverges, but its \"finite part\"... At n=1 the finite part of Σ 1/(2k+1) relates to log 2-ish not −γ...\n\nI'm clearly not going to rediscover the exact BL bookkeeping by numerology. The right move: READ BL Thm 2's actual statement (we have \"BL-1999-fulltext.txt\" and \"Theorem-2.txt\" in research/paper/!). Let me read those.","signature":""},{"type":"text","text":"D-032 gives the key: \"Thm 6.1: S_f(n) = λ_n(√n) + O(√n log n)\". Let me read the actual BL Thm 2 statement from the archived text to pin the decomposition exactly."},{"type":"tool_use","id":"Bash_41","name":"Bash","input":{"command":"wc -l /d/Python/Quantum/research/paper/BL-1999-fulltext.txt /d/Python/Quantum/research/paper/Theorem-2.txt 2>/dev/null; grep -n \"S_\\\\\\\\infty\\|S_f\\|Theorem 2\" /d/Python/Quantum/research/paper/Theorem-2.txt | head -20","description":"Check BL text files and Theorem 2 content"},"extra_content":null}]