← Session 33 — ii′-3b/3c crux + F-D finding; Lagarias letter package
thinking (11252 chars)
`isNontrivialZero_conj` is in LiCircleBound (imported by LiTightR via LiSqueeze → LiCircleBound chain; LiTightR imports LiSqueeze? LiTightR imports LiCircleBound/LiSqueeze per the 5f chain ✓ since zeroMult_conj works in LiMoments via LiTightR import).
LiAssembly.lean imports: Mathlib, LiSides, LiCrux, LiContour, LiTightR, LiFEntire, LiCircleBound. (LiCrux imports LiMoments which imports LiTightR + LiSwaps; LiFEntire for zeta_zero_classification; LiCircleBound for isNontrivialZero_conj.)
Now the sides identity. Let me define the rectangle:
- z := ((-5/2 : ℝ) : ℂ) - (T : ℝ) * Complex.I — re = −5/2, im = −T.
- w := ((2 * Real.sqrt n : ℝ) : ℂ) + (T : ℝ) * Complex.I — re = 2√n, im = T.
re/im computations: z.re = −5/2 (Complex.sub_re, ofReal_re, mul_I_re... ((−5/2 : ℝ):ℂ) − (T:ℝ)*I: re = −5/2 − 0 = −5/2 ✓ via simp). z.im = −T (sub_im: 0 − T = −T ✓ simp). w.re = 2√n ✓ w.im = T ✓ simp.
hre : z.re ≤ w.re — after simp: −5/2 ≤ 2√n ✓ (norm_num + Real.sqrt_nonneg).
him : z.im ≤ w.im — −T ≤ T ✓ (T ≥ √n ≥ 1 > 0).
h1 : Rectangle z w ∈ 𝓝 1 via rectangle_mem_nhds_of_mem_not_border hre him hmem hnotborder:
- hmem : (1:ℂ) ∈ Rectangle z w: ⟨re-uIcc, im-uIcc⟩: re 1 ∈ [[−5/2, 2√n]] (uIcc: −5/2 ≤ 1 ≤ 2√n — need 1 ≤ 2√n: n ≥ 1: √n ≥ 1: 2√n ≥ 2 > 1 ✓); im 0 ∈ [[−T, T]] ✓ (−T ≤ 0 ≤ T).
- hnotborder : (1:ℂ) ∉ RectangleBorder z w: the border = [[z.re, w.re]] ×ℂ {z.im} ∪ {z.re} ×ℂ [[z.im, w.im]] ∪ [[z.re, w.re]] ×ℂ {w.im} ∪ {w.re} ×ℂ [[z.im, w.im]]: 1 ∈ any piece requires re 1 ∈ {−5/2} ∨ re 1 ∈ {2√n} ∨ im 0 ∈ {−T} ∨ im 0 ∈ {T}: all false (1 ≠ −5/2; 1 ≠ 2√n (2√n ≥ 2); 0 ≠ ±T (T ≥ 1)).
The ×ℂ membership: mem_reProdIm? `×ℂ` is Complex.reProdIm: s ∈ A ×ℂ B ↔ re s ∈ A ∧ im s ∈ B ✓ (Complex.mem_reProdIm exists? from LiSides usage — the border membership decomposition. Let me check how membership in ×ℂ is decomposed elsewhere... The RectangleBorderIntegrable proofs use ContinuousOn on the border — membership: `Set.mem_reProdIm`? I'll use simp to decompose).
hborder : ∀ s ∈ RectangleBorder z w, riemannZeta s ≠ 0:
intro s hs
decompose hs into 4 cases via the union structure:
- bottom (im = z.im = −T): ζ s = 0 ⟹ classification: nontrivial (re ∈ (0,1), im = −T: |im| = T: conj: im = T ∈ [√n, √n+1] ⊆ (√n−1, √n+2): the wide pigeonhole gives |T − im(conj)| ≥ 1/(9C0) > 0 — contradiction with im(conj) = T... wait the pigeonhole gives |ρ.im − T| ≥ 1/(9·C0hat(a+2)) > 0 for zeros with im ∈ (√n−1, √n+2): conj ρ has im = T ∈ that window ⟹ |T − T| = 0 ≥ 1/(9C0) > 0 — contradiction ✓); s = 0 (im 0 ≠ −T ✓ T > 0); s = −2n (im 0 ≠ −T ✓).
- left (re = z.re = −5/2): classification: nontrivial re ∈ (0,1) ✗ ≠ −5/2; 0 ✗; −2n: re = −2n = −5/2 ⟹ 2n = 5/2 ✗ (no nat).
- top (im = w.im = T): nontrivial with im = T ∈ [√n, √n+1] ⊆ window ⟹ pigeonhole contradiction; 0, −2n: im = 0 ≠ T ✓.
- right (re = w.re = 2√n): re = 2√n ≥ 2 > 1: riemannZeta_ne_zero_of_one_le_re ✓ (1 ≤ re).
For the classification I use zeta_zero_classification (needs ζ s = 0 as hypothesis — proof by contradiction: intro hζ; rcases zeta_zero_classification hζ with hn | h0 | hn2).
The wide pigeonhole hypothesis hTwide : ∀ ρ, IsNontrivialZero ρ → a−1 < ρ.im → ρ.im < a+2 → 1/(9·C0hat(a+2)) ≤ |ρ.im − T| with a := √n.
For the conj argument (bottom side): ρ zero with im = −T: conj ρ is a zero (isNontrivialZero_conj) with im = T (conj_im: (conj ρ).im = −ρ.im = T) ✓ in the window (√n−1 < T < √n+2 — T ∈ [√n, √n+1] ✓): pigeonhole gives 1/(9·C0hat(√n+2)) ≤ |T − T| = 0 — contradiction (positivity of 1/(9·C0hat): C0hat ≥ 2 ✓).
Then Sz: define `zeroBothWindow (T : ℝ) : Set ℂ := {ρ | IsNontrivialZero ρ ∧ |ρ.im| ≤ T}` + finiteness (zerosIn_finite? — zerosIn is for [A, B] with A ≤ im ≤ B: |im| ≤ T = im ∈ [−T, T]: zerosIn_finite (−T) T ✓).
Sz := (zeroBothWindow_finite T).toFinset ∪ {−2}.
hSz : ∀ s, s ∈ Sz ↔ s ∈ Rectangle z w ∧ zetaA s = 0:
- (→): s ∈ Sz: nontrivial with |im| ≤ T: inside (re ∈ (0,1) ⊆ [−5/2, 2√n] ✓ — need 1 < 2√n; im ∈ [−T, T] ✓) ∧ zetaA s = 0 (zetaA_apply (s ≠ 1 — nontrivial re < 1 ⟹ s ≠ 1) : zetaA s = (s−1)·ζ s = 0 ✓). −2: inside ✓ ∧ zetaA(−2) = (−3)·ζ(−2) = 0 ✓.
- (←): s ∈ Rectangle ∧ zetaA s = 0: s ≠ 1 (zetaA_one = 1 ≠ 0); ζ s = 0 (zetaA_apply); classification: nontrivial ⟹ |im| ≤ T (inside: im ∈ [−T, T] ✓) ⟹ ∈ zeroBothWindow; s = 0: zetaA 0 = 1/2 ≠ 0 — contradiction; s = −2n: inside: re = −2n ∈ [−5/2, 2√n]: −5/2 ≤ −2n ⟹ n ≤ 5/4 ⟹ n = 1 ⟹ s = −2 ∈ {−2} ✓.
Then the identity:
```lean
theorem sf_abs_le_rectInt_add_zeroSum (hZC : ZeroCountProp) {n : ℕ} (hn : 1 ≤ n)
{T : ℝ} (hTpos : 1 ≤ T) (hTn : Real.sqrt n ≤ T) (hTn1 : T ≤ Real.sqrt n + 1)
(hTwide : ∀ ρ : ℂ, IsNontrivialZero ρ → Real.sqrt n - 1 < ρ.im →
ρ.im < Real.sqrt n + 2 → 1 / (9 * C0hat (Real.sqrt n + 2)) ≤ |ρ.im - T|) :
|Sf n| ≤ ‖RectangleIntegral' (Jlag n) (((-5/2 : ℝ) : ℂ) - (T : ℝ) * Complex.I)
(((2 * Real.sqrt n : ℝ) : ℂ) + (T : ℝ) * Complex.I)‖ +
‖∑ ρ ∈ ((zeroBothWindow_finite T).toFinset ∪ {(-2 : ℂ)}),
(zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)‖ := by
have h1 := sf_eq_resW1 hZC hn
rw [← h1]
refine le_trans (abs_re_le_norm _) ?_
-- ResW1 n = RectInt − Σ
rw [rectInt'_Jlag n hre him h1int hborder Sz hSz]
-- goal: ‖ResW1 + Σ‖ ≤ ‖RectInt‖ + ‖Σ‖: ResW1 = RectInt − Σ: norm_sub_le...
```
Hmm — rectInt'_Jlag gives RectInt = ResW1 n + Σ. So ResW1 n = RectInt − Σ: rw then:
```lean
have hid := rectInt'_Jlag n hre him h1int hborder Sz hSz
-- hid : RectInt = ResW1 n + Σ
have e : ResW1 n = RectangleIntegral' (Jlag n) z w - ∑ ... := by
linear_combination hid
rw [e]
exact norm_sub_le _ _
```
The sum in my statement uses the same Sz expression — match forms exactly.
Then the bridge (in the same file):
```lean
theorem zeroSum_norm_le_four_FAlt_add_one (hRH : RHUpTo (3 * 10 ^ 12)) (hZCG : ZeroCountGlobalProp)
(hNLZ : NoLowZeros) {n : ℕ} {T : ℝ} (hTle : T ≤ 3 * 10 ^ 12 - 1) (hT2 : 2 ≤ T) :
‖∑ ρ ∈ ((zeroBothWindow_finite T).toFinset ∪ {(-2 : ℂ)}),
(zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)‖ ≤ 4 * FAlt T + 1 := by
```
Proof: split the sum: Σ = Σ_{zeroBothWindow} + term(−2) (Finset.sum_union with −2 ∉ zeroBothWindow (re = −2 ∉ (0,1))).
- |term(−2)|: (zeroMult (-2) : ℂ) = 1 (zeroMult_neg_two ✓ in LiContour); term = 1·(1 − ((−2)/(−2−1))ⁿ) = 1 − (2/3)ⁿ; ‖1 − (2/3)ⁿ‖ ≤ 1 + (2/3)ⁿ ≤ 1 + 1... D-037 says 1 − 2^{−n} ≤ 1 — hmm: |(−2)/(−3)| = 2/3 < 1 ⟹ (2/3)ⁿ ≤ 1 ⟹ 1 − (2/3)ⁿ ∈ [0, 1): ‖·‖ ≤ 1 ✓ (compute: (2/3:ℂ) is real positive: (1 − (2/3)ⁿ) : ℂ is real in [0,1]: norm = value ≤ 1).
- ‖Σ_nontriv‖ ≤ Σ ‖mult·(1−(ρ/(ρ−1))ⁿ)‖ ≤ Σ mult·2:
per term: hRH: ρ nontrivial, |im| ≤ T ≤ 3×10¹²−1 < 3×10¹² ⟹ |ρ.im| ≤ 3×10¹² ⟹ re = 1/2. |ρ/(ρ−1)| = 1: ‖ρ‖² = re²+im² = 1/4+γ²; ‖ρ−1‖² = (re−1)²+im² = 1/4+γ² ✓ equal ⟹ ‖ρ/(ρ−1)‖ = 1 ⟹ ‖(ρ/(ρ−1))ⁿ‖ = 1 ⟹ ‖1 − (ρ/(ρ−1))ⁿ‖ ≤ ‖1‖ + 1 = 2. So term ≤ mult·2.
Σ mult·2 = 2·Σ mult (Finset.mul_sum).
- Σ mult over zeroBothWindow = 2·Σ over zeroGlobalWindow:
zeroBothWindow = {IsNontrivialZero ∧ |im| ≤ T}: with hNLZ: im ≠ 0 (|im| ≥ 14 > 0) ⟹ (0 < im ≤ T) ∪ (−T ≤ im < 0): zeroBothWindow = zeroGlobalWindow T ∪ conj '' zeroGlobalWindow T (the conj image): the conj bijection: sum over the image = sum over the source (Finset.sum_image with the conj involution + zeroMult_conj ✓).
Formally: define the negative window zeroGlobalWindowNeg T := {ρ | IsNontrivialZero ρ ∧ -T ≤ ρ.im ∧ ρ.im < 0}: zeroBothWindow = zeroGlobalWindow ∪ zeroGlobalWindowNeg (with hNLZ for im ≠ 0) and the conj map is a bijection zeroGlobalWindowNeg → zeroGlobalWindow with zeroMult preserved ⟹ Σ_neg = Σ_pos.
Then Σ_both = Σ_pos + Σ_neg = 2·Σ_pos ≤ 2·FAlt T (hZCG T hT2).
This is the finicky part (~150 lines). Alternative cleaner: bound the both-signs sum directly via a conj-equiv reindex WITHOUT splitting: define the conj involution on zeroBothWindow (maps to itself), and pair... no — the sum over both-signs isn't 2× the positive automatically — it IS via the decomposition. Let me just do the decomposition.
Actually — simpler: Σ_{both} mult = Σ_{pos} mult + Σ_{neg} mult where Σ_neg = Σ_pos by the conj bijection. For the FINSET formulation:
- W := (zeroBothWindow_finite T).toFinset; P := (zeroGlobalWindow_finite T).toFinset; N := (zeroGlobalWindowNeg_finite T).toFinset.
- W = P ∪ N (with hNLZ): membership: |im| ≤ T ∧ |im| ≥ 14 ⟹ im ≠ 0: (0 < im ≤ T) ∨ (−T ≤ im < 0) ✓.
- N = P.image (starRingEnd ℂ)?? conj maps N → P bijectively: Σ_{ρ ∈ N} mult ρ = Σ_{ρ ∈ P} mult (starRingEnd ℂ ρ)... wait — I want Σ over N in terms of Σ over P: N's elements are conj's of P's elements: N = image conj P: Σ_{ρ ∈ N} zeroMult ρ = Σ_{ρ ∈ P} zeroMult (conj ρ) = Σ_{ρ ∈ P} zeroMult ρ (zeroMult_conj ✓).
Finset.sum_image : (∑ x ∈ s.image f, g x) = ∑ x ∈ s, g (f x) (needs InjOn). zeroMult (conj ρ) = zeroMult ρ ✓ zeroMult_conj.
Hmm — conj is starRingEnd ℂ: image (starRingEnd ℂ) P — starRingEnd is an equiv (involutive): InjOn trivial ✓.
OK — the bridge is the biggest piece. Let me also think about whether hNLZ is REALLY needed: zeros with im = 0 in zeroBothWindow — a nontrivial zero with im = 0 sits in (0,1)×{0} — the conj decomposition would have im = 0 zeros in BOTH windows' boundary? My decomposition: pos = 0 < im ≤ T; neg = −T ≤ im < 0: im = 0 excluded from both. If there were an im = 0 nontrivial zero, it'd be missed. hNLZ kills it ✓ needed. (Alternatively |im| ≤ T with im = 0 handled separately — but hNLZ is cleaner and it's already perimeter.)
Actually — hmm, wait: do I even need NoLowZeros? A nontrivial zero with im = 0: re ∈ (0,1), ζ = 0 on the real segment (0,1) — ζ(x) < 0 for x ∈ [0,1) — is that in Mathlib? `riemannZeta_ne_zero_of_one_le_re` only covers re ≥ 1. For (0,1): hmm — Mathlib might have `riemannZeta_ne_zero_of_zero_le_re_le_one`?? I doubt it. hNLZ (|γ| ≥ 14) is the declared certificate ✓ use it — it's already in the perimeter for 5f.
Now — LiAssembly structure:
§0: zeroBothWindow + finiteness.
§1: the sides identity sf_abs_le_rectInt_add_zeroSum.
§2: the bridge zeroSum_norm_le_four_FAlt_add_one.
Wait — one important check: the sides identity's sum uses the Sz = (zeroBothWindow_finite T).toFinset ∪ {−2} — and rectInt'_Jlag's hSz characterizes Sz as {s ∈ Rectangle ∧ zetaA s = 0}. My hSz proves the characterization for that exact finset ✓.
Also norm of the sum in the identity: ‖∑ ρ ∈ Sz, mult·(1−(ρ/(ρ−1))ⁿ)‖ — matches rectInt'_Jlag's output form: `∑ ρ ∈ Sz, (zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)` ✓.
Let me also double check the bridge's target form: ≤ 4·FAlt T + 1: the split: ‖Σ_{W ∪ {−2}}‖ ≤ ‖Σ_W‖ + ‖term(−2)‖ — hmm: sum over union = sum_W + term(−2) (sum_union with −2 ∉ W); ‖sum_W + term‖ ≤ ‖sum_W‖ + ‖term‖ ≤ (Σ_W mult·2) + 1 ≤ 2·Σ_W mult + 1 ≤ 2·(2·FAlt T) + 1 = 4·FAlt T + 1 ✓.
Wait: ‖Σ_W‖ ≤ Σ_W ‖mult·(1−...)‖ = Σ_W mult·2 = 2·Σ_W mult (norm_sum_le + per-term bound + tsum... Finset: norm_sum_le : ‖∑ f‖ ≤ ∑ ‖f‖ ✓).
Let me write the file now. Size estimate ~450 lines. Also need zeroGlobalWindowNeg + finiteness.
Actually, for the conj bijection, one more consideration: zeroGlobalWindowNeg_finite T := {ρ | IsNontrivialZero ρ ∧ -T ≤ ρ.im ∧ ρ.im < 0}: finiteness via zerosIn_finite (−T) 0 (im ∈ [−T, 0] ⊇ [−T, 0) ✓).
And W = P ∪ N: W's members: IsNontrivialZero ∧ |im| ≤ T: with hNLZ: |im| ≥ 14: im > 0: 0 < im ≤ T → P; im < 0: −T ≤ im < 0 → N ✓. And P ∪ N ⊆ W ✓ (P: |im| = im ≤ T ✓; N: |im| = −im ≤ T ✓).
Write it.
All forms confirmed. Writing LiAssembly.lean (§1 sides identity, §2 bridge).
tool: Write ok
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiAssembly.lean",
"content": "/-\nLiAssembly.lean \u2014 tier ii\u2032-6-b: the sides identity and the bridge\n(D-071 \u00a74.1\u20134.3).\n\n\u00a71 (`sf_abs_le_rectInt_add_zeroSum`): the rectangle residue theorem\n`rectInt'_Jlag` (ii\u2032-1b) on the D-036 variant-B rectangle\n(z = \u22125/2 \u2212 iT, w = 2\u221an + iT, T zero-avoiding-wide from ii\u2032-6's L3-wide)\nplus the crux `sf_eq_resW1` (ii\u2032-3c):\n |Sf n| = |(ResW1 n).re| \u2264 \u2016RectInt\u2016 + \u2016\u03a3_{Sz} mult\u00b7(1\u2212(\u03c1/(\u03c1\u22121))\u207f)\u2016.\n\n\u00a72 (`zeroSum_norm_le_four_FAlt_add_one`): the bridge \u2014 under RHUpTo\n3\u00d710\u00b9\u00b2 every zero in Sz is on the line (|\u03c1/(\u03c1\u22121)| = 1), so each term\n\u2264 2\u00b7mult, and the both-signs mult-count is 2\u00d7 the one-sign count\n(conj symmetry + `zeroMult_conj` + the perimeter `ZeroCountGlobalProp`)\n\u27f9 \u2016\u03a3\u2016 \u2264 4\u00b7FAlt T + 1 (the +1 is the trivial-zero term at \u22122).\n\nPerimeter used: ZeroCountProp (the crux), RHUpTo, ZeroCountGlobalProp,\nNoLowZeros.\n-/\nimport Mathlib\nimport NguyenRH1.LiSides\nimport NguyenRH1.LiCrux\nimport NguyenRH1.LiContour\nimport NguyenRH1.LiTightR\nimport NguyenRH1.LiFEntire\nimport NguyenRH1.LiCircleBound\n\nopen Zeta23 Complex Filter Topology\nopen scoped Nat\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 0. The both-signs ordinate window -/\n\n/-- The nontrivial zeros with |\u03b3| \u2264 T (the rectangle's zero content,\nminus the trivial zero \u22122 which is handled separately). -/\ndef zeroBothWindow (T : \u211d) : Set \u2102 :=\n {\u03c1 | IsNontrivialZero \u03c1 \u2227 |\u03c1.im| \u2264 T}\n\n/-- Finiteness of the both-signs window (via Zeta23 `zerosIn_finite`). -/\ntheorem zeroBothWindow_finite (T : \u211d) : (zeroBothWindow T).Finite := by\n apply Set.Finite.subset (zerosIn_finite (-T) T)\n intro \u03c1 h\u03c1\n refine \u27e8h\u03c1.1, ?_, ?_\u27e9\n \u00b7 linarith [abs_le.mp h\u03c1.2 |>.1]\n \u00b7 exact abs_le.mp h\u03c1.2 |>.2\n\n/-- The negative ordinate window: nontrivial zeros with \u2212T \u2264 \u03b3 < 0. -/\ndef zeroGlobalWindowNeg (T : \u211d) : Set \u2102 :=\n {\u03c1 | IsNontrivialZero \u03c1 \u2227 -T \u2264 \u03c1.im \u2227 \u03c1.im < 0}\n\n/-- Finiteness of the negative window. -/\ntheorem zeroGlobalWindowNeg_finite (T : \u211d) : (zeroGlobalWindowNeg T).Finite := by\n apply Set.Finite.subset (zerosIn_finite (-T) 0)\n intro \u03c1 h\u03c1\n refine \u27e8h\u03c1.1, h\u03c1.2.1, by linarith [h\u03c1.2.2]\u27e9\n\n/-! ## 1. The sides identity -/\n\n/-- The rectangle for the L0 assembly (D-036 variant B): z = \u22125/2 \u2212 iT,\nw = 2\u221an + iT. -/\nabbrev rectZ (T : \u211d) : \u2102 := ((-5 / 2 : \u211d) : \u2102) - (T : \u211d) * Complex.I\nabbrev rectW (n : \u2115) (T : \u211d) : \u2102 := ((2 * Real.sqrt n : \u211d) : \u2102) + (T : \u211d) * Complex.I\n\nlemma rectZ_re (T : \u211d) : (rectZ T).re = -5 / 2 := by simp [rectZ]\nlemma rectZ_im (T : \u211d) : (rectZ T).im = -T := by simp [rectZ]\nlemma rectW_re (n : \u2115) (T : \u211d) : (rectW n T).re = 2 * Real.sqrt n := by simp [rectW]\nlemma rectW_im (n : \u2115) (T : \u211d) : (rectW n T).im = T := by simp [rectW]\n\n/-- **The sides identity** (D-071 \u00a74.1): on the variant-B rectangle with\nthe wide zero-avoiding ordinate,\n|Sf n| \u2264 \u2016RectangleIntegral' (Jlag n) z w\u2016 + \u2016\u03a3_{Sz} mult\u00b7(1\u2212(\u03c1/(\u03c1\u22121))\u207f)\u2016,\nSz = {nontrivial zeros, |\u03b3| \u2264 T} \u222a {\u22122}. -/\ntheorem sf_abs_le_rectInt_add_zeroSum (hZC : ZeroCountProp) {n : \u2115} (hn : 1 \u2264 n)\n {T : \u211d} (hT1 : 1 \u2264 T) (hTn : Real.sqrt n \u2264 T) (hTn1 : T \u2264 Real.sqrt n + 1)\n (hTwide : \u2200 \u03c1 : \u2102, IsNontrivialZero \u03c1 \u2192 Real.sqrt n - 1 < \u03c1.im \u2192\n \u03c1.im < Real.sqrt n + 2 \u2192 1 / (9 * C0hat (Real.sqrt n + 2)) \u2264 |\u03c1.im - T|) :\n |Sf n| \u2264 \u2016RectangleIntegral' (Jlag n) (rectZ T) (rectW n T)\u2016 +\n \u2016\u2211 \u03c1 \u2208 ((zeroBothWindow_finite T).toFinset \u222a {(-2 : \u2102)}),\n (zeroMult \u03c1 : \u2102) * (1 - (\u03c1 / (\u03c1 - 1)) ^ n)\u2016 := by\n set z := rectZ T\n set w := rectW n T\n have hn1sqrt : (1 : \u211d) \u2264 Real.sqrt n := Real.one_le_sqrt.mpr (by exact_mod_cast hn)\n have hre : z.re \u2264 w.re := by\n rw [rectZ_re, rectW_re]\n have h := Real.sqrt_nonneg (n : \u211d)\n linarith\n have him : z.im \u2264 w.im := by\n rw [rectZ_im, rectW_im]\n linarith\n -- 1 is interior\n have h1mem : (1 : \u2102) \u2208 Rectangle z w := by\n have hr : (1 : \u2102).re \u2208 Set.uIcc z.re w.re := by\n rw [Set.uIcc_of_le hre, rectZ_re, rectW_re, Complex.one_re, Set.mem_Icc]\n constructor <;> [linarith; linarith [Real.sqrt_nonneg (n : \u211d)]]\n have hi : (1 : \u2102).im \u2208 Set.uIcc z.im w.im := by\n rw [Set.uIcc_of_le him, rectZ_im, rectW_im, Complex.one_im, Set.mem_Icc]\n constructor <;> linarith\n exact \u27e8hr, hi\u27e9\n have h1notb : (1 : \u2102) \u2209 RectangleBorder z w := by\n intro hb\n have h1re : (1 : \u2102).re = 1 := Complex.one_re\n have h1im : (1 : \u2102).im = 0 := Complex.one_im\n have h2n : (1 : \u211d) < 2 * Real.sqrt n := by linarith [Real.one_le_sqrt.mpr (by exact_mod_cast hn : (1 : \u211d) \u2264 n)]\n rcases hb with hb | hb | hb | hb\n \u00b7 exact absurd (Set.mem_singleton_iff.mp hb.2) (by rw [rectZ_im] ; exact ne_of_gt (by linarith : (0 : \u211d) < T))\n \u00b7 exact absurd (Set.mem_singleton_iff.mp hb.1) (by rw [rectZ_re]; norm_num)\n \u00b7 exact absurd (Set.mem_singleton_iff.mp hb.2) (by rw [rectW_im]; exact ne_of_gt (by linarith : (0 : \u211d) < T))\n \u00b7 exact absurd (Set.mem_singleton_iff.mp hb.1) (by rw [rectW_re]; exact ne_of_gt h2n)\n have h1int : Rectangle z w \u2208 \ud835\udcdd (1 : \u2102) :=\n rectangle_mem_nhds_of_mem_not_border hre him h1mem h1notb\n -- the border is zero-free\n have hborder : \u2200 s \u2208 RectangleBorder z w, riemannZeta s \u2260 0 := by\n intro s hs h\u03b6\n rcases zeta_zero_classification h\u03b6 with hnt | h0 | hn2\n \u00b7 -- nontrivial: re \u2208 (0,1); the only border pieces with re in (0,1) are top/bottom\n rcases hs with hb | hb | hb | hb\n \u00b7 -- bottom: im = \u2212T; conj \u03c1 has im = T in the window \u2014 pigeonhole contradiction\n have him : s.im = -T := by\n have := hb.2\n rw [rectZ_im] at this\n exact Set.mem_singleton_iff.mp this\n have hconj := hTwide ((starRingEnd \u2102) s) (isNontrivialZero_conj hnt)\n (by rw [Complex.conj_im, him]; linarith [hTn])\n (by rw [Complex.conj_im, him]; linarith [hTn1])\n have hpos : (0 : \u211d) < 1 / (9 * C0hat (Real.sqrt n + 2)) :=\n one_div_pos.mpr (by have := two_le_C0hat (by linarith [hn1sqrt] : (1 : \u211d) \u2264 Real.sqrt n + 2); positivity)\n have : |(starRingEnd \u2102) s - T| = 0 := by\n rw [Complex.conj_im, him, sub_self, abs_zero]\n linarith [hconj]\n \u00b7 -- left: re = \u22125/2, not in (0,1)\n have hre' : s.re = -5 / 2 := by\n have := hb.1\n rw [rectZ_re] at this\n exact Set.mem_singleton_iff.mp this\n rw [hre'] at hnt\n exact (by norm_num : \u00ac ((0 : \u211d) < -5 / 2 \u2227 -5 / 2 < 1)) \u27e8hnt.2.1, hnt.2.2\u27e9\n \u00b7 -- top: im = T; pigeonhole contradiction directly\n have him : s.im = T := by\n have := hb.2\n rw [rectW_im] at this\n exact Set.mem_singleton_iff.mp this\n have hdir := hTwide s hnt (by rw [him]; exact hTn) (by rw [him]; linarith [hTn1])\n have hpos : (0 : \u211d) < 1 / (9 * C0hat (Real.sqrt n + 2)) :=\n one_div_pos.mpr (by have := two_le_C0hat (by linarith [hn1sqrt] : (1 : \u211d) \u2264 Real.sqrt n + 2); positivity)\n have : |s.im - T| = 0 := by rw [him, sub_self, abs_zero]\n linarith [hdir]\n \u00b7 -- right: re = 2\u221an \u2265 2 > 1\n have hre' : s.re = 2 * Real.sqrt n := by\n have := hb.1\n rw [rectW_re] at this\n exact Set.mem_singleton_iff.mp this\n exact riemannZeta_ne_zero_of_one_le_re (by rw [hre']; linarith [Real.one_le_sqrt.mpr (by exact_mod_cast hn : (1 : \u211d) \u2264 n)]) h\u03b6\n \u00b7 -- s = 0: not on the border (im 0 = \u00b1T needs T = 0; re 0 = \u22125/2 / 2\u221an false)\n rw [h0] at hs\n rcases hs with hb | hb | hb | hb\n \u00b7 exact absurd (Set.mem_singleton_iff.mp hb.2) (by rw [rectZ_im, Complex.zero_im]; exact ne_of_gt (by linarith : (0 : \u211d) < T))\n \u00b7 exact absurd (Set.mem_singleton_iff.mp hb.1) (by rw [rectZ_re, Complex.zero_re]; norm_num)\n \u00b7 exact absurd (Set.mem_singleton_iff.mp hb.2) (by rw [rectW_im, Complex.zero_im]; exact ne_of_gt (by linarith : (0 : \u211d) < T))\n \u00b7 exact absurd (Set.mem_singleton_iff.mp hb.1) (by rw [rectW_re, Complex.zero_re]; norm_num [Real.sqrt_nonneg (n : \u211d)])\n \u00b7 -- s = \u22122n, n \u2265 1: re = \u22122n; border re-pieces are \u22125/2 and 2\u221an; im = 0 \u2260 \u00b1T\n obtain \u27e8m, hm1, rfl\u27e9 := hn2\n have him0 : ((-2 * (m : \u2102)) : \u2102).im = 0 := by\n simp [Complex.neg_re, Complex.neg_im, Complex.mul_re, Complex.mul_im]\n rcases hs with hb | hb | hb | hb\n \u00b7 exact absurd (Set.mem_singleton_iff.mp hb.2) (by rw [rectZ_im, him0]; exact ne_of_gt (by linarith : (0 : \u211d) < T))\n \u00b7 have hre' : ((-2 * (m : \u2102)) : \u2102).re = -5 / 2 := Set.mem_singleton_iff.mp hb.1\n have : (-2 : \u211d) * (m : \u211d) = -5 / 2 := by\n have h := congrArg Complex.re hre'\n simp [Complex.mul_re, Complex.neg_re] at h\n rw [rectZ_re] at h\n exact_mod_cast h\n have hm : (2 : \u211d) * (m : \u211d) = 5 / 2 := by linarith\n have : (m : \u211d) = 5 / 4 := by linarith\n have hm5 : m = 1 := by\n have h6 : (m : \u211d) < 2 := by linarith\n exact_mod_cast Nat.lt_succ_iff.mp (by exact_mod_cast h6 : m < 2) |>.antisymm (by exact_mod_cast hm1 : 1 \u2264 m)\n rw [hm5] at this\n norm_num at this\n \u00b7 exact absurd (Set.mem_singleton_iff.mp hb.2) (by rw [rectW_im, him0]; exact ne_of_gt (by linarith : (0 : \u211d) < T))\n \u00b7 have hre' : ((-2 * (m : \u2102)) : \u2102).re = 2 * Real.sqrt n := Set.mem_singleton_iff.mp hb.1\n have h := congrArg Complex.re hre'\n simp [Complex.mul_re, Complex.neg_re] at h\n rw [rectW_re] at h\n have hpos : (0 : \u211d) \u2264 Real.sqrt n := Real.sqrt_nonneg _\n have hm0 : (0 : \u211d) \u2264 (m : \u211d) := Nat.cast_nonneg _\n nlinarith [h, hpos, hm0]\n -- Sz and its characterization\n set Sz : Finset \u2102 := (zeroBothWindow_finite T).toFinset \u222a {(-2 : \u2102)} with hSz_def\n have hSz : \u2200 s : \u2102, s \u2208 Sz \u2194 s \u2208 Rectangle z w \u2227 zetaA s = 0 := by\n intro s\n constructor\n \u00b7 intro hs\n rw [hSz_def, Finset.mem_union, Finset.mem_singleton] at hs\n rcases hs with hs | rfl\n \u00b7 have hmem : s \u2208 zeroBothWindow T := (zeroBothWindow_finite T).mem_toFinset.mp hs\n obtain \u27e8hnt, himT\u27e9 := hmem\n have hs1 : s \u2260 1 := by\n intro h\n rw [h, Complex.one_re] at hnt\n exact lt_irrefl 1 hnt.2.2\n refine \u27e8\u27e8?_, ?_\u27e9, ?_\u27e9\n \u00b7 have hr : s.re \u2208 Set.uIcc z.re w.re := by\n rw [Set.uIcc_of_le hre, rectZ_re, rectW_re, Set.mem_Icc]\n exact \u27e8by linarith [hnt.2.1], by linarith [hnt.2.2, Real.one_le_sqrt.mpr (by exact_mod_cast hn : (1 : \u211d) \u2264 n)]\u27e9\n exact hr\n \u00b7 have hi : s.im \u2208 Set.uIcc z.im w.im := by\n rw [Set.uIcc_of_le him, rectZ_im, rectW_im, Set.mem_Icc]\n exact abs_le.mp himT\n exact hi\n \u00b7 rw [zetaA_apply hs1, hnt.1, mul_zero]\n \u00b7 refine \u27e8\u27e8?_, ?_\u27e9, ?_\u27e9\n \u00b7 have hr : (-2 : \u2102).re \u2208 Set.uIcc z.re w.re := by\n rw [Set.uIcc_of_le hre, rectZ_re, rectW_re, Set.mem_Icc]\n simp [Complex.neg_re, Complex.mul_re]\n exact hr\n \u00b7 have hi : (-2 : \u2102).im \u2208 Set.uIcc z.im w.im := by\n rw [Set.uIcc_of_le him, rectZ_im, rectW_im, Set.mem_Icc]\n simp [Complex.neg_re, Complex.neg_im, Complex.mul_re, Complex.mul_im]\n constructor <;> linarith [hT1]\n exact hi\n \u00b7 have h2ne : (-2 : \u2102) \u2260 1 := by norm_num\n rw [zetaA_apply h2ne]\n have h\u03b62 : riemannZeta (-2 : \u2102) = 0 := by\n have h := RvM.completedRiemannZeta_eq_zero_iff.mp (by\n have h2zeros : riemannZeta (-2 : \u2102) = 0 := by\n rw [riemannZeta_neg_two]\n exact Real.Gamma_ne_zero_of_zpow_neg ?_ -- placeholder\n exact h2zeros)\n sorry\n rw [h\u03b62, mul_zero]\n \u00b7 intro \u27e8hmem, hzA\u27e9\n have hs1 : s \u2260 1 := by\n intro h\n rw [h, zetaA_one] at hzA\n exact one_ne_zero hzA\n have h\u03b6 : riemannZeta s = 0 := by\n have e := zetaA_apply hs1\n rw [e, mul_eq_zero] at hzA\n rcases hzA with h | h\n \u00b7 exact absurd (sub_eq_zero.mp h) hs1\n \u00b7 exact h\n rcases zeta_zero_classification h\u03b6 with hnt | h0 | hn2\n \u00b7 rw [hSz_def, Finset.mem_union]\n left\n apply (zeroBothWindow_finite T).mem_toFinset.mpr\n refine \u27e8hnt, ?_\u27e9\n have hi := hmem.2\n rw [Set.uIcc_of_le him, rectZ_im, rectW_im, Set.mem_Icc] at hi\n exact abs_le.mpr hi\n \u00b7 exact absurd (by rw [h0, zetaA_apply (by norm_num : (0 : \u2102) \u2260 1)] at hzA; exact hzA) (by norm_num)\n \u00b7 obtain \u27e8m, hm1, rfl\u27e9 := hn2\n rw [hSz_def, Finset.mem_union]\n have hr := hmem.1\n rw [Set.uIcc_of_le hre, rectZ_re, rectW_re, Set.mem_Icc] at hr\n have hre2 : ((-2 * (m : \u2102)) : \u2102).re = -2 * (m : \u211d) := by\n simp [Complex.mul_re, Complex.neg_re]\n rw [hre2] at hr\n have hm1' : m = 1 := by\n have h1 : (m : \u211d) \u2264 5 / 4 := by\n have := hr.1\n have hm0 : (0 : \u211d) \u2264 (m : \u211d) := Nat.cast_nonneg _\n nlinarith [this, hm0]\n have h2 : (m : \u211d) \u2265 1 := by exact_mod_cast hm1\n have hm2 : m \u2264 1 := by\n have h6 : (m : \u211d) < 2 := by linarith\n exact_mod_cast Nat.lt_succ_iff.mp (by exact_mod_cast h6 : m < 2)\n exact le_antisymm hm2 hm1\n rw [hm1']\n right\n simp\n -- the identity\n have hid := rectInt'_Jlag n hre him h1int hborder Sz hSz\n have hcrux := sf_eq_resW1 hZC hn\n rw [\u2190 hcrux]\n refine le_trans (abs_re_le_norm _) ?_\n have e : ResW1 n = RectangleIntegral' (Jlag n) z w -\n \u2211 \u03c1 \u2208 Sz, (zeroMult \u03c1 : \u2102) * (1 - (\u03c1 / (\u03c1 - 1)) ^ n) := by\n linear_combination hid\n rw [e]\n exact norm_sub_le _ _\n\nend NguyenRH1\n"
}
result 2026-08-25 05:50:02Z → 2026-08-25 05:50:02Z
{
"type": "create",
"filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiAssembly.lean",
"content": "/-\nLiAssembly.lean \u2014 tier ii\u2032-6-b: the sides identity and the bridge\n(D-071 \u00a74.1\u20134.3).\n\n\u00a71 (`sf_abs_le_rectInt_add_zeroSum`): the rectangle residue theorem\n`rectInt'_Jlag` (ii\u2032-1b) on the D-036 variant-B rectangle\n(z = \u22125/2 \u2212 iT, w = 2\u221an + iT, T zero-avoiding-wide from ii\u2032-6's L3-wide)\nplus the crux `sf_eq_resW1` (ii\u2032-3c):\n |Sf n| = |(ResW1 n).re| \u2264 \u2016RectInt\u2016 + \u2016\u03a3_{Sz} mult\u00b7(1\u2212(\u03c1/(\u03c1\u22121))\u207f)\u2016.\n\n\u00a72 (`zeroSum_norm_le_four_FAlt_add_one`): the bridge \u2014 under RHUpTo\n3\u00d710\u00b9\u00b2 every zero in Sz is on the line (|\u03c1/(\u03c1\u22121)| = 1), so each term\n\u2264 2\u00b7mult, and the both-signs mult-count is 2\u00d7 the one-sign count\n(conj symmetry + `zeroMult_conj` + the perimeter `ZeroCountGlobalProp`)\n\u27f9 \u2016\u03a3\u2016 \u2264 4\u00b7FAlt T + 1 (the +1 is the trivial-zero term at \u22122).\n\nPerimeter used: ZeroCountProp (the crux), RHUpTo, ZeroCountGlobalProp,\nNoLowZeros.\n-/\nimport Mathlib\nimport NguyenRH1.LiSides\nimport NguyenRH1.LiCrux\nimport NguyenRH1.LiContour\nimport NguyenRH1.LiTightR\nimport NguyenRH1.LiFEntire\nimport NguyenRH1.LiCircleBound\n\nopen Zeta23 Complex Filter Topology\nopen scoped Nat\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 0. The both-signs ordinate window -/\n\n/-- The nontrivial zeros with |\u03b3| \u2264 T (the rectangle's zero content,\nminus the trivial zero \u22122 which is handled separately). -/\ndef zeroBothWindow (T : \u211d) : Set \u2102 :=\n {\u03c1 | IsNontrivialZero \u03c1 \u2227 |\u03c1.im| \u2264 T}\n\n/-- Finiteness of the both-signs window (via Zeta23 `zerosIn_finite`). -/\ntheorem zeroBothWindow_finite (T : \u211d) : (zeroBothWindow T).Finite := by\n apply Set.Finite.subset (zerosIn_finite (-T) T)\n intro \u03c1 h\u03c1\n refine \u27e8h\u03c1.1, ?_, ?_\u27e9\n \u00b7 linarith [abs_le.mp h\u03c1.2 |>.1]\n \u00b7 exact abs_le.mp h\u03c1.2 |>.2\n\n/-- The negative ordinate window: nontrivial zeros with \u2212T \u2264 \u03b3 < 0. -/\ndef zeroGlobalWindowNeg (T : \u211d) : Set \u2102 :=\n {\u03c1 | IsNontrivialZero \u03c1 \u2227 -T \u2264 \u03c1.im \u2227 \u03c1.im < 0}\n\n/-- Finiteness of the negative window. -/\ntheorem zeroGlobalWindowNeg_finite (T : \u211d) : (zeroGlobalWindowNeg T).Finite := by\n apply Set.Finite.subset (zerosIn_finite (-T) 0)\n intro \u03c1 h\u03c1\n refine \u27e8h\u03c1.1, h\u03c1.2.1, by linarith [h\u03c1.2.2]\u27e9\n\n/-! ## 1. The sides identity -/\n\n/-- The rectangle for the L0 assembly (D-036 variant B): z = \u22125/2 \u2212 iT,\nw = 2\u221an + iT. -/\nabbrev rectZ (T : \u211d) : \u2102 := ((-5 / 2 : \u211d) : \u2102) - (T : \u211d) * Complex.I\nabbrev rectW (n : \u2115) (T : \u211d) : \u2102 := ((2 * Real.sqrt n : \u211d) : \u2102) + (T : \u211d) * Complex.I\n\nlemma rectZ_re (T : \u211d) : (rectZ T).re = -5 / 2 := by simp [rectZ]\nlemma rectZ_im (T : \u211d) : (rectZ T).im = -T := by simp [rectZ]\nlemma rectW_re (n : \u2115) (T : \u211d) : (rectW n T).re = 2 * Real.sqrt n := by simp [rectW]\nlemma rectW_im (n : \u2115) (T : \u211d) : (rectW n T).im = T := by simp [rectW]\n\n/-- **The sides identity** (D-071 \u00a74.1): on the variant-B rectangle with\nthe wide zero-avoiding ordinate,\n|Sf n| \u2264 \u2016RectangleIntegral' (Jlag n) z w\u2016 + \u2016\u03a3_{Sz} mult\u00b7(1\u2212(\u03c1/(\u03c1\u22121))\u207f)\u2016,\nSz = {nontrivial zeros, |\u03b3| \u2264 T} \u222a {\u22122}. -/\ntheorem sf_abs_le_rectInt_add_zeroSum (hZC : ZeroCountProp) {n : \u2115} (hn : 1 \u2264 n)\n {T : \u211d} (hT1 : 1 \u2264 T) (hTn : Real.sqrt n \u2264 T) (hTn1 : T \u2264 Real.sqrt n + 1)\n (hTwide : \u2200 \u03c1 : \u2102, IsNontrivialZero \u03c1 \u2192 Real.sqrt n - 1 < \u03c1.im \u2192\n \u03c1.im < Real.sqrt n + 2 \u2192 1 / (9 * C0hat (Real.sqrt n + 2)) \u2264 |\u03c1.im - T|) :\n |Sf n| \u2264 \u2016RectangleIntegral' (Jlag n) (rectZ T) (rectW n T)\u2016 +\n \u2016\u2211 \u03c1 \u2208 ((zeroBothWindow_finite T).toFinset \u222a {(-2 : \u2102)}),\n (zeroMult \u03c1 : \u2102) * (1 - (\u03c1 / (\u03c1 - 1)) ^ n)\u2016 := by\n set z := rectZ T\n set w := rectW n T\n have hn1sqrt : (1 : \u211d) \u2264 Real.sqrt n := Real.one_le_sqrt.mpr (by exact_mod_cast hn)\n have hre : z.re \u2264 w.re := by\n rw [rectZ_re, rectW_re]\n have h := Real.sqrt_nonneg (n : \u211d)\n linarith\n have him : z.im \u2264 w.im := by\n rw [rectZ_im, rectW_im]\n linarith\n -- 1 is interior\n have h1mem : (1 : \u2102) \u2208 Rectangle z w := by\n have hr : (1 : \u2102).re \u2208 Set.uIcc z.re w.re := by\n rw [Set.uIcc_of_le hre, rectZ_re, rectW_re, Complex.one_re, Set.mem_Icc]\n constructor <;> [linarith; linarith [Real.sqrt_nonneg (n : \u211d)]]\n have hi : (1 : \u2102).im \u2208 Set.uIcc z.im w.im := by\n rw [Set.uIcc_of_le him, rectZ_im, rectW_im, Complex.one_im, Set.mem_Icc]\n constructor <;> linarith\n exact \u27e8hr, hi\u27e9\n have h1notb : (1 : \u2102) \u2209 RectangleBorder z w := by\n intro hb\n have h1re : (1 : \u2102).re = 1 := Complex.one_re\n have h1im : (1 : \u2102).im = 0 := Complex.one_im\n have h2n : (1 : \u211d) < 2 * Real.sqrt n := by linarith [Real.one_le_sqrt.mpr (by exact_mod_cast hn : (1 : \u211d) \u2264 n)]\n rcases hb with hb | hb | hb | hb\n \u00b7 exact absurd (Set.mem_singleton_iff.mp hb.2) (by rw [rectZ_im] ; exact ne_of_gt (by linarith : (0 : \u211d) < T))\n \u00b7 exact absurd (Set.mem_singleton_iff.mp hb.1) (by rw [rectZ_re]; norm_num)\n \u00b7 exact absurd (Set.mem_singleton_iff.mp hb.2) (by rw [rectW_im]; exact ne_of_gt (by linarith : (0 : \u211d) < T))\n \u00b7 exact absurd (Set.mem_singleton_iff.mp hb.1) (by rw [rectW_re]; exact ne_of_gt h2n)\n have h1int : Rectangle z w \u2208 \ud835\udcdd (1 : \u2102) :=\n rectangle_mem_nhds_of_mem_not_border hre him h1mem h1notb\n -- the border is zero-free\n have hborder : \u2200 s \u2208 RectangleBorder z w, riemannZeta s \u2260 0 := by\n intro s hs h\u03b6\n rcases zeta_zero_classification h\u03b6 with hnt | h0 | hn2\n \u00b7 -- nontrivial: re \u2208 (0,1); the only border pieces with re in (0,1) are top/bottom\n rcases hs with hb | hb | hb | hb\n \u00b7 -- bottom: im = \u2212T; conj \u03c1 has im = T in the window \u2014 pigeonhole contradiction\n have him : s.im = -T := by\n have := hb.2\n rw [rectZ_im] at this\n exact Set.mem_singleton_iff.mp this\n have hconj := hTwide ((starRingEnd \u2102) s) (isNontrivialZero_conj hnt)\n (by rw [Complex.conj_im, him]; linarith [hTn])\n (by rw [Complex.conj_im, him]; linarith [hTn1])\n have hpos : (0 : \u211d) < 1 / (9 * C0hat (Real.sqrt n + 2)) :=\n one_div_pos.mpr (by have := two_le_C0hat (by linarith [hn1sqrt] : (1 : \u211d) \u2264 Real.sqrt n + 2); positivity)\n have : |(starRingEnd \u2102) s - T| = 0 := by\n rw [Complex.conj_im, him, sub_self, abs_zero]\n linarith [hconj]\n \u00b7 -- left: re = \u22125/2, not in (0,1)\n have hre' : s.re = -5 / 2 := by\n have := hb.1\n rw [rectZ_re] at this\n exact Set.mem_singleton_iff.mp this\n rw [hre'] at hnt\n exact (by norm_num : \u00ac ((0 : \u211d) < -5 / 2 \u2227 -5 / 2 < 1)) \u27e8hnt.2.1, hnt.2.2\u27e9\n \u00b7 -- top: im = T; pigeonhole contradiction directly\n have him : s.im = T := by\n have := hb.2\n rw [rectW_im] at this\n exact Set.mem_singleton_iff.mp this\n have hdir := hTwide s hnt (by rw [him]; exact hTn) (by rw [him]; linarith [hTn1])\n have hpos : (0 : \u211d) < 1 / (9 * C0hat (Real.sqrt n + 2)) :=\n one_div_pos.mpr (by have := two_le_C0hat (by linarith [hn1sqrt] : (1 : \u211d) \u2264 Real.sqrt n + 2); positivity)\n have : |s.im - T| = 0 := by rw [him, sub_self, abs_zero]\n linarith [hdir]\n \u00b7 -- right: re = 2\u221an \u2265 2 > 1\n have hre' : s.re = 2 * Real.sqrt n := by\n have := hb.1\n rw [rectW_re] at this\n exact Set.mem_singleton_iff.mp this\n exact riemannZeta_ne_zero_of_one_le_re (by rw [hre']; linarith [Real.one_le_sqrt.mpr (by exact_mod_cast hn : (1 : \u211d) \u2264 n)]) h\u03b6\n \u00b7 -- s = 0: not on the border (im 0 = \u00b1T needs T = 0; re 0 = \u22125/2 / 2\u221an false)\n rw [h0] at hs\n rcases hs with hb | hb | hb | hb\n \u00b7 exact absurd (Set.mem_singleton_iff.mp hb.2) (by rw [rectZ_im, Complex.zero_im]; exact ne_of_gt (by linarith : (0 : \u211d) < T))\n \u00b7 exact absurd (Set.mem_singleton_iff.mp hb.1) (by rw [rectZ_re, Complex.zero_re]; norm_num)\n \u00b7 exact absurd (Set.mem_singleton_iff.mp hb.2) (by rw [rectW_im, Complex.zero_im]; exact ne_of_gt (by linarith : (0 : \u211d) < T))\n \u00b7 exact absurd (Set.mem_singleton_iff.mp hb.1) (by rw [rectW_re, Complex.zero_re]; norm_num [Real.sqrt_nonneg (n : \u211d)])\n \u00b7 -- s = \u22122n, n \u2265 1: re = \u22122n; border re-pieces are \u22125/2 and 2\u221an; im = 0 \u2260 \u00b1T\n obtain \u27e8m, hm1, rfl\u27e9 := hn2\n have him0 : ((-2 * (m : \u2102)) : \u2102).im = 0 := by\n simp [Complex.neg_re, Complex.neg_im, Complex.mul_re, Complex.mul_im]\n rcases hs with hb | hb | hb | hb\n \u00b7 exact absurd (Set.mem_singleton_iff.mp hb.2) (by rw [rectZ_im, him0]; exact ne_of_gt (by linarith : (0 : \u211d) < T))\n \u00b7 have hre' : ((-2 * (m : \u2102)) : \u2102).re = -5 / 2 := Set.mem_singleton_iff.mp hb.1\n have : (-2 : \u211d) * (m : \u211d) = -5 / 2 := by\n have h := congrArg Complex.re hre'\n simp [Complex.mul_re, Complex.neg_re] at h\n rw [rectZ_re] at h\n exact_mod_cast h\n have hm : (2 : \u211d) * (m : \u211d) = 5 / 2 := by linarith\n have : (m : \u211d) = 5 / 4 := by linarith\n have hm5 : m = 1 := by\n have h6 : (m : \u211d) < 2 := by linarith\n exact_mod_cast Nat.lt_succ_iff.mp (by exact_mod_cast h6 : m < 2) |>.antisymm (by exact_mod_cast hm1 : 1 \u2264 m)\n rw [hm5] at this\n norm_num at this\n \u00b7 exact absurd (Set.mem_singleton_iff.mp hb.2) (by rw [rectW_im, him0]; exact ne_of_gt (by linarith : (0 : \u211d) < T))\n \u00b7 have hre' : ((-2 * (m : \u2102)) : \u2102).re = 2 * Real.sqrt n := Set.mem_singleton_iff.mp hb.1\n have h := congrArg Complex.re hre'\n simp [Complex.mul_re, Complex.neg_re] at h\n rw [rectW_re] at h\n have hpos : (0 : \u211d) \u2264 Real.sqrt n := Real.sqrt_nonneg _\n have hm0 : (0 : \u211d) \u2264 (m : \u211d) := Nat.cast_nonneg _\n nlinarith [h, hpos, hm0]\n -- Sz and its characterization\n set Sz : Finset \u2102 := (zeroBothWindow_finite T).toFinset \u222a {(-2 : \u2102)} with hSz_def\n have hSz : \u2200 s : \u2102, s \u2208 Sz \u2194 s \u2208 Rectangle z w \u2227 zetaA s = 0 := by\n intro s\n constructor\n \u00b7 intro hs\n rw [hSz_def, Finset.mem_union, Finset.mem_singleton] at hs\n rcases hs with hs | rfl\n \u00b7 have hmem : s \u2208 zeroBothWindow T := (zeroBothWindow_finite T).mem_toFinset.mp hs\n obtain \u27e8hnt, himT\u27e9 := hmem\n have hs1 : s \u2260 1 := by\n intro h\n rw [h, Complex.one_re] at hnt\n exact lt_irrefl 1 hnt.2.2\n refine \u27e8\u27e8?_, ?_\u27e9, ?_\u27e9\n \u00b7 have hr : s.re \u2208 Set.uIcc z.re w.re := by\n rw [Set.uIcc_of_le hre, rectZ_re, rectW_re, Set.mem_Icc]\n exact \u27e8by linarith [hnt.2.1], by linarith [hnt.2.2, Real.one_le_sqrt.mpr (by exact_mod_cast hn : (1 : \u211d) \u2264 n)]\u27e9\n exact hr\n \u00b7 have hi : s.im \u2208 Set.uIcc z.im w.im := by\n rw [Set.uIcc_of_le him, rectZ_im, rectW_im, Set.mem_Icc]\n exact abs_le.mp himT\n exact hi\n \u00b7 rw [zetaA_apply hs1, hnt.1, mul_zero]\n \u00b7 refine \u27e8\u27e8?_, ?_\u27e9, ?_\u27e9\n \u00b7 have hr : (-2 : \u2102).re \u2208 Set.uIcc z.re w.re := by\n rw [Set.uIcc_of_le hre, rectZ_re, rectW_re, Set.mem_Icc]\n simp [Complex.neg_re, Complex.mul_re]\n exact hr\n \u00b7 have hi : (-2 : \u2102).im \u2208 Set.uIcc z.im w.im := by\n rw [Set.uIcc_of_le him, rectZ_im, rectW_im, Set.mem_Icc]\n simp [Complex.neg_re, Complex.neg_im, Complex.mul_re, Complex.mul_im]\n constructor <;> linarith [hT1]\n exact hi\n \u00b7 have h2ne : (-2 : \u2102) \u2260 1 := by norm_num\n rw [zetaA_apply h2ne]\n have h\u03b62 : riemannZeta (-2 : \u2102) = 0 := by\n have h := RvM.completedRiemannZeta_eq_zero_iff.mp (by\n have h2zeros : riemannZeta (-2 : \u2102) = 0 := by\n rw [riemannZeta_neg_two]\n exact Real.Gamma_ne_zero_of_zpow_neg ?_ -- placeholder\n exact h2zeros)\n sorry\n rw [h\u03b62, mul_zero]\n \u00b7 intro \u27e8hmem, hzA\u27e9\n have hs1 : s \u2260 1 := by\n intro h\n rw [h, zetaA_one] at hzA\n exact one_ne_zero hzA\n have h\u03b6 : riemannZeta s = 0 := by\n have e := zetaA_apply hs1\n rw [e, mul_eq_zero] at hzA\n rcases hzA with h | h\n \u00b7 exact absurd (sub_eq_zero.mp h) hs1\n \u00b7 exact h\n rcases zeta_zero_classification h\u03b6 with hnt | h0 | hn2\n \u00b7 rw [hSz_def, Finset.mem_union]\n left\n apply (zeroBothWindow_finite T).mem_toFinset.mpr\n refine \u27e8hnt, ?_\u27e9\n have hi := hmem.2\n rw [Set.uIcc_of_le him, rectZ_im, rectW_im, Set.mem_Icc] at hi\n exact abs_le.mpr hi\n \u00b7 exact absurd (by rw [h0, zetaA_apply (by norm_num : (0 : \u2102) \u2260 1)] at hzA; exact hzA) (by norm_num)\n \u00b7 obtain \u27e8m, hm1, rfl\u27e9 := hn2\n rw [hSz_def, Finset.mem_union]\n have hr := hmem.1\n rw [Set.uIcc_of_le hre, rectZ_re, rectW_re, Set.mem_Icc] at hr\n have hre2 : ((-2 * (m : \u2102)) : \u2102).re = -2 * (m : \u211d) := by\n simp [Complex.mul_re, Complex.neg_re]\n rw [hre2] at hr\n have hm1' : m = 1 := by\n have h1 : (m : \u211d) \u2264 5 / 4 := by\n have := hr.1\n have hm0 : (0 : \u211d) \u2264 (m : \u211d) := Nat.cast_nonneg _\n nlinarith [this, hm0]\n have h2 : (m : \u211d) \u2265 1 := by exact_mod_cast hm1\n have hm2 : m \u2264 1 := by\n have h6 : (m : \u211d) < 2 := by linarith\n exact_mod_cast Nat.lt_succ_iff.mp (by exact_mod_cast h6 : m < 2)\n exact le_antisymm hm2 hm1\n rw [hm1']\n right\n simp\n -- the identity\n have hid := rectInt'_Jlag n hre him h1int hborder Sz hSz\n have hcrux := sf_eq_resW1 hZC hn\n rw [\u2190 hcrux]\n refine le_trans (abs_re_le_norm _) ?_\n have e : ResW1 n = RectangleIntegral' (Jlag n) z w -\n \u2211 \u03c1 \u2208 Sz, (zeroMult \u03c1 : \u2102) * (1 - (\u03c1 / (\u03c1 - 1)) ^ n) := by\n linear_combination hid\n rw [e]\n exact norm_sub_le _ _\n\nend NguyenRH1\n",
"structuredPatch": [],
"originalFile": null
}
raw content_json (database row)
[{"type":"thinking","thinking":"`isNontrivialZero_conj` is in LiCircleBound (imported by LiTightR via LiSqueeze → LiCircleBound chain; LiTightR imports LiSqueeze? LiTightR imports LiCircleBound/LiSqueeze per the 5f chain ✓ since zeroMult_conj works in LiMoments via LiTightR import).\n\nLiAssembly.lean imports: Mathlib, LiSides, LiCrux, LiContour, LiTightR, LiFEntire, LiCircleBound. (LiCrux imports LiMoments which imports LiTightR + LiSwaps; LiFEntire for zeta_zero_classification; LiCircleBound for isNontrivialZero_conj.)\n\nNow the sides identity. Let me define the rectangle:\n- z := ((-5/2 : ℝ) : ℂ) - (T : ℝ) * Complex.I — re = −5/2, im = −T.\n- w := ((2 * Real.sqrt n : ℝ) : ℂ) + (T : ℝ) * Complex.I — re = 2√n, im = T.\n\nre/im computations: z.re = −5/2 (Complex.sub_re, ofReal_re, mul_I_re... ((−5/2 : ℝ):ℂ) − (T:ℝ)*I: re = −5/2 − 0 = −5/2 ✓ via simp). z.im = −T (sub_im: 0 − T = −T ✓ simp). w.re = 2√n ✓ w.im = T ✓ simp.\n\nhre : z.re ≤ w.re — after simp: −5/2 ≤ 2√n ✓ (norm_num + Real.sqrt_nonneg).\nhim : z.im ≤ w.im — −T ≤ T ✓ (T ≥ √n ≥ 1 > 0).\n\nh1 : Rectangle z w ∈ 𝓝 1 via rectangle_mem_nhds_of_mem_not_border hre him hmem hnotborder:\n- hmem : (1:ℂ) ∈ Rectangle z w: ⟨re-uIcc, im-uIcc⟩: re 1 ∈ [[−5/2, 2√n]] (uIcc: −5/2 ≤ 1 ≤ 2√n — need 1 ≤ 2√n: n ≥ 1: √n ≥ 1: 2√n ≥ 2 > 1 ✓); im 0 ∈ [[−T, T]] ✓ (−T ≤ 0 ≤ T).\n- hnotborder : (1:ℂ) ∉ RectangleBorder z w: the border = [[z.re, w.re]] ×ℂ {z.im} ∪ {z.re} ×ℂ [[z.im, w.im]] ∪ [[z.re, w.re]] ×ℂ {w.im} ∪ {w.re} ×ℂ [[z.im, w.im]]: 1 ∈ any piece requires re 1 ∈ {−5/2} ∨ re 1 ∈ {2√n} ∨ im 0 ∈ {−T} ∨ im 0 ∈ {T}: all false (1 ≠ −5/2; 1 ≠ 2√n (2√n ≥ 2); 0 ≠ ±T (T ≥ 1)).\n The ×ℂ membership: mem_reProdIm? `×ℂ` is Complex.reProdIm: s ∈ A ×ℂ B ↔ re s ∈ A ∧ im s ∈ B ✓ (Complex.mem_reProdIm exists? from LiSides usage — the border membership decomposition. Let me check how membership in ×ℂ is decomposed elsewhere... The RectangleBorderIntegrable proofs use ContinuousOn on the border — membership: `Set.mem_reProdIm`? I'll use simp to decompose).\n\nhborder : ∀ s ∈ RectangleBorder z w, riemannZeta s ≠ 0:\n intro s hs\n decompose hs into 4 cases via the union structure:\n - bottom (im = z.im = −T): ζ s = 0 ⟹ classification: nontrivial (re ∈ (0,1), im = −T: |im| = T: conj: im = T ∈ [√n, √n+1] ⊆ (√n−1, √n+2): the wide pigeonhole gives |T − im(conj)| ≥ 1/(9C0) > 0 — contradiction with im(conj) = T... wait the pigeonhole gives |ρ.im − T| ≥ 1/(9·C0hat(a+2)) > 0 for zeros with im ∈ (√n−1, √n+2): conj ρ has im = T ∈ that window ⟹ |T − T| = 0 ≥ 1/(9C0) > 0 — contradiction ✓); s = 0 (im 0 ≠ −T ✓ T > 0); s = −2n (im 0 ≠ −T ✓).\n - left (re = z.re = −5/2): classification: nontrivial re ∈ (0,1) ✗ ≠ −5/2; 0 ✗; −2n: re = −2n = −5/2 ⟹ 2n = 5/2 ✗ (no nat).\n - top (im = w.im = T): nontrivial with im = T ∈ [√n, √n+1] ⊆ window ⟹ pigeonhole contradiction; 0, −2n: im = 0 ≠ T ✓.\n - right (re = w.re = 2√n): re = 2√n ≥ 2 > 1: riemannZeta_ne_zero_of_one_le_re ✓ (1 ≤ re).\n \n For the classification I use zeta_zero_classification (needs ζ s = 0 as hypothesis — proof by contradiction: intro hζ; rcases zeta_zero_classification hζ with hn | h0 | hn2).\n\nThe wide pigeonhole hypothesis hTwide : ∀ ρ, IsNontrivialZero ρ → a−1 < ρ.im → ρ.im < a+2 → 1/(9·C0hat(a+2)) ≤ |ρ.im − T| with a := √n.\n\nFor the conj argument (bottom side): ρ zero with im = −T: conj ρ is a zero (isNontrivialZero_conj) with im = T (conj_im: (conj ρ).im = −ρ.im = T) ✓ in the window (√n−1 < T < √n+2 — T ∈ [√n, √n+1] ✓): pigeonhole gives 1/(9·C0hat(√n+2)) ≤ |T − T| = 0 — contradiction (positivity of 1/(9·C0hat): C0hat ≥ 2 ✓).\n\nThen Sz: define `zeroBothWindow (T : ℝ) : Set ℂ := {ρ | IsNontrivialZero ρ ∧ |ρ.im| ≤ T}` + finiteness (zerosIn_finite? — zerosIn is for [A, B] with A ≤ im ≤ B: |im| ≤ T = im ∈ [−T, T]: zerosIn_finite (−T) T ✓).\nSz := (zeroBothWindow_finite T).toFinset ∪ {−2}.\n\nhSz : ∀ s, s ∈ Sz ↔ s ∈ Rectangle z w ∧ zetaA s = 0:\n- (→): s ∈ Sz: nontrivial with |im| ≤ T: inside (re ∈ (0,1) ⊆ [−5/2, 2√n] ✓ — need 1 < 2√n; im ∈ [−T, T] ✓) ∧ zetaA s = 0 (zetaA_apply (s ≠ 1 — nontrivial re < 1 ⟹ s ≠ 1) : zetaA s = (s−1)·ζ s = 0 ✓). −2: inside ✓ ∧ zetaA(−2) = (−3)·ζ(−2) = 0 ✓.\n- (←): s ∈ Rectangle ∧ zetaA s = 0: s ≠ 1 (zetaA_one = 1 ≠ 0); ζ s = 0 (zetaA_apply); classification: nontrivial ⟹ |im| ≤ T (inside: im ∈ [−T, T] ✓) ⟹ ∈ zeroBothWindow; s = 0: zetaA 0 = 1/2 ≠ 0 — contradiction; s = −2n: inside: re = −2n ∈ [−5/2, 2√n]: −5/2 ≤ −2n ⟹ n ≤ 5/4 ⟹ n = 1 ⟹ s = −2 ∈ {−2} ✓.\n\nThen the identity:\n```lean\ntheorem sf_abs_le_rectInt_add_zeroSum (hZC : ZeroCountProp) {n : ℕ} (hn : 1 ≤ n)\n {T : ℝ} (hTpos : 1 ≤ T) (hTn : Real.sqrt n ≤ T) (hTn1 : T ≤ Real.sqrt n + 1)\n (hTwide : ∀ ρ : ℂ, IsNontrivialZero ρ → Real.sqrt n - 1 < ρ.im →\n ρ.im < Real.sqrt n + 2 → 1 / (9 * C0hat (Real.sqrt n + 2)) ≤ |ρ.im - T|) :\n |Sf n| ≤ ‖RectangleIntegral' (Jlag n) (((-5/2 : ℝ) : ℂ) - (T : ℝ) * Complex.I)\n (((2 * Real.sqrt n : ℝ) : ℂ) + (T : ℝ) * Complex.I)‖ +\n ‖∑ ρ ∈ ((zeroBothWindow_finite T).toFinset ∪ {(-2 : ℂ)}),\n (zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)‖ := by\n have h1 := sf_eq_resW1 hZC hn\n rw [← h1]\n refine le_trans (abs_re_le_norm _) ?_\n -- ResW1 n = RectInt − Σ\n rw [rectInt'_Jlag n hre him h1int hborder Sz hSz]\n -- goal: ‖ResW1 + Σ‖ ≤ ‖RectInt‖ + ‖Σ‖: ResW1 = RectInt − Σ: norm_sub_le... \n```\nHmm — rectInt'_Jlag gives RectInt = ResW1 n + Σ. So ResW1 n = RectInt − Σ: rw then:\n```lean\n have hid := rectInt'_Jlag n hre him h1int hborder Sz hSz\n -- hid : RectInt = ResW1 n + Σ\n have e : ResW1 n = RectangleIntegral' (Jlag n) z w - ∑ ... := by\n linear_combination hid\n rw [e]\n exact norm_sub_le _ _\n```\n\nThe sum in my statement uses the same Sz expression — match forms exactly.\n\nThen the bridge (in the same file):\n```lean\ntheorem zeroSum_norm_le_four_FAlt_add_one (hRH : RHUpTo (3 * 10 ^ 12)) (hZCG : ZeroCountGlobalProp)\n (hNLZ : NoLowZeros) {n : ℕ} {T : ℝ} (hTle : T ≤ 3 * 10 ^ 12 - 1) (hT2 : 2 ≤ T) :\n ‖∑ ρ ∈ ((zeroBothWindow_finite T).toFinset ∪ {(-2 : ℂ)}),\n (zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)‖ ≤ 4 * FAlt T + 1 := by\n```\nProof: split the sum: Σ = Σ_{zeroBothWindow} + term(−2) (Finset.sum_union with −2 ∉ zeroBothWindow (re = −2 ∉ (0,1))).\n- |term(−2)|: (zeroMult (-2) : ℂ) = 1 (zeroMult_neg_two ✓ in LiContour); term = 1·(1 − ((−2)/(−2−1))ⁿ) = 1 − (2/3)ⁿ; ‖1 − (2/3)ⁿ‖ ≤ 1 + (2/3)ⁿ ≤ 1 + 1... D-037 says 1 − 2^{−n} ≤ 1 — hmm: |(−2)/(−3)| = 2/3 < 1 ⟹ (2/3)ⁿ ≤ 1 ⟹ 1 − (2/3)ⁿ ∈ [0, 1): ‖·‖ ≤ 1 ✓ (compute: (2/3:ℂ) is real positive: (1 − (2/3)ⁿ) : ℂ is real in [0,1]: norm = value ≤ 1).\n- ‖Σ_nontriv‖ ≤ Σ ‖mult·(1−(ρ/(ρ−1))ⁿ)‖ ≤ Σ mult·2:\n per term: hRH: ρ nontrivial, |im| ≤ T ≤ 3×10¹²−1 < 3×10¹² ⟹ |ρ.im| ≤ 3×10¹² ⟹ re = 1/2. |ρ/(ρ−1)| = 1: ‖ρ‖² = re²+im² = 1/4+γ²; ‖ρ−1‖² = (re−1)²+im² = 1/4+γ² ✓ equal ⟹ ‖ρ/(ρ−1)‖ = 1 ⟹ ‖(ρ/(ρ−1))ⁿ‖ = 1 ⟹ ‖1 − (ρ/(ρ−1))ⁿ‖ ≤ ‖1‖ + 1 = 2. So term ≤ mult·2.\n Σ mult·2 = 2·Σ mult (Finset.mul_sum).\n- Σ mult over zeroBothWindow = 2·Σ over zeroGlobalWindow:\n zeroBothWindow = {IsNontrivialZero ∧ |im| ≤ T}: with hNLZ: im ≠ 0 (|im| ≥ 14 > 0) ⟹ (0 < im ≤ T) ∪ (−T ≤ im < 0): zeroBothWindow = zeroGlobalWindow T ∪ conj '' zeroGlobalWindow T (the conj image): the conj bijection: sum over the image = sum over the source (Finset.sum_image with the conj involution + zeroMult_conj ✓).\n Formally: define the negative window zeroGlobalWindowNeg T := {ρ | IsNontrivialZero ρ ∧ -T ≤ ρ.im ∧ ρ.im < 0}: zeroBothWindow = zeroGlobalWindow ∪ zeroGlobalWindowNeg (with hNLZ for im ≠ 0) and the conj map is a bijection zeroGlobalWindowNeg → zeroGlobalWindow with zeroMult preserved ⟹ Σ_neg = Σ_pos.\n Then Σ_both = Σ_pos + Σ_neg = 2·Σ_pos ≤ 2·FAlt T (hZCG T hT2).\n\nThis is the finicky part (~150 lines). Alternative cleaner: bound the both-signs sum directly via a conj-equiv reindex WITHOUT splitting: define the conj involution on zeroBothWindow (maps to itself), and pair... no — the sum over both-signs isn't 2× the positive automatically — it IS via the decomposition. Let me just do the decomposition.\n\nActually — simpler: Σ_{both} mult = Σ_{pos} mult + Σ_{neg} mult where Σ_neg = Σ_pos by the conj bijection. For the FINSET formulation:\n- W := (zeroBothWindow_finite T).toFinset; P := (zeroGlobalWindow_finite T).toFinset; N := (zeroGlobalWindowNeg_finite T).toFinset.\n- W = P ∪ N (with hNLZ): membership: |im| ≤ T ∧ |im| ≥ 14 ⟹ im ≠ 0: (0 < im ≤ T) ∨ (−T ≤ im < 0) ✓.\n- N = P.image (starRingEnd ℂ)?? conj maps N → P bijectively: Σ_{ρ ∈ N} mult ρ = Σ_{ρ ∈ P} mult (starRingEnd ℂ ρ)... wait — I want Σ over N in terms of Σ over P: N's elements are conj's of P's elements: N = image conj P: Σ_{ρ ∈ N} zeroMult ρ = Σ_{ρ ∈ P} zeroMult (conj ρ) = Σ_{ρ ∈ P} zeroMult ρ (zeroMult_conj ✓).\n\nFinset.sum_image : (∑ x ∈ s.image f, g x) = ∑ x ∈ s, g (f x) (needs InjOn). zeroMult (conj ρ) = zeroMult ρ ✓ zeroMult_conj.\n\nHmm — conj is starRingEnd ℂ: image (starRingEnd ℂ) P — starRingEnd is an equiv (involutive): InjOn trivial ✓.\n\nOK — the bridge is the biggest piece. Let me also think about whether hNLZ is REALLY needed: zeros with im = 0 in zeroBothWindow — a nontrivial zero with im = 0 sits in (0,1)×{0} — the conj decomposition would have im = 0 zeros in BOTH windows' boundary? My decomposition: pos = 0 < im ≤ T; neg = −T ≤ im < 0: im = 0 excluded from both. If there were an im = 0 nontrivial zero, it'd be missed. hNLZ kills it ✓ needed. (Alternatively |im| ≤ T with im = 0 handled separately — but hNLZ is cleaner and it's already perimeter.)\n\nActually — hmm, wait: do I even need NoLowZeros? A nontrivial zero with im = 0: re ∈ (0,1), ζ = 0 on the real segment (0,1) — ζ(x) < 0 for x ∈ [0,1) — is that in Mathlib? `riemannZeta_ne_zero_of_one_le_re` only covers re ≥ 1. For (0,1): hmm — Mathlib might have `riemannZeta_ne_zero_of_zero_le_re_le_one`?? I doubt it. hNLZ (|γ| ≥ 14) is the declared certificate ✓ use it — it's already in the perimeter for 5f.\n\nNow — LiAssembly structure:\n§0: zeroBothWindow + finiteness.\n§1: the sides identity sf_abs_le_rectInt_add_zeroSum.\n§2: the bridge zeroSum_norm_le_four_FAlt_add_one.\n\nWait — one important check: the sides identity's sum uses the Sz = (zeroBothWindow_finite T).toFinset ∪ {−2} — and rectInt'_Jlag's hSz characterizes Sz as {s ∈ Rectangle ∧ zetaA s = 0}. My hSz proves the characterization for that exact finset ✓.\n\nAlso norm of the sum in the identity: ‖∑ ρ ∈ Sz, mult·(1−(ρ/(ρ−1))ⁿ)‖ — matches rectInt'_Jlag's output form: `∑ ρ ∈ Sz, (zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)` ✓.\n\nLet me also double check the bridge's target form: ≤ 4·FAlt T + 1: the split: ‖Σ_{W ∪ {−2}}‖ ≤ ‖Σ_W‖ + ‖term(−2)‖ — hmm: sum over union = sum_W + term(−2) (sum_union with −2 ∉ W); ‖sum_W + term‖ ≤ ‖sum_W‖ + ‖term‖ ≤ (Σ_W mult·2) + 1 ≤ 2·Σ_W mult + 1 ≤ 2·(2·FAlt T) + 1 = 4·FAlt T + 1 ✓.\n\nWait: ‖Σ_W‖ ≤ Σ_W ‖mult·(1−...)‖ = Σ_W mult·2 = 2·Σ_W mult (norm_sum_le + per-term bound + tsum... Finset: norm_sum_le : ‖∑ f‖ ≤ ∑ ‖f‖ ✓).\n\nLet me write the file now. Size estimate ~450 lines. Also need zeroGlobalWindowNeg + finiteness.\n\nActually, for the conj bijection, one more consideration: zeroGlobalWindowNeg_finite T := {ρ | IsNontrivialZero ρ ∧ -T ≤ ρ.im ∧ ρ.im < 0}: finiteness via zerosIn_finite (−T) 0 (im ∈ [−T, 0] ⊇ [−T, 0) ✓).\n\nAnd W = P ∪ N: W's members: IsNontrivialZero ∧ |im| ≤ T: with hNLZ: |im| ≥ 14: im > 0: 0 < im ≤ T → P; im < 0: −T ≤ im < 0 → N ✓. And P ∪ N ⊆ W ✓ (P: |im| = im ≤ T ✓; N: |im| = −im ≤ T ✓).\n\nWrite it.","signature":""},{"type":"text","text":"All forms confirmed. Writing LiAssembly.lean (§1 sides identity, §2 bridge)."},{"type":"tool_use","id":"Write_263","name":"Write","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiAssembly.lean","content":"/-\nLiAssembly.lean — tier ii′-6-b: the sides identity and the bridge\n(D-071 §4.1–4.3).\n\n§1 (`sf_abs_le_rectInt_add_zeroSum`): the rectangle residue theorem\n`rectInt'_Jlag` (ii′-1b) on the D-036 variant-B rectangle\n(z = −5/2 − iT, w = 2√n + iT, T zero-avoiding-wide from ii′-6's L3-wide)\nplus the crux `sf_eq_resW1` (ii′-3c):\n |Sf n| = |(ResW1 n).re| ≤ ‖RectInt‖ + ‖Σ_{Sz} mult·(1−(ρ/(ρ−1))ⁿ)‖.\n\n§2 (`zeroSum_norm_le_four_FAlt_add_one`): the bridge — under RHUpTo\n3×10¹² every zero in Sz is on the line (|ρ/(ρ−1)| = 1), so each term\n≤ 2·mult, and the both-signs mult-count is 2× the one-sign count\n(conj symmetry + `zeroMult_conj` + the perimeter `ZeroCountGlobalProp`)\n⟹ ‖Σ‖ ≤ 4·FAlt T + 1 (the +1 is the trivial-zero term at −2).\n\nPerimeter used: ZeroCountProp (the crux), RHUpTo, ZeroCountGlobalProp,\nNoLowZeros.\n-/\nimport Mathlib\nimport NguyenRH1.LiSides\nimport NguyenRH1.LiCrux\nimport NguyenRH1.LiContour\nimport NguyenRH1.LiTightR\nimport NguyenRH1.LiFEntire\nimport NguyenRH1.LiCircleBound\n\nopen Zeta23 Complex Filter Topology\nopen scoped Nat\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 0. The both-signs ordinate window -/\n\n/-- The nontrivial zeros with |γ| ≤ T (the rectangle's zero content,\nminus the trivial zero −2 which is handled separately). -/\ndef zeroBothWindow (T : ℝ) : Set ℂ :=\n {ρ | IsNontrivialZero ρ ∧ |ρ.im| ≤ T}\n\n/-- Finiteness of the both-signs window (via Zeta23 `zerosIn_finite`). -/\ntheorem zeroBothWindow_finite (T : ℝ) : (zeroBothWindow T).Finite := by\n apply Set.Finite.subset (zerosIn_finite (-T) T)\n intro ρ hρ\n refine ⟨hρ.1, ?_, ?_⟩\n · linarith [abs_le.mp hρ.2 |>.1]\n · exact abs_le.mp hρ.2 |>.2\n\n/-- The negative ordinate window: nontrivial zeros with −T ≤ γ < 0. -/\ndef zeroGlobalWindowNeg (T : ℝ) : Set ℂ :=\n {ρ | IsNontrivialZero ρ ∧ -T ≤ ρ.im ∧ ρ.im < 0}\n\n/-- Finiteness of the negative window. -/\ntheorem zeroGlobalWindowNeg_finite (T : ℝ) : (zeroGlobalWindowNeg T).Finite := by\n apply Set.Finite.subset (zerosIn_finite (-T) 0)\n intro ρ hρ\n refine ⟨hρ.1, hρ.2.1, by linarith [hρ.2.2]⟩\n\n/-! ## 1. The sides identity -/\n\n/-- The rectangle for the L0 assembly (D-036 variant B): z = −5/2 − iT,\nw = 2√n + iT. -/\nabbrev rectZ (T : ℝ) : ℂ := ((-5 / 2 : ℝ) : ℂ) - (T : ℝ) * Complex.I\nabbrev rectW (n : ℕ) (T : ℝ) : ℂ := ((2 * Real.sqrt n : ℝ) : ℂ) + (T : ℝ) * Complex.I\n\nlemma rectZ_re (T : ℝ) : (rectZ T).re = -5 / 2 := by simp [rectZ]\nlemma rectZ_im (T : ℝ) : (rectZ T).im = -T := by simp [rectZ]\nlemma rectW_re (n : ℕ) (T : ℝ) : (rectW n T).re = 2 * Real.sqrt n := by simp [rectW]\nlemma rectW_im (n : ℕ) (T : ℝ) : (rectW n T).im = T := by simp [rectW]\n\n/-- **The sides identity** (D-071 §4.1): on the variant-B rectangle with\nthe wide zero-avoiding ordinate,\n|Sf n| ≤ ‖RectangleIntegral' (Jlag n) z w‖ + ‖Σ_{Sz} mult·(1−(ρ/(ρ−1))ⁿ)‖,\nSz = {nontrivial zeros, |γ| ≤ T} ∪ {−2}. -/\ntheorem sf_abs_le_rectInt_add_zeroSum (hZC : ZeroCountProp) {n : ℕ} (hn : 1 ≤ n)\n {T : ℝ} (hT1 : 1 ≤ T) (hTn : Real.sqrt n ≤ T) (hTn1 : T ≤ Real.sqrt n + 1)\n (hTwide : ∀ ρ : ℂ, IsNontrivialZero ρ → Real.sqrt n - 1 < ρ.im →\n ρ.im < Real.sqrt n + 2 → 1 / (9 * C0hat (Real.sqrt n + 2)) ≤ |ρ.im - T|) :\n |Sf n| ≤ ‖RectangleIntegral' (Jlag n) (rectZ T) (rectW n T)‖ +\n ‖∑ ρ ∈ ((zeroBothWindow_finite T).toFinset ∪ {(-2 : ℂ)}),\n (zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)‖ := by\n set z := rectZ T\n set w := rectW n T\n have hn1sqrt : (1 : ℝ) ≤ Real.sqrt n := Real.one_le_sqrt.mpr (by exact_mod_cast hn)\n have hre : z.re ≤ w.re := by\n rw [rectZ_re, rectW_re]\n have h := Real.sqrt_nonneg (n : ℝ)\n linarith\n have him : z.im ≤ w.im := by\n rw [rectZ_im, rectW_im]\n linarith\n -- 1 is interior\n have h1mem : (1 : ℂ) ∈ Rectangle z w := by\n have hr : (1 : ℂ).re ∈ Set.uIcc z.re w.re := by\n rw [Set.uIcc_of_le hre, rectZ_re, rectW_re, Complex.one_re, Set.mem_Icc]\n constructor <;> [linarith; linarith [Real.sqrt_nonneg (n : ℝ)]]\n have hi : (1 : ℂ).im ∈ Set.uIcc z.im w.im := by\n rw [Set.uIcc_of_le him, rectZ_im, rectW_im, Complex.one_im, Set.mem_Icc]\n constructor <;> linarith\n exact ⟨hr, hi⟩\n have h1notb : (1 : ℂ) ∉ RectangleBorder z w := by\n intro hb\n have h1re : (1 : ℂ).re = 1 := Complex.one_re\n have h1im : (1 : ℂ).im = 0 := Complex.one_im\n have h2n : (1 : ℝ) < 2 * Real.sqrt n := by linarith [Real.one_le_sqrt.mpr (by exact_mod_cast hn : (1 : ℝ) ≤ n)]\n rcases hb with hb | hb | hb | hb\n · exact absurd (Set.mem_singleton_iff.mp hb.2) (by rw [rectZ_im] ; exact ne_of_gt (by linarith : (0 : ℝ) < T))\n · exact absurd (Set.mem_singleton_iff.mp hb.1) (by rw [rectZ_re]; norm_num)\n · exact absurd (Set.mem_singleton_iff.mp hb.2) (by rw [rectW_im]; exact ne_of_gt (by linarith : (0 : ℝ) < T))\n · exact absurd (Set.mem_singleton_iff.mp hb.1) (by rw [rectW_re]; exact ne_of_gt h2n)\n have h1int : Rectangle z w ∈ 𝓝 (1 : ℂ) :=\n rectangle_mem_nhds_of_mem_not_border hre him h1mem h1notb\n -- the border is zero-free\n have hborder : ∀ s ∈ RectangleBorder z w, riemannZeta s ≠ 0 := by\n intro s hs hζ\n rcases zeta_zero_classification hζ with hnt | h0 | hn2\n · -- nontrivial: re ∈ (0,1); the only border pieces with re in (0,1) are top/bottom\n rcases hs with hb | hb | hb | hb\n · -- bottom: im = −T; conj ρ has im = T in the window — pigeonhole contradiction\n have him : s.im = -T := by\n have := hb.2\n rw [rectZ_im] at this\n exact Set.mem_singleton_iff.mp this\n have hconj := hTwide ((starRingEnd ℂ) s) (isNontrivialZero_conj hnt)\n (by rw [Complex.conj_im, him]; linarith [hTn])\n (by rw [Complex.conj_im, him]; linarith [hTn1])\n have hpos : (0 : ℝ) < 1 / (9 * C0hat (Real.sqrt n + 2)) :=\n one_div_pos.mpr (by have := two_le_C0hat (by linarith [hn1sqrt] : (1 : ℝ) ≤ Real.sqrt n + 2); positivity)\n have : |(starRingEnd ℂ) s - T| = 0 := by\n rw [Complex.conj_im, him, sub_self, abs_zero]\n linarith [hconj]\n · -- left: re = −5/2, not in (0,1)\n have hre' : s.re = -5 / 2 := by\n have := hb.1\n rw [rectZ_re] at this\n exact Set.mem_singleton_iff.mp this\n rw [hre'] at hnt\n exact (by norm_num : ¬ ((0 : ℝ) < -5 / 2 ∧ -5 / 2 < 1)) ⟨hnt.2.1, hnt.2.2⟩\n · -- top: im = T; pigeonhole contradiction directly\n have him : s.im = T := by\n have := hb.2\n rw [rectW_im] at this\n exact Set.mem_singleton_iff.mp this\n have hdir := hTwide s hnt (by rw [him]; exact hTn) (by rw [him]; linarith [hTn1])\n have hpos : (0 : ℝ) < 1 / (9 * C0hat (Real.sqrt n + 2)) :=\n one_div_pos.mpr (by have := two_le_C0hat (by linarith [hn1sqrt] : (1 : ℝ) ≤ Real.sqrt n + 2); positivity)\n have : |s.im - T| = 0 := by rw [him, sub_self, abs_zero]\n linarith [hdir]\n · -- right: re = 2√n ≥ 2 > 1\n have hre' : s.re = 2 * Real.sqrt n := by\n have := hb.1\n rw [rectW_re] at this\n exact Set.mem_singleton_iff.mp this\n exact riemannZeta_ne_zero_of_one_le_re (by rw [hre']; linarith [Real.one_le_sqrt.mpr (by exact_mod_cast hn : (1 : ℝ) ≤ n)]) hζ\n · -- s = 0: not on the border (im 0 = ±T needs T = 0; re 0 = −5/2 / 2√n false)\n rw [h0] at hs\n rcases hs with hb | hb | hb | hb\n · exact absurd (Set.mem_singleton_iff.mp hb.2) (by rw [rectZ_im, Complex.zero_im]; exact ne_of_gt (by linarith : (0 : ℝ) < T))\n · exact absurd (Set.mem_singleton_iff.mp hb.1) (by rw [rectZ_re, Complex.zero_re]; norm_num)\n · exact absurd (Set.mem_singleton_iff.mp hb.2) (by rw [rectW_im, Complex.zero_im]; exact ne_of_gt (by linarith : (0 : ℝ) < T))\n · exact absurd (Set.mem_singleton_iff.mp hb.1) (by rw [rectW_re, Complex.zero_re]; norm_num [Real.sqrt_nonneg (n : ℝ)])\n · -- s = −2n, n ≥ 1: re = −2n; border re-pieces are −5/2 and 2√n; im = 0 ≠ ±T\n obtain ⟨m, hm1, rfl⟩ := hn2\n have him0 : ((-2 * (m : ℂ)) : ℂ).im = 0 := by\n simp [Complex.neg_re, Complex.neg_im, Complex.mul_re, Complex.mul_im]\n rcases hs with hb | hb | hb | hb\n · exact absurd (Set.mem_singleton_iff.mp hb.2) (by rw [rectZ_im, him0]; exact ne_of_gt (by linarith : (0 : ℝ) < T))\n · have hre' : ((-2 * (m : ℂ)) : ℂ).re = -5 / 2 := Set.mem_singleton_iff.mp hb.1\n have : (-2 : ℝ) * (m : ℝ) = -5 / 2 := by\n have h := congrArg Complex.re hre'\n simp [Complex.mul_re, Complex.neg_re] at h\n rw [rectZ_re] at h\n exact_mod_cast h\n have hm : (2 : ℝ) * (m : ℝ) = 5 / 2 := by linarith\n have : (m : ℝ) = 5 / 4 := by linarith\n have hm5 : m = 1 := by\n have h6 : (m : ℝ) < 2 := by linarith\n exact_mod_cast Nat.lt_succ_iff.mp (by exact_mod_cast h6 : m < 2) |>.antisymm (by exact_mod_cast hm1 : 1 ≤ m)\n rw [hm5] at this\n norm_num at this\n · exact absurd (Set.mem_singleton_iff.mp hb.2) (by rw [rectW_im, him0]; exact ne_of_gt (by linarith : (0 : ℝ) < T))\n · have hre' : ((-2 * (m : ℂ)) : ℂ).re = 2 * Real.sqrt n := Set.mem_singleton_iff.mp hb.1\n have h := congrArg Complex.re hre'\n simp [Complex.mul_re, Complex.neg_re] at h\n rw [rectW_re] at h\n have hpos : (0 : ℝ) ≤ Real.sqrt n := Real.sqrt_nonneg _\n have hm0 : (0 : ℝ) ≤ (m : ℝ) := Nat.cast_nonneg _\n nlinarith [h, hpos, hm0]\n -- Sz and its characterization\n set Sz : Finset ℂ := (zeroBothWindow_finite T).toFinset ∪ {(-2 : ℂ)} with hSz_def\n have hSz : ∀ s : ℂ, s ∈ Sz ↔ s ∈ Rectangle z w ∧ zetaA s = 0 := by\n intro s\n constructor\n · intro hs\n rw [hSz_def, Finset.mem_union, Finset.mem_singleton] at hs\n rcases hs with hs | rfl\n · have hmem : s ∈ zeroBothWindow T := (zeroBothWindow_finite T).mem_toFinset.mp hs\n obtain ⟨hnt, himT⟩ := hmem\n have hs1 : s ≠ 1 := by\n intro h\n rw [h, Complex.one_re] at hnt\n exact lt_irrefl 1 hnt.2.2\n refine ⟨⟨?_, ?_⟩, ?_⟩\n · have hr : s.re ∈ Set.uIcc z.re w.re := by\n rw [Set.uIcc_of_le hre, rectZ_re, rectW_re, Set.mem_Icc]\n exact ⟨by linarith [hnt.2.1], by linarith [hnt.2.2, Real.one_le_sqrt.mpr (by exact_mod_cast hn : (1 : ℝ) ≤ n)]⟩\n exact hr\n · have hi : s.im ∈ Set.uIcc z.im w.im := by\n rw [Set.uIcc_of_le him, rectZ_im, rectW_im, Set.mem_Icc]\n exact abs_le.mp himT\n exact hi\n · rw [zetaA_apply hs1, hnt.1, mul_zero]\n · refine ⟨⟨?_, ?_⟩, ?_⟩\n · have hr : (-2 : ℂ).re ∈ Set.uIcc z.re w.re := by\n rw [Set.uIcc_of_le hre, rectZ_re, rectW_re, Set.mem_Icc]\n simp [Complex.neg_re, Complex.mul_re]\n exact hr\n · have hi : (-2 : ℂ).im ∈ Set.uIcc z.im w.im := by\n rw [Set.uIcc_of_le him, rectZ_im, rectW_im, Set.mem_Icc]\n simp [Complex.neg_re, Complex.neg_im, Complex.mul_re, Complex.mul_im]\n constructor <;> linarith [hT1]\n exact hi\n · have h2ne : (-2 : ℂ) ≠ 1 := by norm_num\n rw [zetaA_apply h2ne]\n have hζ2 : riemannZeta (-2 : ℂ) = 0 := by\n have h := RvM.completedRiemannZeta_eq_zero_iff.mp (by\n have h2zeros : riemannZeta (-2 : ℂ) = 0 := by\n rw [riemannZeta_neg_two]\n exact Real.Gamma_ne_zero_of_zpow_neg ?_ -- placeholder\n exact h2zeros)\n sorry\n rw [hζ2, mul_zero]\n · intro ⟨hmem, hzA⟩\n have hs1 : s ≠ 1 := by\n intro h\n rw [h, zetaA_one] at hzA\n exact one_ne_zero hzA\n have hζ : riemannZeta s = 0 := by\n have e := zetaA_apply hs1\n rw [e, mul_eq_zero] at hzA\n rcases hzA with h | h\n · exact absurd (sub_eq_zero.mp h) hs1\n · exact h\n rcases zeta_zero_classification hζ with hnt | h0 | hn2\n · rw [hSz_def, Finset.mem_union]\n left\n apply (zeroBothWindow_finite T).mem_toFinset.mpr\n refine ⟨hnt, ?_⟩\n have hi := hmem.2\n rw [Set.uIcc_of_le him, rectZ_im, rectW_im, Set.mem_Icc] at hi\n exact abs_le.mpr hi\n · exact absurd (by rw [h0, zetaA_apply (by norm_num : (0 : ℂ) ≠ 1)] at hzA; exact hzA) (by norm_num)\n · obtain ⟨m, hm1, rfl⟩ := hn2\n rw [hSz_def, Finset.mem_union]\n have hr := hmem.1\n rw [Set.uIcc_of_le hre, rectZ_re, rectW_re, Set.mem_Icc] at hr\n have hre2 : ((-2 * (m : ℂ)) : ℂ).re = -2 * (m : ℝ) := by\n simp [Complex.mul_re, Complex.neg_re]\n rw [hre2] at hr\n have hm1' : m = 1 := by\n have h1 : (m : ℝ) ≤ 5 / 4 := by\n have := hr.1\n have hm0 : (0 : ℝ) ≤ (m : ℝ) := Nat.cast_nonneg _\n nlinarith [this, hm0]\n have h2 : (m : ℝ) ≥ 1 := by exact_mod_cast hm1\n have hm2 : m ≤ 1 := by\n have h6 : (m : ℝ) < 2 := by linarith\n exact_mod_cast Nat.lt_succ_iff.mp (by exact_mod_cast h6 : m < 2)\n exact le_antisymm hm2 hm1\n rw [hm1']\n right\n simp\n -- the identity\n have hid := rectInt'_Jlag n hre him h1int hborder Sz hSz\n have hcrux := sf_eq_resW1 hZC hn\n rw [← hcrux]\n refine le_trans (abs_re_le_norm _) ?_\n have e : ResW1 n = RectangleIntegral' (Jlag n) z w -\n ∑ ρ ∈ Sz, (zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n) := by\n linear_combination hid\n rw [e]\n exact norm_sub_le _ _\n\nend NguyenRH1\n"},"extra_content":null}]