← Session 30 — ii′-5e squeeze capstone + 5f perimeter repair
thinking (388 chars)
LiContour builds with the two new perimeter declarations. Now write D-069 (the 5f design doc), then commit this sub-stage (5f-0: design + perimeter declarations), then continue with 5f-i.
Let me write D-069 concisely but completely: Finding 1 (piece-2 gap), Finding 2 (H(T) — ii′-6 repair map), the two declarations, the honest assembly arithmetic, the piece plan, and the sub-stage map.
LiContour green with both declarations. Writing the D-069 design doc.
tool: Write
input
{
"file_path": "D:\\Python\\Quantum\\research\\derivations\\D-069-ii-prime-5f-design.md",
"content": "# D-069 \u2014 ii\u2032-5f design: the tight R-bound in Lean (D-056's Theorem R)\nDate: 2026-08-23 | Session: 035 | Task: 5.1 tier ii\u2032-5f\nStatus: DESIGN COMPLETE; two perimeter additions (P1, P2) APPROVED by the\nuser 2026-08-23 and declared (LiContour.lean, session-035 commit).\n\n## 0. Target\n\nD-056's Theorem R, in the LiDisc-capstone shape:\n \u2016logDeriv \u03b6 s \u2212 \u03a3_{\u03c1 \u2208 nearZeros t} m_\u03c1/(s\u2212\u03c1)\u2016 \u2264 10.5\u00b7log(|t|+2) + 48\nfor s = \u03c3 + it, \u03c3 \u2208 [\u22125/2, 3], |t| \u2265 10, s off the excluded set \u2014 from\n`partialFraction_identity` (5e-v-d) at s vs the reference point\ns\u2080 = 2 + it (B cancels; no evaluation of B needed).\n\n## 1. Finding 1 (session 035): D-056's piece 2 undercounts the near window\n\nD-056's assembly charges the near sum \u03a3_{|\u03b3\u2212t|<1} 1/|s\u2080\u2212\u03c1| ONE unit-window\ncount C\u2080(t), but |\u03b3\u2212t| < 1 spans TWO unit windows. Two honest routes:\n- **per-unit perimeter (even mult-weighted)**: \u03a3 \u2264 \u0108\u2080(t) + \u0108\u2080(t+1) \u2264\n 2\u00b7\u0108\u2080(t+1) = 0.866\u00b7L + 1.772\u00b7LL + 5.8 \u2014 the fold becomes \u2248 11.2\u00b7L + 51,\n BREAKING the baked 10.5/48 constants (they were derived from the\n one-C\u2080 piece 2).\n- **Trudgian F/S-pair applied to the two-unit window directly** (N(t+1)\n \u2212 N(t\u22121)): the S_b-pair does NOT double vs the one-unit form, giving\n \u2264 0.59231\u00b7L + 0.886\u00b7LL + 2.591. With this the full honest assembly is\n 6.111\u00b7L + 12.163\u00b7LL + 47.6 \u2264 10.5\u00b7L + 48 \u2014 **FITS**, worst point the\n loglog pinch at t \u2248 13.1 (L = e, margin \u2248 0.15\u20130.4; see \u00a73).\n\nConclusion: the 10.5/48 constants survive, but ONLY via the two-unit\nform, which is NOT derivable from the per-unit perimeter \u27f9 new declared\nspecialization **(P1) `ZeroCountProp2`** (approved; LiContour.lean).\n\nThis is a D-054-class assembly slip (paper-side; the BOUND is true \u2014\nE-028 measured 26\u00d7 slack; the traced constants needed the sharper\ncount form). Erratum to D-056 \u00a72 piece 2 recorded here.\n\n## 2. The two perimeter additions (approved 2026-08-23)\n\n- **(P1) `ZeroCountProp2`**: \u2200 t \u2265 10, the mult-weighted count of zeros\n with |\u03b3\u2212t| \u2264 1 is \u2264 0.6\u00b7log(t+2) + 0.886\u00b7log log(t+2) + 2.7. Honesty\n check: the F/S-pair gives \u2264 0.59231\u00b7L + 0.886\u00b7LL + 2.591 (F-diff \u2264\n (1/\u03c0)(L \u2212 log 2\u03c0); S_b-pair \u2264 0.274\u00b7L + 0.886\u00b7LL + 3.176), so the\n closed form has 0.008\u00b7L + 0.109 slack. Same source as `ZeroCountProp`\n (Trudgian 2014 N(T)/S(T), D-062 \u00a74 class).\n- **(P2) `NoLowZeros`**: no nontrivial zeros with |\u03b3| \u2264 14 (first zero\n 14.1347\u2026). This is the zero-LOCATION content of the Platt\u2013Trudgian-class\n Turing-method certificate \u2014 NOT implied by `RHUpTo` (on-line only) nor\n by the count bounds (S_b slack \u226b 1 at low height). Piece 3 consumes it:\n the far sum's intervals below height 14 are otherwise only symbolically\n bounded (Jensen gives \u2248 3.25 vs the true 0 \u2014 breaks the constants at\n the t = 10 pinch).\n\nPaper-ii\u2032-7 duty: the appendix's perimeter list gains these two items\n(same trust classes as the existing entries).\n\n## 3. The honest assembly (the fold)\n\nWith L = log(t+2), LL = log L, C\u2080 := \u0108\u2080(t+1) = 0.433\u00b7L\u2032 + 0.886\u00b7LL\u2032 + 2.9\n(L\u2032 = log(t+3) \u2264 L + 1/12):\n1. \u2016\u03b6\u2032/\u03b6(s\u2080)\u2016 \u2264 dirichletC2 \u2264 0.995 (\u039b(n) \u2264 log n \u27f9 \u2264 \u03a3_{n\u22652} log n/n\u00b2\n \u2264 (log 2)/4 + (log 3)/9 + \u222b\u2083^\u221e log x/x\u00b2 dx = (log 2)/4 + (log 3)/9 +\n (log 3 + 1)/3 \u2248 0.1733 + 0.1221 + 0.6995 = 0.9949; budget 1.01).\n2. near \u2264 P1-count \u2264 0.6\u00b7L + 0.886\u00b7LL + 2.7 (|s\u2080\u2212\u03c1| \u2265 1 since re \u03c1 \u2264 1).\n3. far \u2264 4.5\u221a2\u00b7[C\u2080 + (C\u2080 + 0.55) + 0.55] = 12.7279\u00b7C\u2080 + 7.00\n (per-interval |s\u2080\u2212s| \u2264 4.5, |s\u2212\u03c1| \u2265 x, |s\u2080\u2212\u03c1| \u2265 (1+x)/\u221a2 with\n x = |t\u2212\u03b3|; \u03a3_{k\u22651} 1/(k(k+1)) = 1; C\u2080(2t+1) \u2264 C\u2080 + 0.55; the k > t\n tail \u2264 0.55 via \u03a3_{k\u226511} log k/k\u00b2 \u2264 (log 10 + 1)/10 \u2264 0.331 and\n \u03a3 1/(k(k+1)) \u2264 1/11; the height-< 14 intervals empty by P2; the\n negative-\u03b3 side via conjugation).\n4./5. \u20161/s \u2212 1/s\u2080\u2016, \u20161/(s\u22121) \u2212 1/(s\u2080\u22121)\u2016 \u2264 4.5/|t|\u00b2 \u2264 0.045 each.\n6. \u00bd\u2016\u03c8(s/2) \u2212 \u03c8(s\u2080/2)\u2016 \u2264 0.30 (sharp digamma remainder |r(w)| \u2264\n 1.2/|w|\u00b2 via the level-2 EM (LiRBound b2Fun machinery) \u2014 the Lean\n Lemma D; |log(w/w\u2080)| \u2264 0.45\u00b7(1+\u03b5) via the arg/modulus split).\nTotal: 6.111\u00b7L + 12.163\u00b7LL + 47.6 \u2264 10.5\u00b7L + 48 \u27fa\n12.163\u00b7LL \u2212 4.389\u00b7L \u2264 0.4, and max over L \u2265 log 12 is at L* = 12.163/4.389\n= 2.772 with value 12.163\u00b7log(2.772) \u2212 4.389\u00b72.772 \u2248 0.234 \u2264 0.4 \u2713\n(the pinch lemma: one-variable calculus + certified endpoint/point\nevaluation, LiBasePoints pattern).\n\n## 4. Finding 2 (session 035; ii\u2032-6 repair map \u2014 NOT 5f scope)\n\nD-036 \u00a72's H(T) = 3\u00b7\u0108\u2080\u00b2 + A\u00b7log + B\u2080 charges the horizontal-contour near\nsum (i) one unit-window count (Finding-1 issue again \u2014 the two-unit form\nfixes this part cheaply) and (ii) L3's clearance 1/(3\u00b7\u0108\u2080), which covers\nonly zeros INSIDE the pigeonhole window: with T \u2208 [a, a+1], zeros just\noutside [a, a+1] can sit at distance < 1/(3\u0108\u2080) from T. Honest repair:\nextend the pigeonhole to the 3-unit window (a\u22121, a+2) (count \u2264 3\u00b7\u0108\u2080,\nclearance \u2265 1/(7\u00b7\u0108\u2080)-ish) and split the near sum at |\u03b3\u2212T| = 1/4:\n\u03a3 \u2264 \u0108\u2080\u00b77\u0108\u2080 + 2\u0108\u2080\u00b74 = 7\u00b7\u0108\u2080\u00b2 + 8\u00b7\u0108\u2080. Impact: marginTilde's baked\n3\u00b7\u0108\u2080\u00b2 coefficient moves to \u2248 7 + o(1); the margin at the certified base\npoints drops by \u2248 2(e\u2074+1)\u00b77\u00b74\u00b7\u0108\u2080\u00b2 (\u2248 1.5\u00d710\u2075 at n = 8\u00d710\u2074) \u2014 the\ncrossover N\u2080 moves up (estimate: within [10\u2075, 5\u00d710\u2075], still under the\nfinite-verification cap); the convexity proof is structural and\nre-verifies. TO BE FACED at ii\u2032-6 (D-037's I_III (2/3)\u00b7\u0108\u2080 coefficient\ngets the analogous two-unit correction to (4/3)-ish). File under the\n4.5-class repair map. E-028's 26\u00d7 slack says the theorem survives; the\ncertified crossover artifacts move.\n\n## 5. Lean build plan (sub-stages)\n\n- **5f-0** (session 035, DONE): this design + P1/P2 declarations\n (LiContour.lean: `zeroAbsWindow`, `zeroAbsWindow_finite`,\n `ZeroCountProp2`, `NoLowZeros`) + the mult-weighted `ZeroCountProp`\n repair (`one_le_zeroMult`; consumer adaptations in\n exists_zero_avoiding_T, exists_gapCircle_radius).\n- **5f-i**: the reference-point difference identity (from\n partialFraction_identity; seriesFun difference termwise + the\n near/far split via tsum_split_finset + the nearZeros subtype bridge) +\n the elementary pieces 1 (dirichletC2 \u2264 0.995 via \u039b \u2264 log + integral\n comparison), 2 (P1 count \u00d7 |s\u2080\u2212\u03c1| \u2265 1), 4, 5 (norm algebra).\n- **5f-ii**: piece 6 (the sharp digamma remainder |r| \u2264 1.2/|w|\u00b2 via\n the level-2 EM; then the log-difference arg/modulus split) and\n piece 3 (the far-sum interval machine: per-interval C0hat counts from\n the perimeter + conj for the negative side + P2 for the low intervals\n + the \u03a3 1/(k(k+1)) = 1 telescoping sum).\n- **5f-iii**: the assembly + the pinch lemma (12.163\u00b7LL \u2264 4.389\u00b7L +\n const for L \u2265 log 12 via the interior-max calculus) + the capstone\n `logDeriv_riemannZeta_sub_nearZeros_le_tight` + audit.\n\nCapstone statement (5f-iii; t \u2265 10 first, the t \u2264 \u221210 corollary via\nconjugation if ii\u2032-6's bottom horizontal needs it \u2014 TBD there):\n theorem logDeriv_riemannZeta_sub_nearZeros_le_tight\n (hZC : ZeroCountProp) (hZC2 : ZeroCountProp2) (hNLZ : NoLowZeros)\n {t : \u211d} (ht : 10 \u2264 t) {s : \u2102}\n (h\u03c3 : -5/2 \u2264 s.re \u2227 s.re \u2264 3) (him : s.im = t)\n (h\u03b6 : riemannZeta s \u2260 0) :\n \u2016logDeriv riemannZeta s\n - \u2211 \u03c1 \u2208 nearZeros t, (zeroMult \u03c1 : \u2102) / (s - \u03c1)\u2016\n \u2264 10.5 * Real.log (|t| + 2) + 48\n\n## 6. Risks\n- Piece 3 is the longest piece (the interval machine; LiCircleBound-shell\n flavor \u2014 1\u20131.5 sessions alone).\n- The pinch lemma's margin is \u2248 0.15\u20130.4 \u2014 certifiable but tight; every\n piece constant must keep its budget (piece 1 \u2264 1.01, piece 6 \u2264 0.30).\n- The digamma EM remainder sign conventions (b2Fun) need care.\n"
}
raw content_json (database row)
[{"type":"thinking","thinking":"LiContour builds with the two new perimeter declarations. Now write D-069 (the 5f design doc), then commit this sub-stage (5f-0: design + perimeter declarations), then continue with 5f-i.\n\nLet me write D-069 concisely but completely: Finding 1 (piece-2 gap), Finding 2 (H(T) — ii′-6 repair map), the two declarations, the honest assembly arithmetic, the piece plan, and the sub-stage map.","signature":""},{"type":"text","text":"LiContour green with both declarations. Writing the D-069 design doc."},{"type":"tool_use","id":"Write_127","name":"Write","input":{"file_path":"D:\\Python\\Quantum\\research\\derivations\\D-069-ii-prime-5f-design.md","content":"# D-069 — ii′-5f design: the tight R-bound in Lean (D-056's Theorem R)\nDate: 2026-08-23 | Session: 035 | Task: 5.1 tier ii′-5f\nStatus: DESIGN COMPLETE; two perimeter additions (P1, P2) APPROVED by the\nuser 2026-08-23 and declared (LiContour.lean, session-035 commit).\n\n## 0. Target\n\nD-056's Theorem R, in the LiDisc-capstone shape:\n ‖logDeriv ζ s − Σ_{ρ ∈ nearZeros t} m_ρ/(s−ρ)‖ ≤ 10.5·log(|t|+2) + 48\nfor s = σ + it, σ ∈ [−5/2, 3], |t| ≥ 10, s off the excluded set — from\n`partialFraction_identity` (5e-v-d) at s vs the reference point\ns₀ = 2 + it (B cancels; no evaluation of B needed).\n\n## 1. Finding 1 (session 035): D-056's piece 2 undercounts the near window\n\nD-056's assembly charges the near sum Σ_{|γ−t|<1} 1/|s₀−ρ| ONE unit-window\ncount C₀(t), but |γ−t| < 1 spans TWO unit windows. Two honest routes:\n- **per-unit perimeter (even mult-weighted)**: Σ ≤ Ĉ₀(t) + Ĉ₀(t+1) ≤\n 2·Ĉ₀(t+1) = 0.866·L + 1.772·LL + 5.8 — the fold becomes ≈ 11.2·L + 51,\n BREAKING the baked 10.5/48 constants (they were derived from the\n one-C₀ piece 2).\n- **Trudgian F/S-pair applied to the two-unit window directly** (N(t+1)\n − N(t−1)): the S_b-pair does NOT double vs the one-unit form, giving\n ≤ 0.59231·L + 0.886·LL + 2.591. With this the full honest assembly is\n 6.111·L + 12.163·LL + 47.6 ≤ 10.5·L + 48 — **FITS**, worst point the\n loglog pinch at t ≈ 13.1 (L = e, margin ≈ 0.15–0.4; see §3).\n\nConclusion: the 10.5/48 constants survive, but ONLY via the two-unit\nform, which is NOT derivable from the per-unit perimeter ⟹ new declared\nspecialization **(P1) `ZeroCountProp2`** (approved; LiContour.lean).\n\nThis is a D-054-class assembly slip (paper-side; the BOUND is true —\nE-028 measured 26× slack; the traced constants needed the sharper\ncount form). Erratum to D-056 §2 piece 2 recorded here.\n\n## 2. The two perimeter additions (approved 2026-08-23)\n\n- **(P1) `ZeroCountProp2`**: ∀ t ≥ 10, the mult-weighted count of zeros\n with |γ−t| ≤ 1 is ≤ 0.6·log(t+2) + 0.886·log log(t+2) + 2.7. Honesty\n check: the F/S-pair gives ≤ 0.59231·L + 0.886·LL + 2.591 (F-diff ≤\n (1/π)(L − log 2π); S_b-pair ≤ 0.274·L + 0.886·LL + 3.176), so the\n closed form has 0.008·L + 0.109 slack. Same source as `ZeroCountProp`\n (Trudgian 2014 N(T)/S(T), D-062 §4 class).\n- **(P2) `NoLowZeros`**: no nontrivial zeros with |γ| ≤ 14 (first zero\n 14.1347…). This is the zero-LOCATION content of the Platt–Trudgian-class\n Turing-method certificate — NOT implied by `RHUpTo` (on-line only) nor\n by the count bounds (S_b slack ≫ 1 at low height). Piece 3 consumes it:\n the far sum's intervals below height 14 are otherwise only symbolically\n bounded (Jensen gives ≈ 3.25 vs the true 0 — breaks the constants at\n the t = 10 pinch).\n\nPaper-ii′-7 duty: the appendix's perimeter list gains these two items\n(same trust classes as the existing entries).\n\n## 3. The honest assembly (the fold)\n\nWith L = log(t+2), LL = log L, C₀ := Ĉ₀(t+1) = 0.433·L′ + 0.886·LL′ + 2.9\n(L′ = log(t+3) ≤ L + 1/12):\n1. ‖ζ′/ζ(s₀)‖ ≤ dirichletC2 ≤ 0.995 (Λ(n) ≤ log n ⟹ ≤ Σ_{n≥2} log n/n²\n ≤ (log 2)/4 + (log 3)/9 + ∫₃^∞ log x/x² dx = (log 2)/4 + (log 3)/9 +\n (log 3 + 1)/3 ≈ 0.1733 + 0.1221 + 0.6995 = 0.9949; budget 1.01).\n2. near ≤ P1-count ≤ 0.6·L + 0.886·LL + 2.7 (|s₀−ρ| ≥ 1 since re ρ ≤ 1).\n3. far ≤ 4.5√2·[C₀ + (C₀ + 0.55) + 0.55] = 12.7279·C₀ + 7.00\n (per-interval |s₀−s| ≤ 4.5, |s−ρ| ≥ x, |s₀−ρ| ≥ (1+x)/√2 with\n x = |t−γ|; Σ_{k≥1} 1/(k(k+1)) = 1; C₀(2t+1) ≤ C₀ + 0.55; the k > t\n tail ≤ 0.55 via Σ_{k≥11} log k/k² ≤ (log 10 + 1)/10 ≤ 0.331 and\n Σ 1/(k(k+1)) ≤ 1/11; the height-< 14 intervals empty by P2; the\n negative-γ side via conjugation).\n4./5. ‖1/s − 1/s₀‖, ‖1/(s−1) − 1/(s₀−1)‖ ≤ 4.5/|t|² ≤ 0.045 each.\n6. ½‖ψ(s/2) − ψ(s₀/2)‖ ≤ 0.30 (sharp digamma remainder |r(w)| ≤\n 1.2/|w|² via the level-2 EM (LiRBound b2Fun machinery) — the Lean\n Lemma D; |log(w/w₀)| ≤ 0.45·(1+ε) via the arg/modulus split).\nTotal: 6.111·L + 12.163·LL + 47.6 ≤ 10.5·L + 48 ⟺\n12.163·LL − 4.389·L ≤ 0.4, and max over L ≥ log 12 is at L* = 12.163/4.389\n= 2.772 with value 12.163·log(2.772) − 4.389·2.772 ≈ 0.234 ≤ 0.4 ✓\n(the pinch lemma: one-variable calculus + certified endpoint/point\nevaluation, LiBasePoints pattern).\n\n## 4. Finding 2 (session 035; ii′-6 repair map — NOT 5f scope)\n\nD-036 §2's H(T) = 3·Ĉ₀² + A·log + B₀ charges the horizontal-contour near\nsum (i) one unit-window count (Finding-1 issue again — the two-unit form\nfixes this part cheaply) and (ii) L3's clearance 1/(3·Ĉ₀), which covers\nonly zeros INSIDE the pigeonhole window: with T ∈ [a, a+1], zeros just\noutside [a, a+1] can sit at distance < 1/(3Ĉ₀) from T. Honest repair:\nextend the pigeonhole to the 3-unit window (a−1, a+2) (count ≤ 3·Ĉ₀,\nclearance ≥ 1/(7·Ĉ₀)-ish) and split the near sum at |γ−T| = 1/4:\nΣ ≤ Ĉ₀·7Ĉ₀ + 2Ĉ₀·4 = 7·Ĉ₀² + 8·Ĉ₀. Impact: marginTilde's baked\n3·Ĉ₀² coefficient moves to ≈ 7 + o(1); the margin at the certified base\npoints drops by ≈ 2(e⁴+1)·7·4·Ĉ₀² (≈ 1.5×10⁵ at n = 8×10⁴) — the\ncrossover N₀ moves up (estimate: within [10⁵, 5×10⁵], still under the\nfinite-verification cap); the convexity proof is structural and\nre-verifies. TO BE FACED at ii′-6 (D-037's I_III (2/3)·Ĉ₀ coefficient\ngets the analogous two-unit correction to (4/3)-ish). File under the\n4.5-class repair map. E-028's 26× slack says the theorem survives; the\ncertified crossover artifacts move.\n\n## 5. Lean build plan (sub-stages)\n\n- **5f-0** (session 035, DONE): this design + P1/P2 declarations\n (LiContour.lean: `zeroAbsWindow`, `zeroAbsWindow_finite`,\n `ZeroCountProp2`, `NoLowZeros`) + the mult-weighted `ZeroCountProp`\n repair (`one_le_zeroMult`; consumer adaptations in\n exists_zero_avoiding_T, exists_gapCircle_radius).\n- **5f-i**: the reference-point difference identity (from\n partialFraction_identity; seriesFun difference termwise + the\n near/far split via tsum_split_finset + the nearZeros subtype bridge) +\n the elementary pieces 1 (dirichletC2 ≤ 0.995 via Λ ≤ log + integral\n comparison), 2 (P1 count × |s₀−ρ| ≥ 1), 4, 5 (norm algebra).\n- **5f-ii**: piece 6 (the sharp digamma remainder |r| ≤ 1.2/|w|² via\n the level-2 EM; then the log-difference arg/modulus split) and\n piece 3 (the far-sum interval machine: per-interval C0hat counts from\n the perimeter + conj for the negative side + P2 for the low intervals\n + the Σ 1/(k(k+1)) = 1 telescoping sum).\n- **5f-iii**: the assembly + the pinch lemma (12.163·LL ≤ 4.389·L +\n const for L ≥ log 12 via the interior-max calculus) + the capstone\n `logDeriv_riemannZeta_sub_nearZeros_le_tight` + audit.\n\nCapstone statement (5f-iii; t ≥ 10 first, the t ≤ −10 corollary via\nconjugation if ii′-6's bottom horizontal needs it — TBD there):\n theorem logDeriv_riemannZeta_sub_nearZeros_le_tight\n (hZC : ZeroCountProp) (hZC2 : ZeroCountProp2) (hNLZ : NoLowZeros)\n {t : ℝ} (ht : 10 ≤ t) {s : ℂ}\n (hσ : -5/2 ≤ s.re ∧ s.re ≤ 3) (him : s.im = t)\n (hζ : riemannZeta s ≠ 0) :\n ‖logDeriv riemannZeta s\n - ∑ ρ ∈ nearZeros t, (zeroMult ρ : ℂ) / (s - ρ)‖\n ≤ 10.5 * Real.log (|t| + 2) + 48\n\n## 6. Risks\n- Piece 3 is the longest piece (the interval machine; LiCircleBound-shell\n flavor — 1–1.5 sessions alone).\n- The pinch lemma's margin is ≈ 0.15–0.4 — certifiable but tight; every\n piece constant must keep its budget (piece 1 ≤ 1.01, piece 6 ≤ 0.30).\n- The digamma EM remainder sign conventions (b2Fun) need care.\n"},"extra_content":null}]