← Session 22 — ii′-1: liCoeff pairing fix + residue machinery
thinking (1856 chars)
- `neg_pow (a : R) (n : ℕ) : (-a)^n = (-1)^n * a^n` — root-level (after `variable {R}`, in the root namespace section of Commute.lean) ✓ bare `neg_pow`.
- `pow_le_pow_of_le_one (ha₀ : 0 ≤ a) (ha₁ : a ≤ 1) {m n : ℕ} (h : m ≤ n) : a^n ≤ a^m` — GroupWithZero/Basic.lean:393 ✓ root-level presumably (in some namespace? the file Mathlib/Algebra/Order/GroupWithZero/Basic.lean — likely root). So: for 0 ≤ a ≤ 1 and 2 ≤ j: a^j ≤ a^2 via pow_le_pow_of_le_one h0 h1 (show 2 ≤ j) ✓.
Let me check the full statement of pow_le_pow_of_le_one (line 393): `lemma pow_le_pow_of_le_one [PosMulMono M₀] (ha₀ : 0 ≤ a) (ha₁ : a ≤ 1) {m n : ℕ} (h : m ≤ n) : a ^ n ≤ a ^ m` ✓.
All names confirmed. Now write LiSwaps.lean. Plan the file:
```
NguyenRH1/LiSwaps.lean — tier ii′ sub-stage ii′-2 (D-064 §4 R2):
the two elementary swaps.
Part 1 (R2(i)): liCoeff n = Σ_{j=1}^n (−1)^{j+1} C(n,j) σ_j
Part 2 (R2(ii)): SInfty n = Σ_{j=1}^n (−1)^j C(n,j) a_j
Shared: one_sub_one_sub_pow (CommRing-polymorphic binomial expansion),
sum_Icc_one_eq_sum_range / sum_Icc_two_eq_sum_range (bespoke conversions).
```
Order of lemmas:
§0 helpers: sum_Icc_one_eq_sum_range, sum_Icc_two_eq_sum_range, sum_Icc_one_eq_add_sum_Icc_two, one_sub_one_sub_pow.
§1 (R2(i)): sigmaSlice, sigmaP, sigmaSlice_norm_le (j=1 paired / j≥2), sigmaSlice_summable, liSummand_eq_sum_slices, liCoeff_eq_sum_sigma.
§2 (R2(ii)): lagariasA, oddSlice_summable, sInfty_summand_eq, sum_Icc_two_neg_one_choose, sInfty_eq_sum.
Let me also double-check the SInfty definition's exact text so my `show` matches. From the grep at line 380-383:
```
def SInfty (n : ℕ) : ℝ :=
(1 - lagariasA1) * n - 1 +
tsum fun m: {m : ℕ // Odd m ∧ 3 ≤ m} =>
((1 - 1 \ (m: ℝ)) ^ n - 1 + (n : ℝ) / (m : ℝ))
```
The `\` in the grep output is likely `/` in the file (the grep output escaping is suspicious). Let me read the exact lines.
All names verified. Let me check SInfty's exact syntax before writing.
tool: Read ok
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean",
"offset": 374,
"limit": 20
}
result 2026-08-22 03:39:39Z → 2026-08-24 07:31:00Z
{
"type": "text",
"file": {
"filePath": "D:\\Python\\Quantum\\research\\derivations\\D-036-zeta-contour-constants.md",
"content": "## 2. Zero-avoiding height T\nZeros in [\u221an, \u221an+1]: \u2264 C\u2080(\u221an+1). Pigeonhole: some gap \u2265 1/(C\u2080+1);\nchoose T at a gap center \u27f9 distance to nearest zero\n **d_min \u2265 1/(3C\u2080(\u221an+1))**.\nThen on the horizontal segments:\n |\u03b6\u2032/\u03b6(s)| \u2264 C\u2080(T)/d_min + A log(T+2) + B\u2080\n **\u2264 3C\u2080(T)\u00b2 + A log(T+2) + B\u2080 =: H(T)** = O((log T)\u00b2).\n\n## 3. Segment bounds (kernel \u00d7 |\u03b6\u2032/\u03b6| \u00d7 length)\n- **(III) left vertical \u03c3\u2080 = \u22125/2** (length 2T): |1+1/s|\u00b2 = 1 +\n (2\u03c3+1)/|s|\u00b2 \u2264 1 (\u03c3 \u2264 \u22121/2) \u27f9 |k_n| \u2264 2. Nearest nontrivial zeros have\n |\u03c3\u2212\u03b2| \u2265 1.5 \u27f9 |\u03b6\u2032/\u03b6| \u2264 (2/3)C\u2080(T) + A log(T+2) + B\u2080. Trivial zero\n \u03c1 = \u22122 is the only one inside (residue \u2264 1).\n |I_III| \u2264 2\u00b7[(2/3)C\u2080(T) + A]\u00b7log(T+2)\u00b72T + 2\u00b7B\u2080\u00b72T\n \u2264 4T[(2/3)C\u2080(T) + A] log(T+2) + 4B\u2080T.\n With T = \u221an, A = 2: **|I_III| \u2264 4.7 \u221an log n + lower order**\n (dominant term).\n- **(II),(IV) horizontals**: |1+1/s| \u2264 1 + (\u03c3+1)/(\u03c3\u00b2+T\u00b2) \u27f9 |k_n| \u2264\n (1+4/(16+n))\u207f + 1 \u2264 e\u2074 + 1 (\u22123 \u2264 \u03c3 \u2264 3); \u03c3 \u2208 [3, 2\u221an]: stepping\n (6.12): each unit step right gains factor 2 on |\u03b6\u2032/\u03b6| while\n |k_n(s+1)+1|/|k_n(s)+1| \u2264 e \u27f9 geometric sum \u2264 e\u00b7|\u03b6\u2032/\u03b6(3+iT)|\u00b7(e\u2074+1).\n |I_II| = |I_IV| \u2264 (e\u2074+1)\u00b7[7H(T) + e\u00b7|\u03b6\u2032/\u03b6(2)|\u00b72] \u2264 (e\u2074+1)\u00b7[7H(T) + 3.3].\n **\u2264 57\u00b77\u00b7(3C\u2080\u00b2 + A log + B\u2080) = O((log n)\u00b2)** \u2014 negligible vs (III).\n- **(I) right vertical \u03c3\u2081 = 2\u221an** (length 2T): |\u03b6\u2032/\u03b6| \u2264\n 2^{-(\u03c3\u2081\u22122)}\u00b7|\u03b6\u2032/\u03b6(2)| = 2^{-(2\u221an\u22122)}\u00b70.5699; |k_n| \u2264 e^{\u221an/2} + 1.\n **|I_I| \u2264 2\u221an\u00b7(e^{\u221an/2}+1)\u00b70.57\u00b72^{-(2\u221an\u22122)} = o(1)** (explicitly\n \u2264 10^{-0.3\u221an}\u00b74\u221an).\n- **Trivial zeros**: only \u03c1 = \u22122 inside; |(1+1/(\u22122))\u207f \u2212 1| =\n 1 \u2212 2^{\u2212n} \u2264 1. **Contribution \u2264 1.**\n- **Height-window slack** (T \u2212 \u221an < 1): |\u03bb_n(\u221an) \u2212 \u03bb_n(T)| \u2264\n 2\u00b7C\u2080(T)\u00b72 = 4C\u2080(T) (each of \u2264 C\u2080 zeros contributes \u2264 2).\n\n## 4. Assembled bound (with RH verified to height T\u2080)\nFor \u221an + 1 \u2264 T\u2080 (i.e. n \u2264 (T\u2080\u22121)\u00b2), all zeros of \u03bb_n(\u221an) are on the\nline \u27f9 each contributes \u2264 2:\n |\u03bb_n(\u221an)| \u2264 2N(\u221an) \u2264 2F(\u221an) + 2S(\u221an)\n \u2248 (\u221an/\u03c0) log(\u221an/2\u03c0e) + 0.274 log n\u00b7\u2026 \nTherefore\n **|S_f(n)| \u2264 2N(\u221an) + 4C\u2080(\u221an+1) + |I_I| + |I_II| + |I_IV| + |I_III| + 1**\n **\u2264 C\u2081\u221an log n + C\u2082\u221an + C\u2083 log\u00b2n + C\u2084 log n + C\u2085**",
"numLines": 40,
"startLine": 54,
"totalLines": 136
}
}
raw content_json (database row)
[{"type":"thinking","thinking":"- `neg_pow (a : R) (n : ℕ) : (-a)^n = (-1)^n * a^n` — root-level (after `variable {R}`, in the root namespace section of Commute.lean) ✓ bare `neg_pow`.\n- `pow_le_pow_of_le_one (ha₀ : 0 ≤ a) (ha₁ : a ≤ 1) {m n : ℕ} (h : m ≤ n) : a^n ≤ a^m` — GroupWithZero/Basic.lean:393 ✓ root-level presumably (in some namespace? the file Mathlib/Algebra/Order/GroupWithZero/Basic.lean — likely root). So: for 0 ≤ a ≤ 1 and 2 ≤ j: a^j ≤ a^2 via pow_le_pow_of_le_one h0 h1 (show 2 ≤ j) ✓.\n\nLet me check the full statement of pow_le_pow_of_le_one (line 393): `lemma pow_le_pow_of_le_one [PosMulMono M₀] (ha₀ : 0 ≤ a) (ha₁ : a ≤ 1) {m n : ℕ} (h : m ≤ n) : a ^ n ≤ a ^ m` ✓.\n\nAll names confirmed. Now write LiSwaps.lean. Plan the file:\n\n```\nNguyenRH1/LiSwaps.lean — tier ii′ sub-stage ii′-2 (D-064 §4 R2):\nthe two elementary swaps.\n\nPart 1 (R2(i)): liCoeff n = Σ_{j=1}^n (−1)^{j+1} C(n,j) σ_j\nPart 2 (R2(ii)): SInfty n = Σ_{j=1}^n (−1)^j C(n,j) a_j\nShared: one_sub_one_sub_pow (CommRing-polymorphic binomial expansion),\nsum_Icc_one_eq_sum_range / sum_Icc_two_eq_sum_range (bespoke conversions).\n```\n\nOrder of lemmas:\n§0 helpers: sum_Icc_one_eq_sum_range, sum_Icc_two_eq_sum_range, sum_Icc_one_eq_add_sum_Icc_two, one_sub_one_sub_pow.\n§1 (R2(i)): sigmaSlice, sigmaP, sigmaSlice_norm_le (j=1 paired / j≥2), sigmaSlice_summable, liSummand_eq_sum_slices, liCoeff_eq_sum_sigma.\n§2 (R2(ii)): lagariasA, oddSlice_summable, sInfty_summand_eq, sum_Icc_two_neg_one_choose, sInfty_eq_sum.\n\nLet me also double-check the SInfty definition's exact text so my `show` matches. From the grep at line 380-383:\n```\ndef SInfty (n : ℕ) : ℝ :=\n (1 - lagariasA1) * n - 1 +\n tsum fun m: {m : ℕ // Odd m ∧ 3 ≤ m} =>\n ((1 - 1 \\ (m: ℝ)) ^ n - 1 + (n : ℝ) / (m : ℝ))\n```\nThe `\\` in the grep output is likely `/` in the file (the grep output escaping is suspicious). Let me read the exact lines.","signature":""},{"type":"text","text":"All names verified. Let me check SInfty's exact syntax before writing."},{"type":"tool_use","id":"Read_114","name":"Read","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean","offset":374,"limit":20},"extra_content":null}]