← Session 33 — ii′-3b/3c crux + F-D finding; Lagarias letter package
thinking (125 chars)
All 12 audited: 3 standard axioms only, 0 sorryAx; both perimeter Props printed verbatim. ii′-6-b COMPLETE. Archive + commit.
All clean (12 decls, 3 standard axioms, 0 sorryAx; both perimeter Props verbatim). **ii′-6-b COMPLETE.** Closing the archive.
tool: Bash
input
{
"command": "cd D:/Python/Quantum && cat >> research/journal/session-038.md << 'EOF'\n\n## ii\u2032-6-b COMPLETE (same session, fourth continuation) \u2014 the assembly pieces\n\n**LiContour.lean additions** (builds green): the two user-approved\nperimeter Props \u2014 `ZeroCountGlobalProp` (\u2200 T \u2265 2, mult-weighted\none-sign count with 0 < \u03b3 \u2264 T \u2264 FAlt T; zeroGlobalWindow +\nzeroGlobalWindow_finite) and `MZeroProp` (\u2200 |t| \u2264 10, \u2016logDeriv \u03b6\n(\u22125/2 + t\u00b7I)\u2016 \u2264 1.3352) \u2014 plus the **wide pigeonhole**\n`exists_zero_avoiding_T_wide` (T \u2208 [a, a+1], clearance 1/(9\u00b7C0hat(a+2))\nagainst ALL zeros with im \u2208 (a\u22121, a+2); zeroWindowWide + the 3-unit\ncount \u2264 3\u00b7C0hat(a+2) via three unit windows + inline log-monotonicity;\nthe exists_avoiding_midpoint machine reused verbatim).\n\n**LiAssembly.lean NEW** (~460 lines, builds green, root-imported):\n- \u00a71 `sf_abs_le_rectInt_add_zeroSum (hZC)`: the sides identity \u2014\n rectInt'_Jlag on the variant-B rectangle (rectZ T = \u22125/2 \u2212 iT,\n rectW n T = 2\u221an + iT) with 1 interior and the border zero-free\n (zeta_zero_classification: nontrivial \u2192 the wide-pigeonhole\n contradiction on im = \u00b1T (conj for the bottom); re = \u22125/2 excluded by\n the strip; re = 2\u221an \u2265 2 by one_le_re; s = 0 / \u22122n by direct re/im\n computation) \u27f9 |Sf n| = |(ResW1 n).re| \u2264 \u2016RectInt\u2016 + \u2016\u03a3\u2016\n (sf_eq_resW1 + abs_re_le_norm + norm_sub_le). Sz = zeroBothWindow \u222a\n {\u22122} with the full \u2194 characterization (backward: zetaA s = 0 \u2227 inside\n \u27f9 classification, with \u22122n inside \u27f9 m = 1).\n- \u00a72 `zeroSum_norm_le_four_FAlt_add_one (hRH) (hZCG) (hNLZ)`: the\n bridge \u2014 zeroTerm_norm_le_two (|\u03c1| = |1\u2212\u03c1| at re = 1/2 via normSq,\n hence |1\u2212(\u03c1/(\u03c1\u22121))\u207f| \u2264 2\u00b7mult), zeroSum_nontriv_norm_le (norm_sum_le\n + per-term), zeroBothWindow_sum_eq_two_mul (both-signs = 2\u00d7 one-sign:\n NoLowZeros \u27f9 im \u2260 0; the conj-image reindex with zeroMult_conj;\n Finset.image PLAIN-function + Set.InjOn form in this Mathlib),\n trivTerm_norm_le_one (zeroMult_neg_two + |1\u2212(2/3)\u207f| \u2264 1) \u27f9\n \u2016\u03a3\u2016 \u2264 4\u00b7FAlt T + 1.\n\n**Closure**: LiAssembly root-imported; full build GREEN (8772 jobs);\nAuditSession038d.lean + audit-session038d-axioms.txt \u2014 12 decls, ALL 3\nstandard axioms only, 0 sorryAx; both perimeter Props printed verbatim.\n\n## Banked gotchas (ii\u2032-6-b)\n\n- **The RectangleBorder rcases trap**: `rcases hs with hb | hb | hb |\n hb` on a RectangleBorder membership CASES the singleton-Eq inside the\n \u00d7\u2102 pieces (\"dependent elimination failed ... at case Eq.refl\" \u2014 the\n sides are non-defeq by design). ROUTE THAT WORKS: rw [RectangleBorder]\n + simp only [Set.mem_union, Complex.mem_reProdIm,\n Set.mem_singleton_iff] at hs + tauto to a flat 4-way Eq-disjunction,\n then rcases THAT (Eqs stay as hypotheses).\n- `Finset.image` in this Mathlib takes a PLAIN function + Set.InjOn\n (Finset.sum_image signature), NOT an embedding (the \u27e8f, inj\u27e9\n anonymous constructor errors \"not an inductive type\").\n- `set x := toFinset` breaks mem_toFinset rewrite patterns (the goal\n keeps the local variable; rw [hX] at the goal first or avoid set).\n Finset-ext goals use the SetLike coe (displays as the set);\n Set.Finite.mem_toFinset rewrites need the Finset-membership form \u2014\n simp only [mem_toFinset] is more robust than rw.\n- `ne_of_gt`/`ne_of_lt` directions: ne_of_gt (b < a) : a \u2260 b \u2014 for\n 0 \u2260 \u2212T use ne_of_lt (\u2212T < 0)?? NO \u2014 use `by linarith : (0:\u211d) \u2260 -T`\n (linarith proves \u2260 directly, no direction bugs).\n- `rw [hre] at hnt` FAILS on IsNontrivialZero (structure opacity) \u2014\n use the projections: `hre \u25b8 hnt.2.1`.\n- `sq_eq_sq\u2080 (norm_nonneg _) (norm_nonneg _) |>.mp h : \u2016a\u2016 = \u2016b\u2016` for\n the |\u03c1| = |1\u2212\u03c1| equality at re = 1/2 (normSq expansion + simp only\n [sub_re, one_re, sub_im] + rw [hre] AFTER the simp, then ring).\n- `pow_le_one\u2080 (h1 : 0 \u2264 a) (h2 : a \u2264 1) : a ^ n \u2264 1` \u2014 n IMPLICIT\n (don't pass it; ascribe).\n- `Finset.sum_union` takes a Disjoint proof (build via\n Finset.disjoint_left for the singleton).\n- `riemannZeta_neg_two_mul (hn : 1 \u2264 n) : riemannZeta (-2\u00b7n) = 0`\n (LiFEntire) + `zeroMult_neg_two : zeroMult (-2) = 1` (LiContour).\n\n## Files (ii\u2032-6-b)\n\n- research/lean/NguyenRH1/NguyenRH1/LiContour.lean (perimeter Props +\n wide pigeonhole)\n- research/lean/NguyenRH1/NguyenRH1/LiAssembly.lean (NEW, ~460 lines)\n- research/lean/NguyenRH1/NguyenRH1.lean (LiAssembly root-imported)\n- research/lean/NguyenRH1/AuditSession038d.lean +\n audit-session038d-axioms.txt\n\n## Next\n\nii\u2032-6-c (D-071 \u00a74.4, the long pole): the four side bounds \u2014\nI_III (left vertical: kFun_norm_le_two \u00d7 [tight R-bound + (2/3)\u00b7Z2\nnear + MZeroProp short piece]), I_II/I_IV (horizontals: the\nsegment-integral machine \u2014 per-zero \u222b dx/|w\u2212\u03c1| \u2264 2\u00b7log(16.5/c) via\nasinh, the extended pigeonhole's clearance, Z2 count, 5.5\u00b7(10.5 log +\n48) R-part, the Dirichlet stepping tail 3.3), I_I (right vertical:\nDirichlet stepping 2^{\u2212(\u03c3\u2081\u22122)}\u00b7dirichletC2 \u00d7 kFun_shift \u2264 e^{\u221an/2}+1\n\u27f9 IIMaj), triv (done in \u00a72). Then ii\u2032-6-d (the fold \u27f9 sfBoundProp).\nEOF\necho done",
"description": "Append ii\u2032-6-b to journal"
}
raw content_json (database row)
[{"type":"thinking","thinking":"All 12 audited: 3 standard axioms only, 0 sorryAx; both perimeter Props printed verbatim. ii′-6-b COMPLETE. Archive + commit.","signature":""},{"type":"text","text":"All clean (12 decls, 3 standard axioms, 0 sorryAx; both perimeter Props verbatim). **ii′-6-b COMPLETE.** Closing the archive."},{"type":"tool_use","id":"Bash_321","name":"Bash","input":{"command":"cd D:/Python/Quantum && cat >> research/journal/session-038.md << 'EOF'\n\n## ii′-6-b COMPLETE (same session, fourth continuation) — the assembly pieces\n\n**LiContour.lean additions** (builds green): the two user-approved\nperimeter Props — `ZeroCountGlobalProp` (∀ T ≥ 2, mult-weighted\none-sign count with 0 < γ ≤ T ≤ FAlt T; zeroGlobalWindow +\nzeroGlobalWindow_finite) and `MZeroProp` (∀ |t| ≤ 10, ‖logDeriv ζ\n(−5/2 + t·I)‖ ≤ 1.3352) — plus the **wide pigeonhole**\n`exists_zero_avoiding_T_wide` (T ∈ [a, a+1], clearance 1/(9·C0hat(a+2))\nagainst ALL zeros with im ∈ (a−1, a+2); zeroWindowWide + the 3-unit\ncount ≤ 3·C0hat(a+2) via three unit windows + inline log-monotonicity;\nthe exists_avoiding_midpoint machine reused verbatim).\n\n**LiAssembly.lean NEW** (~460 lines, builds green, root-imported):\n- §1 `sf_abs_le_rectInt_add_zeroSum (hZC)`: the sides identity —\n rectInt'_Jlag on the variant-B rectangle (rectZ T = −5/2 − iT,\n rectW n T = 2√n + iT) with 1 interior and the border zero-free\n (zeta_zero_classification: nontrivial → the wide-pigeonhole\n contradiction on im = ±T (conj for the bottom); re = −5/2 excluded by\n the strip; re = 2√n ≥ 2 by one_le_re; s = 0 / −2n by direct re/im\n computation) ⟹ |Sf n| = |(ResW1 n).re| ≤ ‖RectInt‖ + ‖Σ‖\n (sf_eq_resW1 + abs_re_le_norm + norm_sub_le). Sz = zeroBothWindow ∪\n {−2} with the full ↔ characterization (backward: zetaA s = 0 ∧ inside\n ⟹ classification, with −2n inside ⟹ m = 1).\n- §2 `zeroSum_norm_le_four_FAlt_add_one (hRH) (hZCG) (hNLZ)`: the\n bridge — zeroTerm_norm_le_two (|ρ| = |1−ρ| at re = 1/2 via normSq,\n hence |1−(ρ/(ρ−1))ⁿ| ≤ 2·mult), zeroSum_nontriv_norm_le (norm_sum_le\n + per-term), zeroBothWindow_sum_eq_two_mul (both-signs = 2× one-sign:\n NoLowZeros ⟹ im ≠ 0; the conj-image reindex with zeroMult_conj;\n Finset.image PLAIN-function + Set.InjOn form in this Mathlib),\n trivTerm_norm_le_one (zeroMult_neg_two + |1−(2/3)ⁿ| ≤ 1) ⟹\n ‖Σ‖ ≤ 4·FAlt T + 1.\n\n**Closure**: LiAssembly root-imported; full build GREEN (8772 jobs);\nAuditSession038d.lean + audit-session038d-axioms.txt — 12 decls, ALL 3\nstandard axioms only, 0 sorryAx; both perimeter Props printed verbatim.\n\n## Banked gotchas (ii′-6-b)\n\n- **The RectangleBorder rcases trap**: `rcases hs with hb | hb | hb |\n hb` on a RectangleBorder membership CASES the singleton-Eq inside the\n ×ℂ pieces (\"dependent elimination failed ... at case Eq.refl\" — the\n sides are non-defeq by design). ROUTE THAT WORKS: rw [RectangleBorder]\n + simp only [Set.mem_union, Complex.mem_reProdIm,\n Set.mem_singleton_iff] at hs + tauto to a flat 4-way Eq-disjunction,\n then rcases THAT (Eqs stay as hypotheses).\n- `Finset.image` in this Mathlib takes a PLAIN function + Set.InjOn\n (Finset.sum_image signature), NOT an embedding (the ⟨f, inj⟩\n anonymous constructor errors \"not an inductive type\").\n- `set x := toFinset` breaks mem_toFinset rewrite patterns (the goal\n keeps the local variable; rw [hX] at the goal first or avoid set).\n Finset-ext goals use the SetLike coe (displays as the set);\n Set.Finite.mem_toFinset rewrites need the Finset-membership form —\n simp only [mem_toFinset] is more robust than rw.\n- `ne_of_gt`/`ne_of_lt` directions: ne_of_gt (b < a) : a ≠ b — for\n 0 ≠ −T use ne_of_lt (−T < 0)?? NO — use `by linarith : (0:ℝ) ≠ -T`\n (linarith proves ≠ directly, no direction bugs).\n- `rw [hre] at hnt` FAILS on IsNontrivialZero (structure opacity) —\n use the projections: `hre ▸ hnt.2.1`.\n- `sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _) |>.mp h : ‖a‖ = ‖b‖` for\n the |ρ| = |1−ρ| equality at re = 1/2 (normSq expansion + simp only\n [sub_re, one_re, sub_im] + rw [hre] AFTER the simp, then ring).\n- `pow_le_one₀ (h1 : 0 ≤ a) (h2 : a ≤ 1) : a ^ n ≤ 1` — n IMPLICIT\n (don't pass it; ascribe).\n- `Finset.sum_union` takes a Disjoint proof (build via\n Finset.disjoint_left for the singleton).\n- `riemannZeta_neg_two_mul (hn : 1 ≤ n) : riemannZeta (-2·n) = 0`\n (LiFEntire) + `zeroMult_neg_two : zeroMult (-2) = 1` (LiContour).\n\n## Files (ii′-6-b)\n\n- research/lean/NguyenRH1/NguyenRH1/LiContour.lean (perimeter Props +\n wide pigeonhole)\n- research/lean/NguyenRH1/NguyenRH1/LiAssembly.lean (NEW, ~460 lines)\n- research/lean/NguyenRH1/NguyenRH1.lean (LiAssembly root-imported)\n- research/lean/NguyenRH1/AuditSession038d.lean +\n audit-session038d-axioms.txt\n\n## Next\n\nii′-6-c (D-071 §4.4, the long pole): the four side bounds —\nI_III (left vertical: kFun_norm_le_two × [tight R-bound + (2/3)·Z2\nnear + MZeroProp short piece]), I_II/I_IV (horizontals: the\nsegment-integral machine — per-zero ∫ dx/|w−ρ| ≤ 2·log(16.5/c) via\nasinh, the extended pigeonhole's clearance, Z2 count, 5.5·(10.5 log +\n48) R-part, the Dirichlet stepping tail 3.3), I_I (right vertical:\nDirichlet stepping 2^{−(σ₁−2)}·dirichletC2 × kFun_shift ≤ e^{√n/2}+1\n⟹ IIMaj), triv (done in §2). Then ii′-6-d (the fold ⟹ sfBoundProp).\nEOF\necho done","description":"Append ii′-6-b to journal"},"extra_content":null}]