[{"type":"thinking","thinking":"Not malware. Now write the scaffolding file §1. I'll write it in chunks and build after each. Chunk 1: header + Z2hat_mono + nearZerosSub_mult_sum_le + continuity helpers + Jlag_norm_eq + rectangle decomposition + HIntegral split + VIntegral norm + even symmetry.\n\nFor the even symmetry, the points: in VIntegral f x y₁ y₂ the point is `(x : ℝ) + y * Complex.I` with x y : ℝ — the cast is `((x : ℝ) : ℂ)`? In Zeta23 the def is `f (x + y * I)` — with x y : ℝ and I : ℂ, the `+` is ℂ + ℂ so x is coerced via ofReal. So the point is `((x : ℝ) : ℂ) + (y : ℝ) * Complex.I`. Hmm wait — `(y : ℝ) * Complex.I`: ℝ * ℂ — that's via `SMul`? No — in Lean4 Mathlib, ℝ * ℂ doesn't typecheck directly; it must be `((y : ℝ) : ℂ) * Complex.I` with the coercion inserted by the elaborator. The dog-leg file writes `(T : ℝ) * Complex.I` in def dogZ — so that form elaborates (via ↑). OK so the point form: `((x : ℝ) : ℂ) + ((y : ℝ) : ℂ) * Complex.I`.\n\nFor Jlag_conj application: Jlag_conj (n) (hs : s ≠ 1) : Jlag n ((starRingEnd ℂ) s) = (starRingEnd ℂ) (Jlag n s). With s = ((-5/2:ℝ):ℂ) + (t:ℝ)·I: starRingEnd s = ((-5/2:ℝ):ℂ) − (t:ℝ)·I = ((-5/2:ℝ):ℂ) + ((−t):ℝ)·I — a simp/ring normalization. DL-5 did exactly this (hid2 with `simp`).\n\nNow writing chunk 1. Also need:\n\n- `zeta_ne_zero_left_vertical {t : ℝ} : riemannZeta ((-5/2:ℝ) + t·I) ≠ 0` — via zeta_zero_classification: re = −5/2: not nontrivial (re ∈ (0,1)), not 0, not −2n (n ≥ 1: re = −2n ≤ −2, but −2n = −5/2 impossible since 2n = 5/2 not integer). Proof: intro hζ; rcases zeta_zero_classification hζ with hnt | h0 | hn2: hnt: re ∈ (0,1) but re = −5/2 ✗; h0: s = 0 ⟹ im t = 0 and re −5/2 = 0 ✗; hn2: s = −2·m: re: −5/2 = −2m ⟹ m = 5/4 ✗ (cast). This mirrors LiAssembly's border cases — write a standalone lemma for reuse (I_III integrability + capstone hζ hyps).\n\n- `zeta_ne_zero_horizontal (n ≥ ...) T-zero-avoiding`: for the mid-horizontal capstone hζ + integrability: s = σ + iT, σ ∈ [−5/2, 3]: ζ s ≠ 0: zeros = nontrivial ∪ {0} ∪ {−2n}: 0 and −2n have im = 0 ≠ T (T ≥ 316) ✓; nontrivial ρ with im = T: clearance from hTwide (T ∈ [√n, √n+1] window, zeros with γ ∈ (√n−1, √n+2) have |γ−T| ≥ c > 0; zeros outside have |γ−T| ≥ 1 > 0). So s ≠ ρ for all ρ ⟹ ζ s ≠ 0. The proof: intro hζ; rcases classification: hnt: ρ := s nontrivial with im = T: cases: if γ ∈ (√n−1, √n+2): hTwide gives 1/(9·C0hat) ≤ |T−T| = 0 ✗ (linarith with positivity); else |γ−T| ≥ 1: γ ≤ √n−1 ⟹ T−γ ≥ √n−γ ≥ 1 ✗ T = γ... wait s.im = T = γ means |γ−T| = 0 < 1 so γ ∈ (T−1, T+1) ⊆ (√n−1, √n+2) always!! So the \"outside\" case is vacuous: im = T exactly ⟹ γ = T ⟹ γ ∈ (√n−1, √n+2) ✓ hTwide applies ⟹ 0 < c ≤ 0 ✗. Clean.\n\nSo: `zeta_ne_zero_horizontal (hTwide ...) {σ T} (hσ : ...) (hTn : √n ≤ T) (hTn1 : T ≤ √n+1) : riemannZeta (σ + iT) ≠ 0` — needs hTwide as hypothesis (from exists_zero_avoiding_T_wide). Actually for the mid-horizontal and right-tail... the right tail σ ∈ [3, 2√n] is zero-free unconditionally (re ≥ 3 > 1 ✓ riemannZeta_ne_zero_of_one_le_re). The mid segment [−5/2, 3] needs the pigeonhole. Also I_I right vertical re = 2√n ≥ 2 ✓ unconditional. Left vertical re = −5/2 ✓ unconditional (classification).\n\nLet me now write chunk 1 of the file. I'll be careful with cast forms. Write, build, iterate.","signature":""},{"type":"text","text":"Writing the scaffolding chunk of `LiSideBounds.lean`."},{"type":"tool_use","id":"Write_47","name":"Write","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSideBounds.lean","content":"/-\nLiSideBounds.lean — tier ii′-6-c: the four side bounds of the L0\nassembly (D-071 §4.4 with the D-074 dog-leg horizontal and the F-E\nI_I repair, D-074 §9).\n\n§1 scaffolding: Z2hat_mono, the nearZerosSub mult-count bridge,\nlogDeriv continuity on the paths, the Jlag norm factorization, the\nrectangle side decomposition, HIntegral/VIntegral norm machinery,\nthe left-vertical even symmetry, and the two zero-freeness lemmas\n(left vertical by classification, horizontal by the wide pigeonhole).\n\n§2 (6-c-ii): I_III — the left vertical σ = −5/2.\n§3 (6-c-iii): I_I — the right vertical σ₁ = 2√n (F-E form: ≤ e^{1/3}·IIMaj).\n§4 (6-c-iv): the mid-horizontal segment machine [−5/2, 3].\n§5 (6-c-v): the full horizontal assembly (mid + DL-5 tails, both sides).\n\nPerimeter used: ZeroCountProp2 (near-count bridge), MZeroProp (I_III\nshort piece), the 5f tight R-bound hypotheses hZC/hZC2/hNLZ.\n-/\nimport Mathlib\nimport NguyenRH1.LiAssembly\nimport NguyenRH1.LiDogLeg\n\nopen Zeta23 Complex Filter Topology\nopen scoped Nat\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. Scaffolding -/\n\n/-- Z₂ is monotone for t ≥ 1 (clone of `C0hat_mono`, LiGapCircles). -/\ntheorem Z2hat_mono {a b : ℝ} (ha : 1 ≤ a) (hab : a ≤ b) : Z2hat a ≤ Z2hat b := by\n  have hapos : (0 : ℝ) < a + 2 := by linarith\n  have h1 : Real.log (a + 2) ≤ Real.log (b + 2) := Real.log_le_log hapos (by linarith)\n  have hlog1 : (1 : ℝ) ≤ Real.log (a + 2) := by\n    rw [Real.le_log_iff_exp_le hapos]\n    have he := Real.exp_one_lt_d9.le\n    linarith\n  have h2 : Real.log (Real.log (a + 2)) ≤ Real.log (Real.log (b + 2)) :=\n    Real.log_le_log (by linarith) h1\n  unfold Z2hat\n  have h3 : (0 : ℝ) ≤ (0.886 : ℝ) := by norm_num\n  have h4 : (0 : ℝ) ≤ (0.6 : ℝ) := by norm_num\n  nlinarith [h1, h2, h3, h4]\n\n/-- **The nearZerosSub mult-count bridge** (cloned from\n`near_sum_refPoint_le`, LiTightR §5): the multiplicity-weighted count\nof nearZerosSub t is ≤ Z₂(t) via the image/subset bridge and the\nperimeter `ZeroCountProp2`. -/\ntheorem nearZerosSub_mult_sum_le (hZC2 : ZeroCountProp2) {t : ℝ} (ht : 10 ≤ t) :\n    ∑ ρ ∈ nearZerosSub t, (zeroMult ρ.1 : ℝ) ≤ Z2hat t := by\n  classical\n  have hbridge : ∑ ρ ∈ nearZerosSub t, (zeroMult ρ.1 : ℝ)\n      = ∑ ρ ∈ (nearZerosSub t).image (fun ρ => ρ.1), (zeroMult ρ : ℝ) := by\n    rw [Finset.sum_image (fun x _ y _ h => Subtype.ext h)]\n  have hsub : (nearZerosSub t).image (fun ρ => ρ.1)\n      ⊆ (zeroAbsWindow_finite t).toFinset := by\n    intro ρ hρ\n    rw [Finset.mem_image] at hρ\n    obtain ⟨ρ', hρ'mem, hρ'eq⟩ := hρ\n    have hnear := mem_nearZerosSub.mp hρ'mem\n    rw [Set.Finite.mem_toFinset]\n    show IsNontrivialZero ρ ∧ |ρ.im - t| ≤ 1\n    rw [← hρ'eq]\n    exact ⟨ρ'.2, hnear.le⟩\n  calc ∑ ρ ∈ nearZerosSub t, (zeroMult ρ.1 : ℝ)\n      = ∑ ρ ∈ (nearZerosSub t).image (fun ρ => ρ.1), (zeroMult ρ : ℝ) := hbridge\n    _ ≤ ∑ ρ ∈ (zeroAbsWindow_finite t).toFinset, (zeroMult ρ : ℝ) :=\n        Finset.sum_le_sum_of_subset_of_nonneg hsub (fun ρ _ _ => Nat.cast_nonneg _)\n    _ = (((zeroAbsWindow_finite t).toFinset.sum fun ρ => zeroMult ρ) : ℝ) := rfl\n    _ ≤ Z2hat t := hZC2 t ht\n\n/-- logDeriv ζ is continuous at any point off the pole and off the\nzero set (analyticity of ζ + the quotient). -/\ntheorem continuousAt_logDeriv_zeta {s : ℂ} (h1 : s ≠ 1) (hζ : riemannZeta s ≠ 0) :\n    ContinuousAt (logDeriv riemannZeta) s := by\n  have hA : AnalyticAt ℂ (fun z => deriv riemannZeta z / riemannZeta z) s :=\n    ((analyticAt_riemannZeta h1).deriv).div (analyticAt_riemannZeta h1) hζ\n  have heq : logDeriv riemannZeta = fun z => deriv riemannZeta z / riemannZeta z := rfl\n  rw [heq]\n  exact hA.continuousAt\n\n/-- logDeriv ζ is continuous on a set avoiding the pole and the zeros. -/\ntheorem continuousOn_logDeriv_zeta {S : Set ℂ} (h1 : ∀ s ∈ S, s ≠ 1)\n    (hζ : ∀ s ∈ S, riemannZeta s ≠ 0) :\n    ContinuousOn (logDeriv riemannZeta) S :=\n  fun s hs => (continuousAt_logDeriv_zeta (h1 s hs) (hζ s hs)).continuousWithinAt\n\n/-- **The Jlag norm factorization**: Jlag = kFun · (−logDeriv ζ), so\nthe norm splits (logDeriv unfolds to deriv/ζ definitionally). -/\ntheorem Jlag_norm_eq (n : ℕ) (s : ℂ) :\n    ‖Jlag n s‖ = ‖kFun n s‖ * ‖logDeriv riemannZeta s‖ := by\n  unfold Jlag logDeriv\n  rw [norm_mul, norm_neg]\n\n/-- **Zero-freeness on the left vertical** σ = −5/2 (classification:\nnontrivial zeros have re ∈ (0,1), the others are 0 and −2n). -/\ntheorem zeta_ne_zero_left_vertical (t : ℝ) :\n    riemannZeta ((-5 / 2 : ℝ) + (t : ℝ) * Complex.I) ≠ 0 := by\n  intro hζ\n  have hre : (((-5 / 2 : ℝ) : ℂ) + (t : ℝ) * Complex.I).re = -5 / 2 := by simp\n  have him : (((-5 / 2 : ℝ) : ℂ) + (t : ℝ) * Complex.I).im = t := by simp\n  rcases zeta_zero_classification hζ with hnt | h0 | hn2\n  · rw [hre] at hnt\n    linarith [hnt.2.1]\n  · rw [h0] at hre\n    norm_num at hre\n  · obtain ⟨m, hm1, hs⟩ := hn2\n    have hre2 : ((-2 : ℂ) * (m : ℂ)).re = -2 * (m : ℝ) := by\n      simp [Complex.mul_re]\n    rw [hs] at hre\n    rw [hre2] at hre\n    have hm : (m : ℝ) = 5 / 4 := by linarith\n    have h12 : (1 : ℝ) ≤ (m : ℝ) := by exact_mod_cast hm1\n    have h2 : (m : ℝ) < 2 := by linarith\n    have hm2 : m = 1 := by\n      have : m < 2 := by exact_mod_cast h2\n      exact le_antisymm (Nat.lt_succ_iff.mp this) hm1\n    rw [hm2] at hm\n    norm_num at hm\n\n/-- **Zero-freeness on the horizontal at height T** (T the wide\nzero-avoiding ordinate): a zero on the path would be a nontrivial\nzero with γ = T inside the clearance window — contradiction.\n(The trivial zeros have im = 0 ≠ T.) -/\ntheorem zeta_ne_zero_horizontal {n : ℕ} {T : ℝ} {σ : ℝ}\n    (hTwide : ∀ ρ : ℂ, IsNontrivialZero ρ → Real.sqrt n - 1 < ρ.im →\n      ρ.im < Real.sqrt n + 2 → 1 / (9 * C0hat (Real.sqrt n + 2)) ≤ |ρ.im - T|)\n    (hn : 1 ≤ n) (hTn : Real.sqrt n ≤ T) (hTn1 : T ≤ Real.sqrt n + 1) :\n    riemannZeta ((σ : ℝ) + (T : ℝ) * Complex.I) ≠ 0 := by\n  intro hζ\n  have hre : (((σ : ℝ) : ℂ) + (T : ℝ) * Complex.I).re = σ := by simp\n  have him : (((σ : ℝ) : ℂ) + (T : ℝ) * Complex.I).im = T := by simp\n  have hT0 : (0 : ℝ) < T := by\n    have h1 : (1 : ℝ) ≤ Real.sqrt n := Real.one_le_sqrt.mpr (by exact_mod_cast hn)\n    linarith\n  rcases zeta_zero_classification hζ with hnt | h0 | hn2\n  · -- nontrivial with im = T: inside the clearance window\n    have hγ1 : Real.sqrt n - 1 < T := by linarith [Real.sqrt_nonneg (n : ℝ)]\n    have hγ2 : T < Real.sqrt n + 2 := by linarith\n    have hc := hTwide _ hnt (by rw [← him]; exact hγ1) (by rw [← him]; exact hγ2)\n    rw [← him, sub_self, abs_zero] at hc\n    have hpos : (0 : ℝ) < 1 / (9 * C0hat (Real.sqrt n + 2)) := by\n      have h2 := two_le_C0hat (by linarith [Real.sqrt_nonneg (n : ℝ)] :\n        (1 : ℝ) ≤ Real.sqrt n + 2)\n      exact one_div_pos.mpr (by linarith)\n    linarith\n  · rw [h0] at him\n    simp at him\n    linarith\n  · obtain ⟨m, hm1, hs⟩ := hn2\n    have him2 : ((-2 : ℂ) * (m : ℂ)).im = 0 := by simp [Complex.mul_im]\n    rw [hs] at him\n    rw [him2] at him\n    linarith\n\n/-- **The rectangle side decomposition** (Zeta23 def, at the variant-B\nrectangle coordinates). -/\ntheorem rectangleIntegral_Jlag_eq (n : ℕ) (T : ℝ) :\n    RectangleIntegral (Jlag n) (rectZ T) (rectW n T) =\n      HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt n) (-T) -\n        HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt n) T +\n        VIntegral (Jlag n) (2 * Real.sqrt n) (-T) T -\n        VIntegral (Jlag n) (-5 / 2) (-T) T := by\n  unfold RectangleIntegral\n  rw [rectZ_re, rectZ_im, rectW_re, rectW_im]\n\n/-- The norm of a VIntegral is the norm of the plain interval\nintegral (the I • factor has norm 1). -/\ntheorem VIntegral_norm {f : ℂ → ℂ} {x y₁ y₂ : ℝ} :\n    ‖VIntegral f x y₁ y₂‖ = ‖∫ t in y₁..y₂, f ((x : ℝ) + (t : ℝ) * Complex.I)‖ := by\n  unfold VIntegral\n  rw [norm_smul, Complex.norm_I, one_mul]\n\n/-- Splitting an HIntegral at an interior point (integrability\nhypotheses). -/\ntheorem HIntegral_split {f : ℂ → ℂ} {a b c y : ℝ}\n    (h1 : IntervalIntegrable (fun σ => f ((σ : ℝ) + (y : ℝ) * Complex.I))\n      MeasureTheory.volume a b)\n    (h2 : IntervalIntegrable (fun σ => f ((σ : ℝ) + (y : ℝ) * Complex.I))\n      MeasureTheory.volume b c) :\n    HIntegral f a c y = HIntegral f a b y + HIntegral f b c y := by\n  unfold HIntegral\n  rw [intervalIntegral.integral_add_adjacent_intervals h1 h2]\n\n/-- **The left-vertical even symmetry** (Jlag is conjugation-symmetric\nand the left-vertical point at −t is the conjugate of the one at t). -/\ntheorem jlag_left_vertical_norm_even (n : ℕ) (t : ℝ) :\n    ‖Jlag n ((-5 / 2 : ℝ) + (-t : ℝ) * Complex.I)‖ =\n      ‖Jlag n ((-5 / 2 : ℝ) + (t : ℝ) * Complex.I)‖ := by\n  have hconj : ((-5 / 2 : ℝ) : ℂ) + (-t : ℝ) * Complex.I =\n      (starRingEnd ℂ) (((-5 / 2 : ℝ) : ℂ) + (t : ℝ) * Complex.I) := by\n    simp\n  rw [hconj, Jlag_conj n (by\n    intro h\n    have hre : (((-5 / 2 : ℝ) : ℂ) + (t : ℝ) * Complex.I).re = -5 / 2 := by simp\n    rw [h] at hre\n    norm_num at hre), Complex.norm_conj]\n\nend NguyenRH1\n\nend\n"},"extra_content":null}]