← Session 30 — ii′-5e squeeze capstone + 5f perimeter repair
thinking (4012 chars)
- `div_le_div_of_nonneg_right (hab : a ≤ b) (hc : 0 ≤ c) : a / c ≤ b / c` ✓
- `div_mul_cancel₀ _ (h : b ≠ 0) : a / b * b = a` ✓ (usage in LiGapCircles confirms arg order: div_mul_cancel₀ _ hne).
- Nat.le_ceil: used in project? LiFEntire line 84: `Nat.le_ceil _` ✓ seen there (`Nat.le_ceil _ : ‖w‖ ≤ M`). Signature `Nat.le_ceil (a : ℝ) : a ≤ ↑⌈a⌉₊` ✓.
Now write the file. Let me assemble the complete LiSqueeze.lean carefully.
One remaining check — `Metric.mem_sphere.mp hz` gives `dist z 0 = R`? Metric.mem_sphere : z ∈ sphere x r ↔ dist z x = r ✓.
`dist_eq_norm : dist x y = ‖x - y‖` — for ℂ (SeminormedAddCommGroup) ✓ name is `dist_eq_norm` ✓.
For hz0mem the rewrite: rw [Metric.mem_ball, dist_eq_norm, sub_zero] — Metric.mem_ball : z ∈ ball x r ↔ dist z x < r; goal becomes dist z₀ 0 < R → ‖z₀ − 0‖ < R → ‖z₀‖ < R ✓.
Now, in hsphere: `intro z hz` — goal `z ∈ Metric.sphere (0:ℂ) R → ‖Gentire z‖ ≤ RB`? hsphere's statement: ∀ z ∈ Metric.sphere (0:ℂ) R, ... — intro z hz ✓.
After set RB, the hsphere statement I write with RB; the proof's final exact gentire_circle_le ... produces the unfolded form — defeq ✓.
Let me also decide: does `set RB` cause issues with hznorm etc.? No.
One more potential issue: in §4 I reference `Fexpr_circle_le` indirectly via `gentire_circle_le` — fine.
`AnalyticOn.norm_le_of_norm_le_on_sphere le_rfl hGan hsphere hz` — signature: (hyp_r : r ≤ R) (analytic : AnalyticOn ℂ f (closedBall 0 R)) (cond : ∀ z ∈ sphere 0 r, ‖f z‖ ≤ C) (wInS : w ∈ closedBall 0 r) : ‖f w‖ ≤ C. With r := R (our R), R := R: hyp_r : R ≤ R = le_rfl ✓. Implicit {C r R f w} — inferred ✓. BUT: name clash — our `R` vs lemma's `R`; fine.
Wait — the lemma's `f : ℂ → ℂ`, our Gentire ✓. Its `AnalyticOn ℂ f (Metric.closedBall 0 R)` — in the lemma statement it's written `Metric.closedBall 0 R`? From the source: `(analytic : AnalyticOn ℂ f (Metric.closedBall 0 R))` — the source shows `AnalyticOn ℂ f (Metric.closedBall 0 R)`? Looking at the code: `lemma AnalyticOn.norm_le_of_norm_le_on_sphere {C r R : ℝ} {f : ℂ → ℂ} {w : ℂ} (hyp_r : r ≤ R) (analytic : AnalyticOn ℂ f (Metric.closedBall 0 R)) (cond : ∀ z ∈ Metric.sphere 0 r, ‖f z‖ ≤ C) (wInS : w ∈ Metric.closedBall 0 r)`. Hmm the actual file showed `Metric.closedBall 0 R` — from my read: line 33-40 shows `(analytic : AnalyticOn ℂ f (Metric.closedBall 0 R))`, `(cond : ∀ z ∈ Metric.sphere 0 r, ‖f z‖ ≤ C)`, `(wInS : w ∈ Metric.closedBall 0 r)`. ✓ (it showed `Metric.closedBall` — well, the read showed `Metric.closedBall 0 R`? It showed "AnalyticOn ℂ f (Metric.closedBall 0 R)" — yes with Metric prefix.)
hGan : AnalyticOn ℂ Gentire (Metric.closedBall (0:ℂ) R) ✓ matches.
The `(0:ℂ)` vs `0` — fine.
Now assemble the whole §4 proof. One concern: the `key` block is long; Lean elaboration of a big proof is fine but errors need iteration. I'll write it, then compile with `lake env lean NguyenRH1/LiSqueeze.lean` and iterate.
Also the capstone §5.
And finally: root-import LiCircleBound + LiSqueeze in NguyenRH1.lean + update the header comment.
Let me also double-check `Real.log_le_log` signature: from usage `Real.log_le_log (by ... : (0:ℝ) < 2 + R/2) (...)` — hmm line 3894 was `apply Real.log_le_log (by linarith [hRpos] : (0 : ℝ) < 2 + R / 2)` — then remaining goal `2 + R/2 ≤ R`. So Real.log_le_log (hx : 0 < x) : x ≤ y → log x ≤ log y ✓.
`Real.le_log_iff_exp_le` used in two_le_C0hat ✓ not needed here.
Write the file now. Also — important detail: in §4, after `obtain ⟨R, hRlo, hRhi, hgapInt, hgap⟩ := exists_gapCircle_radius hZC (k := k) (by omega)`, the conjunction order: (4k+5/2 ≤ R) ∧ (R ≤ 4k+3) ∧ (∀ m:ℤ, ...) ∧ (∀ ρ, ...) ✓ per the signature I read.
Note the exists_gapCircle_radius hgap form: `1 / (16 * C0hat (4 * (k : ℝ) + 9 / 2))) ≤ |ρ.im - R| ∨ 1 ≤ |ρ.im - R|` — wait the exact statement from LiGapCircles:47-51: `(∀ ρ : ℂ, IsNontrivialZero ρ → (1 / (16 * C0hat (4 * (k : ℝ) + 9 / 2))) ≤ |ρ.im - R| ∨ 1 ≤ |ρ.im - R|)` ✓ matches Fexpr_circle_le's hgap form (modulo extra parens — same term).
Let me now write the file.
All names verified. Writing LiSqueeze.lean now.
tool: Write ok
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSqueeze.lean",
"content": "/-\nNguyenRH1/LiSqueeze.lean \u2014 tier ii\u2032 sub-stage ii\u2032-5e-v-d (D-068 \u00a75):\nthe Schwarz squeeze \u27f9 the partial-fraction capstone.\n\n\u00a71: the \u0108\u2080 growth bound `C0hat_add_two_le` (\u0108\u2080(R+2) \u2264 5\u00b7log R).\n\u00a72: `not_badPoint_on_gapCircle` \u2014 every point of a \u03b3-gap circle is good.\n\u00a73: `gentire_circle_le` \u2014 the Fexpr circle bound transferred to Gentire.\n\u00a74: `gentire_const` \u2014 max-modulus + Schwarz on the gap-circle sequence:\n the (log R)\u00b3/R \u2192 0 squeeze forces Gentire \u2261 Gentire 0.\n\u00a75: the capstone `partialFraction_identity (hZC : ZeroCountProp)`.\n\nArchive references: D-068 \u00a75, STATE.md session-034 next-action design.\n-/\nimport Mathlib\nimport NguyenRH1.LiCircleBound\n\nopen Zeta23 Complex Filter Topology\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. The \u0108\u2080 growth bound -/\n\n/-- \u0108\u2080(R+2) \u2264 5\u00b7log R for R \u2265 16002 (so log R \u2265 9): log(R+4) \u2264 2\u00b7log R,\nlog log(R+4) \u2264 2\u00b7log R, and 2.9 \u2264 (1/3)\u00b7log R; total 2.97\u00b7log R. -/\nlemma C0hat_add_two_le {R : \u211d} (hR : 16002 \u2264 R) :\n C0hat (R + 2) \u2264 5 * Real.log R := by\n have hRpos : (0 : \u211d) < R := by linarith\n have hlogR : (9 : \u211d) \u2264 Real.log R := nine_le_log_of_16002_le hR\n have h1 : Real.log (R + 2 + 2) \u2264 2 * Real.log R := by\n have hle : R + 2 + 2 \u2264 R ^ 2 := by nlinarith [hR]\n have h2 : Real.log (R + 2 + 2) \u2264 Real.log (R ^ 2) :=\n Real.log_le_log (by linarith : (0 : \u211d) < R + 2 + 2) hle\n rwa [Real.log_pow, Nat.cast_two] at h2\n have h2 : Real.log (Real.log (R + 2 + 2)) \u2264 2 * Real.log R := by\n have hpos1 : (0 : \u211d) < Real.log (R + 2 + 2) := by\n have hle : Real.log R \u2264 Real.log (R + 2 + 2) :=\n Real.log_le_log hRpos (by linarith)\n linarith [hlogR]\n have h3 : Real.log (Real.log (R + 2 + 2)) \u2264 Real.log (2 * Real.log R) :=\n Real.log_le_log hpos1 h1\n have h4 : Real.log (2 * Real.log R) = Real.log 2 + Real.log (Real.log R) := by\n rw [Real.log_mul (by norm_num) (by linarith [hlogR] : Real.log R \u2260 0)]\n have h5 : Real.log 2 \u2264 1 := by\n have h := Real.log_le_sub_one_of_pos (by norm_num : (0 : \u211d) < 2)\n linarith\n have h6 : Real.log (Real.log R) \u2264 Real.log R := by\n have h := Real.log_le_sub_one_of_pos (by linarith [hlogR] : (0 : \u211d) < Real.log R)\n linarith\n linarith [h3, h4, h5, h6, hlogR]\n unfold C0hat\n linarith [h1, h2, hlogR]\n\n/-! ## 2. Every \u03b3-gap-circle point is good -/\n\n/-- A point on a \u03b3-gap circle is not a bad point: not a nontrivial zero\n(the circle-bound lemma), not 0 or 1 (norm too large), not \u22122n (the\n\u2124-clearance of R/2). -/\nlemma not_badPoint_on_gapCircle {k : \u2115} (hk : 4000 \u2264 k) {R : \u211d}\n (hRlo : 4 * (k : \u211d) + 5 / 2 \u2264 R)\n (hgap : \u2200 \u03c1 : \u2102, IsNontrivialZero \u03c1 \u2192\n 1 / (16 * C0hat (4 * (k : \u211d) + 9 / 2)) \u2264 |\u03c1.im - R| \u2228 1 \u2264 |\u03c1.im - R|)\n (hgapInt : \u2200 m : \u2124, 1 / 4 \u2264 |R / 2 - (m : \u211d)|)\n {s : \u2102} (hs : \u2016s\u2016 = R) : \u00ac badPoint s := by\n have hR16002 : (16002 : \u211d) \u2264 R := by\n have h1 : (4000 : \u211d) \u2264 (k : \u211d) := by exact_mod_cast hk\n linarith [hRlo]\n have hRpos : (0 : \u211d) < R := by linarith [hR16002]\n rintro (h | h | h | \u27e8n, -, h\u27e9)\n \u00b7 exact not_isNontrivialZero_on_gapCircle hk hRlo hgap hs h\n \u00b7 rw [h, norm_zero] at hs\n linarith [hRpos]\n \u00b7 rw [h, norm_one] at hs\n linarith [hR16002]\n \u00b7 have hR2 : R = 2 * (n : \u211d) := by\n rw [\u2190 hs, h, norm_mul]\n have h1 : \u2016(-2 : \u2102)\u2016 = 2 := by\n rw [show (-2 : \u2102) = ((-2 : \u211d) : \u2102) by push_cast; ring, Complex.norm_real]\n norm_num\n rw [h1, Complex.norm_natCast]\n have hcon := hgapInt (n : \u2124)\n rw [Int.cast_natCast] at hcon\n have h0 : R / 2 - (n : \u211d) = 0 := by rw [hR2]; ring\n rw [h0, abs_zero] at hcon\n linarith [hcon]\n\n/-! ## 3. The circle bound for Gentire -/\n\n/-- The Fexpr circle bound transfers to Gentire on the \u03b3-gap circles\n(every circle point is good, so Gentire = Fexpr there). -/\ntheorem gentire_circle_le {k : \u2115} (hk : 4000 \u2264 k) {R : \u211d}\n (hRlo : 4 * (k : \u211d) + 5 / 2 \u2264 R) (hRhi : R \u2264 4 * (k : \u211d) + 3)\n (hgap : \u2200 \u03c1 : \u2102, IsNontrivialZero \u03c1 \u2192\n 1 / (16 * C0hat (4 * (k : \u211d) + 9 / 2)) \u2264 |\u03c1.im - R| \u2228 1 \u2264 |\u03c1.im - R|)\n (hgapInt : \u2200 m : \u2124, 1 / 4 \u2264 |R / 2 - (m : \u211d)|)\n {s : \u2102} (hs : \u2016s\u2016 = R) :\n \u2016Gentire s\u2016 \u2264 2 * lowZeroConst + dirichletC2 +\n 400000 * A0count * C0hat (R + 2) * (Real.log R) ^ 2 := by\n have hgood : \u00ac badPoint s := not_badPoint_on_gapCircle hk hRlo hgap hgapInt hs\n rw [gentire_eq_Fexpr hgood]\n exact Fexpr_circle_le hk hRlo hRhi hgap hgapInt hs\n\n/-! ## 4. The squeeze: Gentire is constant -/\n\n/-- **The Schwarz squeeze**: under the perimeter zero count, Gentire is\nconstant. For each \u03b5 > 0 pick a \u03b3-gap circle of radius R \u2265 16002 with\nR^{1/4} \u2265 2 + (128\u00b7C\u2081 + 2\u00b7C\u2080')\u00b7\u2016z\u2080\u2016/\u03b5; max-modulus bounds Gentire on the\nball by the circle bound, Schwarz then gives\ndist (Gentire z\u2080) (Gentire 0) \u2264 (C\u2080' + 64\u00b7C\u2081\u00b7R^{3/4})\u00b7\u2016z\u2080\u2016/R \u2264 \u03b5. -/\ntheorem gentire_const (hZC : ZeroCountProp) (z\u2080 : \u2102) : Gentire z\u2080 = Gentire 0 := by\n classical\n have hA0nn : (0 : \u211d) \u2264 A0count := A0count_pos.le\n have key : \u2200 \u03b5 : \u211d, 0 < \u03b5 \u2192 dist (Gentire z\u2080) (Gentire 0) \u2264 \u03b5 := by\n intro \u03b5 h\u03b5\n -- the constants\n set C\u2080' := 2 * lowZeroConst + dirichletC2 + \u2016Gentire 0\u2016 with hC0'\n set C\u2081 := 2000000 * A0count with hC1\n have hC\u2080'nn : (0 : \u211d) \u2264 C\u2080' := by\n rw [hC0']\n linarith [lowZeroConst_nonneg, dirichletC2_nonneg, norm_nonneg (Gentire 0)]\n have hC\u2081nn : (0 : \u211d) \u2264 C\u2081 := by\n rw [hC1]\n exact mul_nonneg (by norm_num) hA0nn\n set c := 2 + (128 * C\u2081 + 2 * C\u2080') * \u2016z\u2080\u2016 / \u03b5 with hc\n have hXnn : (0 : \u211d) \u2264 (128 * C\u2081 + 2 * C\u2080') * \u2016z\u2080\u2016 / \u03b5 :=\n div_nonneg (mul_nonneg (add_nonneg (mul_nonneg (by norm_num) hC\u2081nn)\n (mul_nonneg (by norm_num) hC\u2080'nn)) (norm_nonneg _)) h\u03b5.le\n have hcz : (2 : \u211d) \u2264 c := by rw [hc]; linarith [hXnn]\n have hcnn : (0 : \u211d) \u2264 c := by linarith [hcz]\n -- the radius choice\n set M := max (c ^ 4) (\u2016z\u2080\u2016 + 1) with hM\n obtain \u27e8k, hk4000, hkM\u27e9 : \u2203 k : \u2115, 4000 \u2264 k \u2227 M \u2264 4 * (k : \u211d) := by\n refine \u27e8max 4000 \u2308M / 4\u2309\u208a, le_max_left _ _, ?_\u27e9\n have h1 : M / 4 \u2264 (\u2308M / 4\u2309\u208a : \u211d) := Nat.le_ceil _\n have h2 : (\u2308M / 4\u2309\u208a : \u211d) \u2264 ((max 4000 \u2308M / 4\u2309\u208a : \u2115) : \u211d) := by\n exact_mod_cast le_max_right _ _\n linarith [h1, h2]\n obtain \u27e8R, hRlo, hRhi, hgapInt, hgap\u27e9 :=\n exists_gapCircle_radius hZC (k := k) (by omega)\n have hR16002 : (16002 : \u211d) \u2264 R := by\n have h1 : (4000 : \u211d) \u2264 (k : \u211d) := by exact_mod_cast hk4000\n linarith [hRlo]\n have hRpos : (0 : \u211d) < R := by linarith [hR16002]\n have hlogR : (9 : \u211d) \u2264 Real.log R := nine_le_log_of_16002_le hR16002\n have hMR : M \u2264 R := by linarith [hkM, hRlo]\n -- the circle bound on the sphere, then the ball by max-modulus\n set RB := 2 * lowZeroConst + dirichletC2 +\n 400000 * A0count * C0hat (R + 2) * (Real.log R) ^ 2 with hRB\n have hsphere : \u2200 z \u2208 Metric.sphere (0 : \u2102) R, \u2016Gentire z\u2016 \u2264 RB := by\n intro z hz\n have hznorm : \u2016z\u2016 = R := by\n have h := Metric.mem_sphere.mp hz\n rwa [dist_eq_norm, sub_zero] at h\n exact gentire_circle_le hk4000 hRlo hRhi hgap hgapInt hznorm\n have hGan : AnalyticOn \u2102 Gentire (Metric.closedBall 0 R) :=\n AnalyticOnNhd.analyticOn (fun s _ => gentire_analyticAt_and_eq.1 s)\n have hball : \u2200 z \u2208 Metric.closedBall (0 : \u2102) R, \u2016Gentire z\u2016 \u2264 RB :=\n fun z hz => AnalyticOn.norm_le_of_norm_le_on_sphere le_rfl hGan hsphere hz\n -- the Schwarz inputs\n have hmaps : Set.MapsTo Gentire (Metric.ball 0 R)\n (Metric.closedBall (Gentire 0) (RB + \u2016Gentire 0\u2016)) := by\n intro z hz\n have hzball : z \u2208 Metric.closedBall (0 : \u2102) R := by\n rw [Metric.mem_ball] at hz\n rw [Metric.mem_closedBall]\n exact hz.le\n have h1 := hball z hzball\n rw [Metric.mem_closedBall, dist_eq_norm]\n calc \u2016Gentire z - Gentire 0\u2016 \u2264 \u2016Gentire z\u2016 + \u2016Gentire 0\u2016 := norm_sub_le _ _\n _ \u2264 RB + \u2016Gentire 0\u2016 := by linarith [h1]\n have hdiff : DifferentiableOn \u2102 Gentire (Metric.ball 0 R) :=\n fun z _ => (gentire_analyticAt_and_eq.1 z).differentiableAt.differentiableWithinAt\n have hz0mem : z\u2080 \u2208 Metric.ball (0 : \u2102) R := by\n rw [Metric.mem_ball, dist_eq_norm, sub_zero]\n have h1 : \u2016z\u2080\u2016 + 1 \u2264 M := le_max_right _ _\n linarith [hMR]\n have hschwarz := Complex.dist_le_div_mul_dist_of_mapsTo_ball hdiff hmaps hz0mem\n -- the growth estimates: RB + \u2016Gentire 0\u2016 \u2264 C\u2080' + 64\u00b7C\u2081\u00b7Q\u00b3, R = Q\u2074\n set Q := R ^ ((4 : \u211d)\u207b\u00b9) with hQ\n have hQnn : (0 : \u211d) \u2264 Q := Real.rpow_nonneg hRpos.le _\n have hQpos : (0 : \u211d) < Q := Real.rpow_pos_of_pos hRpos _\n have hQc : c \u2264 Q := by\n have hc4 : c ^ 4 \u2264 R := by\n have h : c ^ 4 \u2264 M := le_max_left _ _\n linarith [hMR]\n have h1 : c = (c ^ 4) ^ ((4 : \u211d)\u207b\u00b9) := by\n have h := (Real.pow_rpow_inv_natCast hcnn (show (4 : \u2115) \u2260 0 by norm_num)).symm\n push_cast at h\n exact h\n have h2 : (c ^ 4) ^ ((4 : \u211d)\u207b\u00b9) \u2264 Q :=\n Real.rpow_le_rpow (pow_nonneg (by linarith [hcz] : (0 : \u211d) \u2264 c) 4) hc4\n (by positivity : (0 : \u211d) \u2264 (4 : \u211d)\u207b\u00b9)\n rw [h1]\n exact h2\n have hL : Real.log R \u2264 4 * Q := by\n have h := Real.log_le_rpow_div hRpos.le (show (0 : \u211d) < (4 : \u211d)\u207b\u00b9 by positivity)\n have h2 : R ^ ((4 : \u211d)\u207b\u00b9) / (4 : \u211d)\u207b\u00b9 = 4 * (R ^ ((4 : \u211d)\u207b\u00b9)) := by\n rw [div_eq_mul_inv, inv_inv]\n ring\n rwa [h2] at h\n have hL3 : (Real.log R) ^ 3 \u2264 64 * Q ^ 3 := by\n have h1 : (Real.log R) ^ 3 \u2264 (4 * Q) ^ 3 :=\n pow_le_pow_left\u2080 (by linarith [hlogR]) hL 3\n have h2 : (4 * Q) ^ 3 = 64 * Q ^ 3 := by ring\n rwa [h2] at h1\n have hR4 : R = Q ^ 4 := by\n have h := Real.rpow_inv_natCast_pow hRpos.le (show (4 : \u2115) \u2260 0 by norm_num)\n push_cast at h\n rw [\u2190 hQ] at h\n exact h.symm\n have h\u01085 : C0hat (R + 2) \u2264 5 * Real.log R := C0hat_add_two_le hR16002\n have hbig : 400000 * A0count * C0hat (R + 2) * (Real.log R) ^ 2\n \u2264 64 * C\u2081 * Q ^ 3 := by\n have hlogRnn : (0 : \u211d) \u2264 Real.log R := by linarith [hlogR]\n have h1 : 400000 * A0count * C0hat (R + 2) * (Real.log R) ^ 2\n \u2264 400000 * A0count * (5 * Real.log R) * (Real.log R) ^ 2 := by\n apply mul_le_mul_of_nonneg_right _ (pow_nonneg hlogRnn 2)\n exact mul_le_mul_of_nonneg_left h\u01085\n (mul_nonneg (by norm_num : (0 : \u211d) \u2264 400000) hA0nn)\n have h2 : 400000 * A0count * (5 * Real.log R) * (Real.log R) ^ 2\n = C\u2081 * (Real.log R) ^ 3 := by\n rw [hC1]\n ring\n have h3 : C\u2081 * (Real.log R) ^ 3 \u2264 64 * C\u2081 * Q ^ 3 := by\n have h := mul_le_mul_of_nonneg_left hL3 hC\u2081nn\n have h' : C\u2081 * (64 * Q ^ 3) = 64 * C\u2081 * Q ^ 3 := by ring\n rwa [h'] at h\n linarith [h1, h2, h3]\n have hRBle : RB + \u2016Gentire 0\u2016 \u2264 C\u2080' + 64 * C\u2081 * Q ^ 3 := by\n rw [hRB, hC0']\n linarith [hbig]\n -- the real squeeze: (RB + \u2016Gentire 0\u2016)/R\u00b7\u2016z\u2080\u2016 \u2264 \u03b5\n have hc1 : 128 * C\u2081 * \u2016z\u2080\u2016 \u2264 \u03b5 * Q := by\n have h1 : (128 * C\u2081 + 2 * C\u2080') * \u2016z\u2080\u2016 / \u03b5 \u2264 c := by rw [hc]; linarith\n have h2 : (128 * C\u2081) * \u2016z\u2080\u2016 \u2264 (128 * C\u2081 + 2 * C\u2080') * \u2016z\u2080\u2016 := by\n apply mul_le_mul_of_nonneg_right _ (norm_nonneg _)\n linarith [hC\u2080'nn]\n have h3 : (128 * C\u2081) * \u2016z\u2080\u2016 / \u03b5 \u2264 c :=\n (div_le_div_of_nonneg_right h2 h\u03b5.le).trans h1\n calc (128 * C\u2081) * \u2016z\u2080\u2016 = (128 * C\u2081) * \u2016z\u2080\u2016 / \u03b5 * \u03b5 := by\n rw [div_mul_cancel\u2080 _ h\u03b5.ne']\n _ \u2264 c * \u03b5 := mul_le_mul_of_nonneg_right h3 h\u03b5.le\n _ \u2264 Q * \u03b5 := mul_le_mul_of_nonneg_right hQc h\u03b5.le\n _ = \u03b5 * Q := by ring\n have hA : 64 * C\u2081 * Q ^ 3 * \u2016z\u2080\u2016 \u2264 (\u03b5 / 2) * Q ^ 4 := by\n have h1 : (64 * C\u2081 * \u2016z\u2080\u2016) * Q ^ 3 \u2264 ((\u03b5 / 2) * Q) * Q ^ 3 := by\n apply mul_le_mul_of_nonneg_right _ (pow_nonneg hQnn 3)\n have h64 : (64 : \u211d) * C\u2081 * \u2016z\u2080\u2016 = (128 * C\u2081 * \u2016z\u2080\u2016) / 2 := by ring\n have hhalf : (\u03b5 / 2) * Q = (\u03b5 * Q) / 2 := by ring\n rw [h64, hhalf]\n linarith [hc1]\n have hL' : (64 * C\u2081 * \u2016z\u2080\u2016) * Q ^ 3 = 64 * C\u2081 * Q ^ 3 * \u2016z\u2080\u2016 := by ring\n have hR' : ((\u03b5 / 2) * Q) * Q ^ 3 = (\u03b5 / 2) * Q ^ 4 := by ring\n rwa [hL', hR'] at h1\n have hB : C\u2080' * \u2016z\u2080\u2016 \u2264 (\u03b5 / 2) * Q ^ 4 := by\n have h1 : (2 * C\u2080') * \u2016z\u2080\u2016 \u2264 \u03b5 * Q := by\n have h2 : (2 * C\u2080') * \u2016z\u2080\u2016 \u2264 (128 * C\u2081 + 2 * C\u2080') * \u2016z\u2080\u2016 := by\n apply mul_le_mul_of_nonneg_right _ (norm_nonneg _)\n linarith [hC\u2081nn]\n have h3 : (128 * C\u2081 + 2 * C\u2080') * \u2016z\u2080\u2016 / \u03b5 \u2264 c := by rw [hc]; linarith\n have h4 : (2 * C\u2080') * \u2016z\u2080\u2016 / \u03b5 \u2264 c :=\n (div_le_div_of_nonneg_right h2 h\u03b5.le).trans h3\n calc (2 * C\u2080') * \u2016z\u2080\u2016 = (2 * C\u2080') * \u2016z\u2080\u2016 / \u03b5 * \u03b5 := by\n rw [div_mul_cancel\u2080 _ h\u03b5.ne']\n _ \u2264 c * \u03b5 := mul_le_mul_of_nonneg_right h4 h\u03b5.le\n _ \u2264 Q * \u03b5 := mul_le_mul_of_nonneg_right hQc h\u03b5.le\n _ = \u03b5 * Q := by ring\n have hQ2 : (2 : \u211d) \u2264 Q := by linarith [hQc, hcz]\n have hQ3 : (2 : \u211d) \u2264 Q ^ 3 := by\n have h := pow_le_pow_left\u2080 (by norm_num : (0 : \u211d) \u2264 2) hQ2 3\n norm_num at h\n linarith [h]\n have h2 : \u03b5 * Q \u2264 (\u03b5 / 2) * Q ^ 4 := by\n have h3 : (\u03b5 / 2) * Q ^ 4 = ((\u03b5 / 2) * Q) * Q ^ 3 := by ring\n rw [h3]\n have h6 : (\u03b5 / 2) * Q * 2 \u2264 (\u03b5 / 2) * Q * Q ^ 3 :=\n mul_le_mul_of_nonneg_left hQ3 (by positivity)\n have h5 : \u03b5 * Q = (\u03b5 / 2) * Q * 2 := by ring\n rw [h5]\n exact h6\n have h7 : C\u2080' * \u2016z\u2080\u2016 \u2264 2 * C\u2080' * \u2016z\u2080\u2016 := by\n have h : (0 : \u211d) \u2264 C\u2080' * \u2016z\u2080\u2016 := mul_nonneg hC\u2080'nn (norm_nonneg _)\n linarith [h]\n linarith [h7, h1, h2]\n have hsum : (RB + \u2016Gentire 0\u2016) * \u2016z\u2080\u2016 \u2264 \u03b5 * Q ^ 4 := by\n have h1 : (RB + \u2016Gentire 0\u2016) * \u2016z\u2080\u2016 \u2264 (C\u2080' + 64 * C\u2081 * Q ^ 3) * \u2016z\u2080\u2016 :=\n mul_le_mul_of_nonneg_right hRBle (norm_nonneg _)\n have h2 : (C\u2080' + 64 * C\u2081 * Q ^ 3) * \u2016z\u2080\u2016\n = C\u2080' * \u2016z\u2080\u2016 + 64 * C\u2081 * Q ^ 3 * \u2016z\u2080\u2016 := by ring\n linarith [h1, h2, hA, hB]\n have hmain : (RB + \u2016Gentire 0\u2016) / R * \u2016z\u2080\u2016 \u2264 \u03b5 := by\n have hQ4pos : (0 : \u211d) < Q ^ 4 := pow_pos hQpos 4\n have h1 : (RB + \u2016Gentire 0\u2016) / R * \u2016z\u2080\u2016 = (RB + \u2016Gentire 0\u2016) * \u2016z\u2080\u2016 / Q ^ 4 := by\n rw [hR4]\n ring\n rw [h1, div_le_iff\u2080 hQ4pos]\n exact hsum\n -- assemble\n have hdz0 : dist z\u2080 (0 : \u2102) = \u2016z\u2080\u2016 := by rw [dist_eq_norm, sub_zero]\n calc dist (Gentire z\u2080) (Gentire 0)\n \u2264 (RB + \u2016Gentire 0\u2016) / R * dist z\u2080 0 := hschwarz\n _ = (RB + \u2016Gentire 0\u2016) / R * \u2016z\u2080\u2016 := by rw [hdz0]\n _ \u2264 \u03b5 := hmain\n -- dist < every \u03b5 \u27f9 dist = 0\n rcases le_or_lt (dist (Gentire z\u2080) (Gentire 0)) 0 with h | h\n \u00b7 exact dist_eq_zero.mp (le_antisymm h dist_nonneg)\n \u00b7 have h2 := key (dist (Gentire z\u2080) (Gentire 0) / 2) (by linarith)\n linarith\n\n/-! ## 5. The capstone: the partial-fraction identity -/\n\n/-- **The ii\u2032-5e capstone** (D-068 \u00a75): under the perimeter zero count\n`ZeroCountProp`, the completed partial-fraction identity\n\u03b6\u2032/\u03b6(s) = B + \u03a3_\u03c1 m_\u03c1(1/(s\u2212\u03c1) + 1/\u03c1) \u2212 1/s \u2212 1/(s\u22121) + \u00bdlog \u03c0 \u2212 \u00bd\u03c8(s/2)\nholds at every s off the excluded set. Proof: the difference Fexpr is\nentire (5e-iv) and O((log R)\u00b2\u00b7\u0108\u2080) = o(R) on the \u03b3-gap circles\n(`Fexpr_circle_le`), so the max-modulus + Schwarz squeeze (`gentire_const`)\nforces it constant. -/\ntheorem partialFraction_identity (hZC : ZeroCountProp) :\n \u2203 B : \u2102, \u2200 s : \u2102, riemannZeta s \u2260 0 \u2192 s \u2260 0 \u2192 s \u2260 1 \u2192\n (\u2200 n : \u2115, 1 \u2264 n \u2192 s \u2260 -2 * (n : \u2102)) \u2192\n logDeriv riemannZeta s\n = B + seriesFun s - 1 / s - 1 / (s - 1) + (Real.log Real.pi : \u2102) / 2\n - Complex.digamma (s / 2) / 2 := by\n refine \u27e8Gentire 0, fun s h\u03b6 hs0 hs1 hsn => ?_\u27e9\n have hgood : \u00ac badPoint s := by\n rintro (h | h | h | \u27e8n, hn, h\u27e9)\n \u00b7 exact h\u03b6 h.1\n \u00b7 exact hs0 h\n \u00b7 exact hs1 h\n \u00b7 exact hsn n hn h\n have hG : Fexpr s = Gentire 0 := by\n rw [\u2190 gentire_eq_Fexpr hgood]\n exact gentire_const hZC s\n rw [Fexpr] at hG\n linear_combination hG\n\nend NguyenRH1\n\nend\n"
}
result 2026-08-24 06:18:15Z → 2026-08-24 06:18:15Z
{
"type": "create",
"filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSqueeze.lean",
"content": "/-\nNguyenRH1/LiSqueeze.lean \u2014 tier ii\u2032 sub-stage ii\u2032-5e-v-d (D-068 \u00a75):\nthe Schwarz squeeze \u27f9 the partial-fraction capstone.\n\n\u00a71: the \u0108\u2080 growth bound `C0hat_add_two_le` (\u0108\u2080(R+2) \u2264 5\u00b7log R).\n\u00a72: `not_badPoint_on_gapCircle` \u2014 every point of a \u03b3-gap circle is good.\n\u00a73: `gentire_circle_le` \u2014 the Fexpr circle bound transferred to Gentire.\n\u00a74: `gentire_const` \u2014 max-modulus + Schwarz on the gap-circle sequence:\n the (log R)\u00b3/R \u2192 0 squeeze forces Gentire \u2261 Gentire 0.\n\u00a75: the capstone `partialFraction_identity (hZC : ZeroCountProp)`.\n\nArchive references: D-068 \u00a75, STATE.md session-034 next-action design.\n-/\nimport Mathlib\nimport NguyenRH1.LiCircleBound\n\nopen Zeta23 Complex Filter Topology\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. The \u0108\u2080 growth bound -/\n\n/-- \u0108\u2080(R+2) \u2264 5\u00b7log R for R \u2265 16002 (so log R \u2265 9): log(R+4) \u2264 2\u00b7log R,\nlog log(R+4) \u2264 2\u00b7log R, and 2.9 \u2264 (1/3)\u00b7log R; total 2.97\u00b7log R. -/\nlemma C0hat_add_two_le {R : \u211d} (hR : 16002 \u2264 R) :\n C0hat (R + 2) \u2264 5 * Real.log R := by\n have hRpos : (0 : \u211d) < R := by linarith\n have hlogR : (9 : \u211d) \u2264 Real.log R := nine_le_log_of_16002_le hR\n have h1 : Real.log (R + 2 + 2) \u2264 2 * Real.log R := by\n have hle : R + 2 + 2 \u2264 R ^ 2 := by nlinarith [hR]\n have h2 : Real.log (R + 2 + 2) \u2264 Real.log (R ^ 2) :=\n Real.log_le_log (by linarith : (0 : \u211d) < R + 2 + 2) hle\n rwa [Real.log_pow, Nat.cast_two] at h2\n have h2 : Real.log (Real.log (R + 2 + 2)) \u2264 2 * Real.log R := by\n have hpos1 : (0 : \u211d) < Real.log (R + 2 + 2) := by\n have hle : Real.log R \u2264 Real.log (R + 2 + 2) :=\n Real.log_le_log hRpos (by linarith)\n linarith [hlogR]\n have h3 : Real.log (Real.log (R + 2 + 2)) \u2264 Real.log (2 * Real.log R) :=\n Real.log_le_log hpos1 h1\n have h4 : Real.log (2 * Real.log R) = Real.log 2 + Real.log (Real.log R) := by\n rw [Real.log_mul (by norm_num) (by linarith [hlogR] : Real.log R \u2260 0)]\n have h5 : Real.log 2 \u2264 1 := by\n have h := Real.log_le_sub_one_of_pos (by norm_num : (0 : \u211d) < 2)\n linarith\n have h6 : Real.log (Real.log R) \u2264 Real.log R := by\n have h := Real.log_le_sub_one_of_pos (by linarith [hlogR] : (0 : \u211d) < Real.log R)\n linarith\n linarith [h3, h4, h5, h6, hlogR]\n unfold C0hat\n linarith [h1, h2, hlogR]\n\n/-! ## 2. Every \u03b3-gap-circle point is good -/\n\n/-- A point on a \u03b3-gap circle is not a bad point: not a nontrivial zero\n(the circle-bound lemma), not 0 or 1 (norm too large), not \u22122n (the\n\u2124-clearance of R/2). -/\nlemma not_badPoint_on_gapCircle {k : \u2115} (hk : 4000 \u2264 k) {R : \u211d}\n (hRlo : 4 * (k : \u211d) + 5 / 2 \u2264 R)\n (hgap : \u2200 \u03c1 : \u2102, IsNontrivialZero \u03c1 \u2192\n 1 / (16 * C0hat (4 * (k : \u211d) + 9 / 2)) \u2264 |\u03c1.im - R| \u2228 1 \u2264 |\u03c1.im - R|)\n (hgapInt : \u2200 m : \u2124, 1 / 4 \u2264 |R / 2 - (m : \u211d)|)\n {s : \u2102} (hs : \u2016s\u2016 = R) : \u00ac badPoint s := by\n have hR16002 : (16002 : \u211d) \u2264 R := by\n have h1 : (4000 : \u211d) \u2264 (k : \u211d) := by exact_mod_cast hk\n linarith [hRlo]\n have hRpos : (0 : \u211d) < R := by linarith [hR16002]\n rintro (h | h | h | \u27e8n, -, h\u27e9)\n \u00b7 exact not_isNontrivialZero_on_gapCircle hk hRlo hgap hs h\n \u00b7 rw [h, norm_zero] at hs\n linarith [hRpos]\n \u00b7 rw [h, norm_one] at hs\n linarith [hR16002]\n \u00b7 have hR2 : R = 2 * (n : \u211d) := by\n rw [\u2190 hs, h, norm_mul]\n have h1 : \u2016(-2 : \u2102)\u2016 = 2 := by\n rw [show (-2 : \u2102) = ((-2 : \u211d) : \u2102) by push_cast; ring, Complex.norm_real]\n norm_num\n rw [h1, Complex.norm_natCast]\n have hcon := hgapInt (n : \u2124)\n rw [Int.cast_natCast] at hcon\n have h0 : R / 2 - (n : \u211d) = 0 := by rw [hR2]; ring\n rw [h0, abs_zero] at hcon\n linarith [hcon]\n\n/-! ## 3. The circle bound for Gentire -/\n\n/-- The Fexpr circle bound transfers to Gentire on the \u03b3-gap circles\n(every circle point is good, so Gentire = Fexpr there). -/\ntheorem gentire_circle_le {k : \u2115} (hk : 4000 \u2264 k) {R : \u211d}\n (hRlo : 4 * (k : \u211d) + 5 / 2 \u2264 R) (hRhi : R \u2264 4 * (k : \u211d) + 3)\n (hgap : \u2200 \u03c1 : \u2102, IsNontrivialZero \u03c1 \u2192\n 1 / (16 * C0hat (4 * (k : \u211d) + 9 / 2)) \u2264 |\u03c1.im - R| \u2228 1 \u2264 |\u03c1.im - R|)\n (hgapInt : \u2200 m : \u2124, 1 / 4 \u2264 |R / 2 - (m : \u211d)|)\n {s : \u2102} (hs : \u2016s\u2016 = R) :\n \u2016Gentire s\u2016 \u2264 2 * lowZeroConst + dirichletC2 +\n 400000 * A0count * C0hat (R + 2) * (Real.log R) ^ 2 := by\n have hgood : \u00ac badPoint s := not_badPoint_on_gapCircle hk hRlo hgap hgapInt hs\n rw [gentire_eq_Fexpr hgood]\n exact Fexpr_circle_le hk hRlo hRhi hgap hgapInt hs\n\n/-! ## 4. The squeeze: Gentire is constant -/\n\n/-- **The Schwarz squeeze**: under the perimeter zero count, Gentire is\nconstant. For each \u03b5 > 0 pick a \u03b3-gap circle of radius R \u2265 16002 with\nR^{1/4} \u2265 2 + (128\u00b7C\u2081 + 2\u00b7C\u2080')\u00b7\u2016z\u2080\u2016/\u03b5; max-modulus bounds Gentire on the\nball by the circle bound, Schwarz then gives\ndist (Gentire z\u2080) (Gentire 0) \u2264 (C\u2080' + 64\u00b7C\u2081\u00b7R^{3/4})\u00b7\u2016z\u2080\u2016/R \u2264 \u03b5. -/\ntheorem gentire_const (hZC : ZeroCountProp) (z\u2080 : \u2102) : Gentire z\u2080 = Gentire 0 := by\n classical\n have hA0nn : (0 : \u211d) \u2264 A0count := A0count_pos.le\n have key : \u2200 \u03b5 : \u211d, 0 < \u03b5 \u2192 dist (Gentire z\u2080) (Gentire 0) \u2264 \u03b5 := by\n intro \u03b5 h\u03b5\n -- the constants\n set C\u2080' := 2 * lowZeroConst + dirichletC2 + \u2016Gentire 0\u2016 with hC0'\n set C\u2081 := 2000000 * A0count with hC1\n have hC\u2080'nn : (0 : \u211d) \u2264 C\u2080' := by\n rw [hC0']\n linarith [lowZeroConst_nonneg, dirichletC2_nonneg, norm_nonneg (Gentire 0)]\n have hC\u2081nn : (0 : \u211d) \u2264 C\u2081 := by\n rw [hC1]\n exact mul_nonneg (by norm_num) hA0nn\n set c := 2 + (128 * C\u2081 + 2 * C\u2080') * \u2016z\u2080\u2016 / \u03b5 with hc\n have hXnn : (0 : \u211d) \u2264 (128 * C\u2081 + 2 * C\u2080') * \u2016z\u2080\u2016 / \u03b5 :=\n div_nonneg (mul_nonneg (add_nonneg (mul_nonneg (by norm_num) hC\u2081nn)\n (mul_nonneg (by norm_num) hC\u2080'nn)) (norm_nonneg _)) h\u03b5.le\n have hcz : (2 : \u211d) \u2264 c := by rw [hc]; linarith [hXnn]\n have hcnn : (0 : \u211d) \u2264 c := by linarith [hcz]\n -- the radius choice\n set M := max (c ^ 4) (\u2016z\u2080\u2016 + 1) with hM\n obtain \u27e8k, hk4000, hkM\u27e9 : \u2203 k : \u2115, 4000 \u2264 k \u2227 M \u2264 4 * (k : \u211d) := by\n refine \u27e8max 4000 \u2308M / 4\u2309\u208a, le_max_left _ _, ?_\u27e9\n have h1 : M / 4 \u2264 (\u2308M / 4\u2309\u208a : \u211d) := Nat.le_ceil _\n have h2 : (\u2308M / 4\u2309\u208a : \u211d) \u2264 ((max 4000 \u2308M / 4\u2309\u208a : \u2115) : \u211d) := by\n exact_mod_cast le_max_right _ _\n linarith [h1, h2]\n obtain \u27e8R, hRlo, hRhi, hgapInt, hgap\u27e9 :=\n exists_gapCircle_radius hZC (k := k) (by omega)\n have hR16002 : (16002 : \u211d) \u2264 R := by\n have h1 : (4000 : \u211d) \u2264 (k : \u211d) := by exact_mod_cast hk4000\n linarith [hRlo]\n have hRpos : (0 : \u211d) < R := by linarith [hR16002]\n have hlogR : (9 : \u211d) \u2264 Real.log R := nine_le_log_of_16002_le hR16002\n have hMR : M \u2264 R := by linarith [hkM, hRlo]\n -- the circle bound on the sphere, then the ball by max-modulus\n set RB := 2 * lowZeroConst + dirichletC2 +\n 400000 * A0count * C0hat (R + 2) * (Real.log R) ^ 2 with hRB\n have hsphere : \u2200 z \u2208 Metric.sphere (0 : \u2102) R, \u2016Gentire z\u2016 \u2264 RB := by\n intro z hz\n have hznorm : \u2016z\u2016 = R := by\n have h := Metric.mem_sphere.mp hz\n rwa [dist_eq_norm, sub_zero] at h\n exact gentire_circle_le hk4000 hRlo hRhi hgap hgapInt hznorm\n have hGan : AnalyticOn \u2102 Gentire (Metric.closedBall 0 R) :=\n AnalyticOnNhd.analyticOn (fun s _ => gentire_analyticAt_and_eq.1 s)\n have hball : \u2200 z \u2208 Metric.closedBall (0 : \u2102) R, \u2016Gentire z\u2016 \u2264 RB :=\n fun z hz => AnalyticOn.norm_le_of_norm_le_on_sphere le_rfl hGan hsphere hz\n -- the Schwarz inputs\n have hmaps : Set.MapsTo Gentire (Metric.ball 0 R)\n (Metric.closedBall (Gentire 0) (RB + \u2016Gentire 0\u2016)) := by\n intro z hz\n have hzball : z \u2208 Metric.closedBall (0 : \u2102) R := by\n rw [Metric.mem_ball] at hz\n rw [Metric.mem_closedBall]\n exact hz.le\n have h1 := hball z hzball\n rw [Metric.mem_closedBall, dist_eq_norm]\n calc \u2016Gentire z - Gentire 0\u2016 \u2264 \u2016Gentire z\u2016 + \u2016Gentire 0\u2016 := norm_sub_le _ _\n _ \u2264 RB + \u2016Gentire 0\u2016 := by linarith [h1]\n have hdiff : DifferentiableOn \u2102 Gentire (Metric.ball 0 R) :=\n fun z _ => (gentire_analyticAt_and_eq.1 z).differentiableAt.differentiableWithinAt\n have hz0mem : z\u2080 \u2208 Metric.ball (0 : \u2102) R := by\n rw [Metric.mem_ball, dist_eq_norm, sub_zero]\n have h1 : \u2016z\u2080\u2016 + 1 \u2264 M := le_max_right _ _\n linarith [hMR]\n have hschwarz := Complex.dist_le_div_mul_dist_of_mapsTo_ball hdiff hmaps hz0mem\n -- the growth estimates: RB + \u2016Gentire 0\u2016 \u2264 C\u2080' + 64\u00b7C\u2081\u00b7Q\u00b3, R = Q\u2074\n set Q := R ^ ((4 : \u211d)\u207b\u00b9) with hQ\n have hQnn : (0 : \u211d) \u2264 Q := Real.rpow_nonneg hRpos.le _\n have hQpos : (0 : \u211d) < Q := Real.rpow_pos_of_pos hRpos _\n have hQc : c \u2264 Q := by\n have hc4 : c ^ 4 \u2264 R := by\n have h : c ^ 4 \u2264 M := le_max_left _ _\n linarith [hMR]\n have h1 : c = (c ^ 4) ^ ((4 : \u211d)\u207b\u00b9) := by\n have h := (Real.pow_rpow_inv_natCast hcnn (show (4 : \u2115) \u2260 0 by norm_num)).symm\n push_cast at h\n exact h\n have h2 : (c ^ 4) ^ ((4 : \u211d)\u207b\u00b9) \u2264 Q :=\n Real.rpow_le_rpow (pow_nonneg (by linarith [hcz] : (0 : \u211d) \u2264 c) 4) hc4\n (by positivity : (0 : \u211d) \u2264 (4 : \u211d)\u207b\u00b9)\n rw [h1]\n exact h2\n have hL : Real.log R \u2264 4 * Q := by\n have h := Real.log_le_rpow_div hRpos.le (show (0 : \u211d) < (4 : \u211d)\u207b\u00b9 by positivity)\n have h2 : R ^ ((4 : \u211d)\u207b\u00b9) / (4 : \u211d)\u207b\u00b9 = 4 * (R ^ ((4 : \u211d)\u207b\u00b9)) := by\n rw [div_eq_mul_inv, inv_inv]\n ring\n rwa [h2] at h\n have hL3 : (Real.log R) ^ 3 \u2264 64 * Q ^ 3 := by\n have h1 : (Real.log R) ^ 3 \u2264 (4 * Q) ^ 3 :=\n pow_le_pow_left\u2080 (by linarith [hlogR]) hL 3\n have h2 : (4 * Q) ^ 3 = 64 * Q ^ 3 := by ring\n rwa [h2] at h1\n have hR4 : R = Q ^ 4 := by\n have h := Real.rpow_inv_natCast_pow hRpos.le (show (4 : \u2115) \u2260 0 by norm_num)\n push_cast at h\n rw [\u2190 hQ] at h\n exact h.symm\n have h\u01085 : C0hat (R + 2) \u2264 5 * Real.log R := C0hat_add_two_le hR16002\n have hbig : 400000 * A0count * C0hat (R + 2) * (Real.log R) ^ 2\n \u2264 64 * C\u2081 * Q ^ 3 := by\n have hlogRnn : (0 : \u211d) \u2264 Real.log R := by linarith [hlogR]\n have h1 : 400000 * A0count * C0hat (R + 2) * (Real.log R) ^ 2\n \u2264 400000 * A0count * (5 * Real.log R) * (Real.log R) ^ 2 := by\n apply mul_le_mul_of_nonneg_right _ (pow_nonneg hlogRnn 2)\n exact mul_le_mul_of_nonneg_left h\u01085\n (mul_nonneg (by norm_num : (0 : \u211d) \u2264 400000) hA0nn)\n have h2 : 400000 * A0count * (5 * Real.log R) * (Real.log R) ^ 2\n = C\u2081 * (Real.log R) ^ 3 := by\n rw [hC1]\n ring\n have h3 : C\u2081 * (Real.log R) ^ 3 \u2264 64 * C\u2081 * Q ^ 3 := by\n have h := mul_le_mul_of_nonneg_left hL3 hC\u2081nn\n have h' : C\u2081 * (64 * Q ^ 3) = 64 * C\u2081 * Q ^ 3 := by ring\n rwa [h'] at h\n linarith [h1, h2, h3]\n have hRBle : RB + \u2016Gentire 0\u2016 \u2264 C\u2080' + 64 * C\u2081 * Q ^ 3 := by\n rw [hRB, hC0']\n linarith [hbig]\n -- the real squeeze: (RB + \u2016Gentire 0\u2016)/R\u00b7\u2016z\u2080\u2016 \u2264 \u03b5\n have hc1 : 128 * C\u2081 * \u2016z\u2080\u2016 \u2264 \u03b5 * Q := by\n have h1 : (128 * C\u2081 + 2 * C\u2080') * \u2016z\u2080\u2016 / \u03b5 \u2264 c := by rw [hc]; linarith\n have h2 : (128 * C\u2081) * \u2016z\u2080\u2016 \u2264 (128 * C\u2081 + 2 * C\u2080') * \u2016z\u2080\u2016 := by\n apply mul_le_mul_of_nonneg_right _ (norm_nonneg _)\n linarith [hC\u2080'nn]\n have h3 : (128 * C\u2081) * \u2016z\u2080\u2016 / \u03b5 \u2264 c :=\n (div_le_div_of_nonneg_right h2 h\u03b5.le).trans h1\n calc (128 * C\u2081) * \u2016z\u2080\u2016 = (128 * C\u2081) * \u2016z\u2080\u2016 / \u03b5 * \u03b5 := by\n rw [div_mul_cancel\u2080 _ h\u03b5.ne']\n _ \u2264 c * \u03b5 := mul_le_mul_of_nonneg_right h3 h\u03b5.le\n _ \u2264 Q * \u03b5 := mul_le_mul_of_nonneg_right hQc h\u03b5.le\n _ = \u03b5 * Q := by ring\n have hA : 64 * C\u2081 * Q ^ 3 * \u2016z\u2080\u2016 \u2264 (\u03b5 / 2) * Q ^ 4 := by\n have h1 : (64 * C\u2081 * \u2016z\u2080\u2016) * Q ^ 3 \u2264 ((\u03b5 / 2) * Q) * Q ^ 3 := by\n apply mul_le_mul_of_nonneg_right _ (pow_nonneg hQnn 3)\n have h64 : (64 : \u211d) * C\u2081 * \u2016z\u2080\u2016 = (128 * C\u2081 * \u2016z\u2080\u2016) / 2 := by ring\n have hhalf : (\u03b5 / 2) * Q = (\u03b5 * Q) / 2 := by ring\n rw [h64, hhalf]\n linarith [hc1]\n have hL' : (64 * C\u2081 * \u2016z\u2080\u2016) * Q ^ 3 = 64 * C\u2081 * Q ^ 3 * \u2016z\u2080\u2016 := by ring\n have hR' : ((\u03b5 / 2) * Q) * Q ^ 3 = (\u03b5 / 2) * Q ^ 4 := by ring\n rwa [hL', hR'] at h1\n have hB : C\u2080' * \u2016z\u2080\u2016 \u2264 (\u03b5 / 2) * Q ^ 4 := by\n have h1 : (2 * C\u2080') * \u2016z\u2080\u2016 \u2264 \u03b5 * Q := by\n have h2 : (2 * C\u2080') * \u2016z\u2080\u2016 \u2264 (128 * C\u2081 + 2 * C\u2080') * \u2016z\u2080\u2016 := by\n apply mul_le_mul_of_nonneg_right _ (norm_nonneg _)\n linarith [hC\u2081nn]\n have h3 : (128 * C\u2081 + 2 * C\u2080') * \u2016z\u2080\u2016 / \u03b5 \u2264 c := by rw [hc]; linarith\n have h4 : (2 * C\u2080') * \u2016z\u2080\u2016 / \u03b5 \u2264 c :=\n (div_le_div_of_nonneg_right h2 h\u03b5.le).trans h3\n calc (2 * C\u2080') * \u2016z\u2080\u2016 = (2 * C\u2080') * \u2016z\u2080\u2016 / \u03b5 * \u03b5 := by\n rw [div_mul_cancel\u2080 _ h\u03b5.ne']\n _ \u2264 c * \u03b5 := mul_le_mul_of_nonneg_right h4 h\u03b5.le\n _ \u2264 Q * \u03b5 := mul_le_mul_of_nonneg_right hQc h\u03b5.le\n _ = \u03b5 * Q := by ring\n have hQ2 : (2 : \u211d) \u2264 Q := by linarith [hQc, hcz]\n have hQ3 : (2 : \u211d) \u2264 Q ^ 3 := by\n have h := pow_le_pow_left\u2080 (by norm_num : (0 : \u211d) \u2264 2) hQ2 3\n norm_num at h\n linarith [h]\n have h2 : \u03b5 * Q \u2264 (\u03b5 / 2) * Q ^ 4 := by\n have h3 : (\u03b5 / 2) * Q ^ 4 = ((\u03b5 / 2) * Q) * Q ^ 3 := by ring\n rw [h3]\n have h6 : (\u03b5 / 2) * Q * 2 \u2264 (\u03b5 / 2) * Q * Q ^ 3 :=\n mul_le_mul_of_nonneg_left hQ3 (by positivity)\n have h5 : \u03b5 * Q = (\u03b5 / 2) * Q * 2 := by ring\n rw [h5]\n exact h6\n have h7 : C\u2080' * \u2016z\u2080\u2016 \u2264 2 * C\u2080' * \u2016z\u2080\u2016 := by\n have h : (0 : \u211d) \u2264 C\u2080' * \u2016z\u2080\u2016 := mul_nonneg hC\u2080'nn (norm_nonneg _)\n linarith [h]\n linarith [h7, h1, h2]\n have hsum : (RB + \u2016Gentire 0\u2016) * \u2016z\u2080\u2016 \u2264 \u03b5 * Q ^ 4 := by\n have h1 : (RB + \u2016Gentire 0\u2016) * \u2016z\u2080\u2016 \u2264 (C\u2080' + 64 * C\u2081 * Q ^ 3) * \u2016z\u2080\u2016 :=\n mul_le_mul_of_nonneg_right hRBle (norm_nonneg _)\n have h2 : (C\u2080' + 64 * C\u2081 * Q ^ 3) * \u2016z\u2080\u2016\n = C\u2080' * \u2016z\u2080\u2016 + 64 * C\u2081 * Q ^ 3 * \u2016z\u2080\u2016 := by ring\n linarith [h1, h2, hA, hB]\n have hmain : (RB + \u2016Gentire 0\u2016) / R * \u2016z\u2080\u2016 \u2264 \u03b5 := by\n have hQ4pos : (0 : \u211d) < Q ^ 4 := pow_pos hQpos 4\n have h1 : (RB + \u2016Gentire 0\u2016) / R * \u2016z\u2080\u2016 = (RB + \u2016Gentire 0\u2016) * \u2016z\u2080\u2016 / Q ^ 4 := by\n rw [hR4]\n ring\n rw [h1, div_le_iff\u2080 hQ4pos]\n exact hsum\n -- assemble\n have hdz0 : dist z\u2080 (0 : \u2102) = \u2016z\u2080\u2016 := by rw [dist_eq_norm, sub_zero]\n calc dist (Gentire z\u2080) (Gentire 0)\n \u2264 (RB + \u2016Gentire 0\u2016) / R * dist z\u2080 0 := hschwarz\n _ = (RB + \u2016Gentire 0\u2016) / R * \u2016z\u2080\u2016 := by rw [hdz0]\n _ \u2264 \u03b5 := hmain\n -- dist < every \u03b5 \u27f9 dist = 0\n rcases le_or_lt (dist (Gentire z\u2080) (Gentire 0)) 0 with h | h\n \u00b7 exact dist_eq_zero.mp (le_antisymm h dist_nonneg)\n \u00b7 have h2 := key (dist (Gentire z\u2080) (Gentire 0) / 2) (by linarith)\n linarith\n\n/-! ## 5. The capstone: the partial-fraction identity -/\n\n/-- **The ii\u2032-5e capstone** (D-068 \u00a75): under the perimeter zero count\n`ZeroCountProp`, the completed partial-fraction identity\n\u03b6\u2032/\u03b6(s) = B + \u03a3_\u03c1 m_\u03c1(1/(s\u2212\u03c1) + 1/\u03c1) \u2212 1/s \u2212 1/(s\u22121) + \u00bdlog \u03c0 \u2212 \u00bd\u03c8(s/2)\nholds at every s off the excluded set. Proof: the difference Fexpr is\nentire (5e-iv) and O((log R)\u00b2\u00b7\u0108\u2080) = o(R) on the \u03b3-gap circles\n(`Fexpr_circle_le`), so the max-modulus + Schwarz squeeze (`gentire_const`)\nforces it constant. -/\ntheorem partialFraction_identity (hZC : ZeroCountProp) :\n \u2203 B : \u2102, \u2200 s : \u2102, riemannZeta s \u2260 0 \u2192 s \u2260 0 \u2192 s \u2260 1 \u2192\n (\u2200 n : \u2115, 1 \u2264 n \u2192 s \u2260 -2 * (n : \u2102)) \u2192\n logDeriv riemannZeta s\n = B + seriesFun s - 1 / s - 1 / (s - 1) + (Real.log Real.pi : \u2102) / 2\n - Complex.digamma (s / 2) / 2 := by\n refine \u27e8Gentire 0, fun s h\u03b6 hs0 hs1 hsn => ?_\u27e9\n have hgood : \u00ac badPoint s := by\n rintro (h | h | h | \u27e8n, hn, h\u27e9)\n \u00b7 exact h\u03b6 h.1\n \u00b7 exact hs0 h\n \u00b7 exact hs1 h\n \u00b7 exact hsn n hn h\n have hG : Fexpr s = Gentire 0 := by\n rw [\u2190 gentire_eq_Fexpr hgood]\n exact gentire_const hZC s\n rw [Fexpr] at hG\n linear_combination hG\n\nend NguyenRH1\n\nend\n",
"structuredPatch": [],
"originalFile": null
}
raw content_json (database row)
[{"type":"thinking","thinking":"- `div_le_div_of_nonneg_right (hab : a ≤ b) (hc : 0 ≤ c) : a / c ≤ b / c` ✓\n- `div_mul_cancel₀ _ (h : b ≠ 0) : a / b * b = a` ✓ (usage in LiGapCircles confirms arg order: div_mul_cancel₀ _ hne).\n- Nat.le_ceil: used in project? LiFEntire line 84: `Nat.le_ceil _` ✓ seen there (`Nat.le_ceil _ : ‖w‖ ≤ M`). Signature `Nat.le_ceil (a : ℝ) : a ≤ ↑⌈a⌉₊` ✓.\n\nNow write the file. Let me assemble the complete LiSqueeze.lean carefully.\n\nOne remaining check — `Metric.mem_sphere.mp hz` gives `dist z 0 = R`? Metric.mem_sphere : z ∈ sphere x r ↔ dist z x = r ✓.\n\n`dist_eq_norm : dist x y = ‖x - y‖` — for ℂ (SeminormedAddCommGroup) ✓ name is `dist_eq_norm` ✓.\n\nFor hz0mem the rewrite: rw [Metric.mem_ball, dist_eq_norm, sub_zero] — Metric.mem_ball : z ∈ ball x r ↔ dist z x < r; goal becomes dist z₀ 0 < R → ‖z₀ − 0‖ < R → ‖z₀‖ < R ✓.\n\nNow, in hsphere: `intro z hz` — goal `z ∈ Metric.sphere (0:ℂ) R → ‖Gentire z‖ ≤ RB`? hsphere's statement: ∀ z ∈ Metric.sphere (0:ℂ) R, ... — intro z hz ✓.\n\nAfter set RB, the hsphere statement I write with RB; the proof's final exact gentire_circle_le ... produces the unfolded form — defeq ✓.\n\nLet me also decide: does `set RB` cause issues with hznorm etc.? No.\n\nOne more potential issue: in §4 I reference `Fexpr_circle_le` indirectly via `gentire_circle_le` — fine.\n\n`AnalyticOn.norm_le_of_norm_le_on_sphere le_rfl hGan hsphere hz` — signature: (hyp_r : r ≤ R) (analytic : AnalyticOn ℂ f (closedBall 0 R)) (cond : ∀ z ∈ sphere 0 r, ‖f z‖ ≤ C) (wInS : w ∈ closedBall 0 r) : ‖f w‖ ≤ C. With r := R (our R), R := R: hyp_r : R ≤ R = le_rfl ✓. Implicit {C r R f w} — inferred ✓. BUT: name clash — our `R` vs lemma's `R`; fine.\n\nWait — the lemma's `f : ℂ → ℂ`, our Gentire ✓. Its `AnalyticOn ℂ f (Metric.closedBall 0 R)` — in the lemma statement it's written `Metric.closedBall 0 R`? From the source: `(analytic : AnalyticOn ℂ f (Metric.closedBall 0 R))` — the source shows `AnalyticOn ℂ f (Metric.closedBall 0 R)`? Looking at the code: `lemma AnalyticOn.norm_le_of_norm_le_on_sphere {C r R : ℝ} {f : ℂ → ℂ} {w : ℂ} (hyp_r : r ≤ R) (analytic : AnalyticOn ℂ f (Metric.closedBall 0 R)) (cond : ∀ z ∈ Metric.sphere 0 r, ‖f z‖ ≤ C) (wInS : w ∈ Metric.closedBall 0 r)`. Hmm the actual file showed `Metric.closedBall 0 R` — from my read: line 33-40 shows `(analytic : AnalyticOn ℂ f (Metric.closedBall 0 R))`, `(cond : ∀ z ∈ Metric.sphere 0 r, ‖f z‖ ≤ C)`, `(wInS : w ∈ Metric.closedBall 0 r)`. ✓ (it showed `Metric.closedBall` — well, the read showed `Metric.closedBall 0 R`? It showed \"AnalyticOn ℂ f (Metric.closedBall 0 R)\" — yes with Metric prefix.)\n\nhGan : AnalyticOn ℂ Gentire (Metric.closedBall (0:ℂ) R) ✓ matches.\n\nThe `(0:ℂ)` vs `0` — fine.\n\nNow assemble the whole §4 proof. One concern: the `key` block is long; Lean elaboration of a big proof is fine but errors need iteration. I'll write it, then compile with `lake env lean NguyenRH1/LiSqueeze.lean` and iterate.\n\nAlso the capstone §5.\n\nAnd finally: root-import LiCircleBound + LiSqueeze in NguyenRH1.lean + update the header comment.\n\nLet me also double-check `Real.log_le_log` signature: from usage `Real.log_le_log (by ... : (0:ℝ) < 2 + R/2) (...)` — hmm line 3894 was `apply Real.log_le_log (by linarith [hRpos] : (0 : ℝ) < 2 + R / 2)` — then remaining goal `2 + R/2 ≤ R`. So Real.log_le_log (hx : 0 < x) : x ≤ y → log x ≤ log y ✓.\n\n`Real.le_log_iff_exp_le` used in two_le_C0hat ✓ not needed here.\n\nWrite the file now. Also — important detail: in §4, after `obtain ⟨R, hRlo, hRhi, hgapInt, hgap⟩ := exists_gapCircle_radius hZC (k := k) (by omega)`, the conjunction order: (4k+5/2 ≤ R) ∧ (R ≤ 4k+3) ∧ (∀ m:ℤ, ...) ∧ (∀ ρ, ...) ✓ per the signature I read.\n\nNote the exists_gapCircle_radius hgap form: `1 / (16 * C0hat (4 * (k : ℝ) + 9 / 2))) ≤ |ρ.im - R| ∨ 1 ≤ |ρ.im - R|` — wait the exact statement from LiGapCircles:47-51: `(∀ ρ : ℂ, IsNontrivialZero ρ → (1 / (16 * C0hat (4 * (k : ℝ) + 9 / 2))) ≤ |ρ.im - R| ∨ 1 ≤ |ρ.im - R|)` ✓ matches Fexpr_circle_le's hgap form (modulo extra parens — same term).\n\nLet me now write the file.","signature":""},{"type":"text","text":"All names verified. Writing LiSqueeze.lean now."},{"type":"tool_use","id":"Write_33","name":"Write","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSqueeze.lean","content":"/-\nNguyenRH1/LiSqueeze.lean — tier ii′ sub-stage ii′-5e-v-d (D-068 §5):\nthe Schwarz squeeze ⟹ the partial-fraction capstone.\n\n§1: the Ĉ₀ growth bound `C0hat_add_two_le` (Ĉ₀(R+2) ≤ 5·log R).\n§2: `not_badPoint_on_gapCircle` — every point of a γ-gap circle is good.\n§3: `gentire_circle_le` — the Fexpr circle bound transferred to Gentire.\n§4: `gentire_const` — max-modulus + Schwarz on the gap-circle sequence:\n the (log R)³/R → 0 squeeze forces Gentire ≡ Gentire 0.\n§5: the capstone `partialFraction_identity (hZC : ZeroCountProp)`.\n\nArchive references: D-068 §5, STATE.md session-034 next-action design.\n-/\nimport Mathlib\nimport NguyenRH1.LiCircleBound\n\nopen Zeta23 Complex Filter Topology\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. The Ĉ₀ growth bound -/\n\n/-- Ĉ₀(R+2) ≤ 5·log R for R ≥ 16002 (so log R ≥ 9): log(R+4) ≤ 2·log R,\nlog log(R+4) ≤ 2·log R, and 2.9 ≤ (1/3)·log R; total 2.97·log R. -/\nlemma C0hat_add_two_le {R : ℝ} (hR : 16002 ≤ R) :\n C0hat (R + 2) ≤ 5 * Real.log R := by\n have hRpos : (0 : ℝ) < R := by linarith\n have hlogR : (9 : ℝ) ≤ Real.log R := nine_le_log_of_16002_le hR\n have h1 : Real.log (R + 2 + 2) ≤ 2 * Real.log R := by\n have hle : R + 2 + 2 ≤ R ^ 2 := by nlinarith [hR]\n have h2 : Real.log (R + 2 + 2) ≤ Real.log (R ^ 2) :=\n Real.log_le_log (by linarith : (0 : ℝ) < R + 2 + 2) hle\n rwa [Real.log_pow, Nat.cast_two] at h2\n have h2 : Real.log (Real.log (R + 2 + 2)) ≤ 2 * Real.log R := by\n have hpos1 : (0 : ℝ) < Real.log (R + 2 + 2) := by\n have hle : Real.log R ≤ Real.log (R + 2 + 2) :=\n Real.log_le_log hRpos (by linarith)\n linarith [hlogR]\n have h3 : Real.log (Real.log (R + 2 + 2)) ≤ Real.log (2 * Real.log R) :=\n Real.log_le_log hpos1 h1\n have h4 : Real.log (2 * Real.log R) = Real.log 2 + Real.log (Real.log R) := by\n rw [Real.log_mul (by norm_num) (by linarith [hlogR] : Real.log R ≠ 0)]\n have h5 : Real.log 2 ≤ 1 := by\n have h := Real.log_le_sub_one_of_pos (by norm_num : (0 : ℝ) < 2)\n linarith\n have h6 : Real.log (Real.log R) ≤ Real.log R := by\n have h := Real.log_le_sub_one_of_pos (by linarith [hlogR] : (0 : ℝ) < Real.log R)\n linarith\n linarith [h3, h4, h5, h6, hlogR]\n unfold C0hat\n linarith [h1, h2, hlogR]\n\n/-! ## 2. Every γ-gap-circle point is good -/\n\n/-- A point on a γ-gap circle is not a bad point: not a nontrivial zero\n(the circle-bound lemma), not 0 or 1 (norm too large), not −2n (the\nℤ-clearance of R/2). -/\nlemma not_badPoint_on_gapCircle {k : ℕ} (hk : 4000 ≤ k) {R : ℝ}\n (hRlo : 4 * (k : ℝ) + 5 / 2 ≤ R)\n (hgap : ∀ ρ : ℂ, IsNontrivialZero ρ →\n 1 / (16 * C0hat (4 * (k : ℝ) + 9 / 2)) ≤ |ρ.im - R| ∨ 1 ≤ |ρ.im - R|)\n (hgapInt : ∀ m : ℤ, 1 / 4 ≤ |R / 2 - (m : ℝ)|)\n {s : ℂ} (hs : ‖s‖ = R) : ¬ badPoint s := by\n have hR16002 : (16002 : ℝ) ≤ R := by\n have h1 : (4000 : ℝ) ≤ (k : ℝ) := by exact_mod_cast hk\n linarith [hRlo]\n have hRpos : (0 : ℝ) < R := by linarith [hR16002]\n rintro (h | h | h | ⟨n, -, h⟩)\n · exact not_isNontrivialZero_on_gapCircle hk hRlo hgap hs h\n · rw [h, norm_zero] at hs\n linarith [hRpos]\n · rw [h, norm_one] at hs\n linarith [hR16002]\n · have hR2 : R = 2 * (n : ℝ) := by\n rw [← hs, h, norm_mul]\n have h1 : ‖(-2 : ℂ)‖ = 2 := by\n rw [show (-2 : ℂ) = ((-2 : ℝ) : ℂ) by push_cast; ring, Complex.norm_real]\n norm_num\n rw [h1, Complex.norm_natCast]\n have hcon := hgapInt (n : ℤ)\n rw [Int.cast_natCast] at hcon\n have h0 : R / 2 - (n : ℝ) = 0 := by rw [hR2]; ring\n rw [h0, abs_zero] at hcon\n linarith [hcon]\n\n/-! ## 3. The circle bound for Gentire -/\n\n/-- The Fexpr circle bound transfers to Gentire on the γ-gap circles\n(every circle point is good, so Gentire = Fexpr there). -/\ntheorem gentire_circle_le {k : ℕ} (hk : 4000 ≤ k) {R : ℝ}\n (hRlo : 4 * (k : ℝ) + 5 / 2 ≤ R) (hRhi : R ≤ 4 * (k : ℝ) + 3)\n (hgap : ∀ ρ : ℂ, IsNontrivialZero ρ →\n 1 / (16 * C0hat (4 * (k : ℝ) + 9 / 2)) ≤ |ρ.im - R| ∨ 1 ≤ |ρ.im - R|)\n (hgapInt : ∀ m : ℤ, 1 / 4 ≤ |R / 2 - (m : ℝ)|)\n {s : ℂ} (hs : ‖s‖ = R) :\n ‖Gentire s‖ ≤ 2 * lowZeroConst + dirichletC2 +\n 400000 * A0count * C0hat (R + 2) * (Real.log R) ^ 2 := by\n have hgood : ¬ badPoint s := not_badPoint_on_gapCircle hk hRlo hgap hgapInt hs\n rw [gentire_eq_Fexpr hgood]\n exact Fexpr_circle_le hk hRlo hRhi hgap hgapInt hs\n\n/-! ## 4. The squeeze: Gentire is constant -/\n\n/-- **The Schwarz squeeze**: under the perimeter zero count, Gentire is\nconstant. For each ε > 0 pick a γ-gap circle of radius R ≥ 16002 with\nR^{1/4} ≥ 2 + (128·C₁ + 2·C₀')·‖z₀‖/ε; max-modulus bounds Gentire on the\nball by the circle bound, Schwarz then gives\ndist (Gentire z₀) (Gentire 0) ≤ (C₀' + 64·C₁·R^{3/4})·‖z₀‖/R ≤ ε. -/\ntheorem gentire_const (hZC : ZeroCountProp) (z₀ : ℂ) : Gentire z₀ = Gentire 0 := by\n classical\n have hA0nn : (0 : ℝ) ≤ A0count := A0count_pos.le\n have key : ∀ ε : ℝ, 0 < ε → dist (Gentire z₀) (Gentire 0) ≤ ε := by\n intro ε hε\n -- the constants\n set C₀' := 2 * lowZeroConst + dirichletC2 + ‖Gentire 0‖ with hC0'\n set C₁ := 2000000 * A0count with hC1\n have hC₀'nn : (0 : ℝ) ≤ C₀' := by\n rw [hC0']\n linarith [lowZeroConst_nonneg, dirichletC2_nonneg, norm_nonneg (Gentire 0)]\n have hC₁nn : (0 : ℝ) ≤ C₁ := by\n rw [hC1]\n exact mul_nonneg (by norm_num) hA0nn\n set c := 2 + (128 * C₁ + 2 * C₀') * ‖z₀‖ / ε with hc\n have hXnn : (0 : ℝ) ≤ (128 * C₁ + 2 * C₀') * ‖z₀‖ / ε :=\n div_nonneg (mul_nonneg (add_nonneg (mul_nonneg (by norm_num) hC₁nn)\n (mul_nonneg (by norm_num) hC₀'nn)) (norm_nonneg _)) hε.le\n have hcz : (2 : ℝ) ≤ c := by rw [hc]; linarith [hXnn]\n have hcnn : (0 : ℝ) ≤ c := by linarith [hcz]\n -- the radius choice\n set M := max (c ^ 4) (‖z₀‖ + 1) with hM\n obtain ⟨k, hk4000, hkM⟩ : ∃ k : ℕ, 4000 ≤ k ∧ M ≤ 4 * (k : ℝ) := by\n refine ⟨max 4000 ⌈M / 4⌉₊, le_max_left _ _, ?_⟩\n have h1 : M / 4 ≤ (⌈M / 4⌉₊ : ℝ) := Nat.le_ceil _\n have h2 : (⌈M / 4⌉₊ : ℝ) ≤ ((max 4000 ⌈M / 4⌉₊ : ℕ) : ℝ) := by\n exact_mod_cast le_max_right _ _\n linarith [h1, h2]\n obtain ⟨R, hRlo, hRhi, hgapInt, hgap⟩ :=\n exists_gapCircle_radius hZC (k := k) (by omega)\n have hR16002 : (16002 : ℝ) ≤ R := by\n have h1 : (4000 : ℝ) ≤ (k : ℝ) := by exact_mod_cast hk4000\n linarith [hRlo]\n have hRpos : (0 : ℝ) < R := by linarith [hR16002]\n have hlogR : (9 : ℝ) ≤ Real.log R := nine_le_log_of_16002_le hR16002\n have hMR : M ≤ R := by linarith [hkM, hRlo]\n -- the circle bound on the sphere, then the ball by max-modulus\n set RB := 2 * lowZeroConst + dirichletC2 +\n 400000 * A0count * C0hat (R + 2) * (Real.log R) ^ 2 with hRB\n have hsphere : ∀ z ∈ Metric.sphere (0 : ℂ) R, ‖Gentire z‖ ≤ RB := by\n intro z hz\n have hznorm : ‖z‖ = R := by\n have h := Metric.mem_sphere.mp hz\n rwa [dist_eq_norm, sub_zero] at h\n exact gentire_circle_le hk4000 hRlo hRhi hgap hgapInt hznorm\n have hGan : AnalyticOn ℂ Gentire (Metric.closedBall 0 R) :=\n AnalyticOnNhd.analyticOn (fun s _ => gentire_analyticAt_and_eq.1 s)\n have hball : ∀ z ∈ Metric.closedBall (0 : ℂ) R, ‖Gentire z‖ ≤ RB :=\n fun z hz => AnalyticOn.norm_le_of_norm_le_on_sphere le_rfl hGan hsphere hz\n -- the Schwarz inputs\n have hmaps : Set.MapsTo Gentire (Metric.ball 0 R)\n (Metric.closedBall (Gentire 0) (RB + ‖Gentire 0‖)) := by\n intro z hz\n have hzball : z ∈ Metric.closedBall (0 : ℂ) R := by\n rw [Metric.mem_ball] at hz\n rw [Metric.mem_closedBall]\n exact hz.le\n have h1 := hball z hzball\n rw [Metric.mem_closedBall, dist_eq_norm]\n calc ‖Gentire z - Gentire 0‖ ≤ ‖Gentire z‖ + ‖Gentire 0‖ := norm_sub_le _ _\n _ ≤ RB + ‖Gentire 0‖ := by linarith [h1]\n have hdiff : DifferentiableOn ℂ Gentire (Metric.ball 0 R) :=\n fun z _ => (gentire_analyticAt_and_eq.1 z).differentiableAt.differentiableWithinAt\n have hz0mem : z₀ ∈ Metric.ball (0 : ℂ) R := by\n rw [Metric.mem_ball, dist_eq_norm, sub_zero]\n have h1 : ‖z₀‖ + 1 ≤ M := le_max_right _ _\n linarith [hMR]\n have hschwarz := Complex.dist_le_div_mul_dist_of_mapsTo_ball hdiff hmaps hz0mem\n -- the growth estimates: RB + ‖Gentire 0‖ ≤ C₀' + 64·C₁·Q³, R = Q⁴\n set Q := R ^ ((4 : ℝ)⁻¹) with hQ\n have hQnn : (0 : ℝ) ≤ Q := Real.rpow_nonneg hRpos.le _\n have hQpos : (0 : ℝ) < Q := Real.rpow_pos_of_pos hRpos _\n have hQc : c ≤ Q := by\n have hc4 : c ^ 4 ≤ R := by\n have h : c ^ 4 ≤ M := le_max_left _ _\n linarith [hMR]\n have h1 : c = (c ^ 4) ^ ((4 : ℝ)⁻¹) := by\n have h := (Real.pow_rpow_inv_natCast hcnn (show (4 : ℕ) ≠ 0 by norm_num)).symm\n push_cast at h\n exact h\n have h2 : (c ^ 4) ^ ((4 : ℝ)⁻¹) ≤ Q :=\n Real.rpow_le_rpow (pow_nonneg (by linarith [hcz] : (0 : ℝ) ≤ c) 4) hc4\n (by positivity : (0 : ℝ) ≤ (4 : ℝ)⁻¹)\n rw [h1]\n exact h2\n have hL : Real.log R ≤ 4 * Q := by\n have h := Real.log_le_rpow_div hRpos.le (show (0 : ℝ) < (4 : ℝ)⁻¹ by positivity)\n have h2 : R ^ ((4 : ℝ)⁻¹) / (4 : ℝ)⁻¹ = 4 * (R ^ ((4 : ℝ)⁻¹)) := by\n rw [div_eq_mul_inv, inv_inv]\n ring\n rwa [h2] at h\n have hL3 : (Real.log R) ^ 3 ≤ 64 * Q ^ 3 := by\n have h1 : (Real.log R) ^ 3 ≤ (4 * Q) ^ 3 :=\n pow_le_pow_left₀ (by linarith [hlogR]) hL 3\n have h2 : (4 * Q) ^ 3 = 64 * Q ^ 3 := by ring\n rwa [h2] at h1\n have hR4 : R = Q ^ 4 := by\n have h := Real.rpow_inv_natCast_pow hRpos.le (show (4 : ℕ) ≠ 0 by norm_num)\n push_cast at h\n rw [← hQ] at h\n exact h.symm\n have hĈ5 : C0hat (R + 2) ≤ 5 * Real.log R := C0hat_add_two_le hR16002\n have hbig : 400000 * A0count * C0hat (R + 2) * (Real.log R) ^ 2\n ≤ 64 * C₁ * Q ^ 3 := by\n have hlogRnn : (0 : ℝ) ≤ Real.log R := by linarith [hlogR]\n have h1 : 400000 * A0count * C0hat (R + 2) * (Real.log R) ^ 2\n ≤ 400000 * A0count * (5 * Real.log R) * (Real.log R) ^ 2 := by\n apply mul_le_mul_of_nonneg_right _ (pow_nonneg hlogRnn 2)\n exact mul_le_mul_of_nonneg_left hĈ5\n (mul_nonneg (by norm_num : (0 : ℝ) ≤ 400000) hA0nn)\n have h2 : 400000 * A0count * (5 * Real.log R) * (Real.log R) ^ 2\n = C₁ * (Real.log R) ^ 3 := by\n rw [hC1]\n ring\n have h3 : C₁ * (Real.log R) ^ 3 ≤ 64 * C₁ * Q ^ 3 := by\n have h := mul_le_mul_of_nonneg_left hL3 hC₁nn\n have h' : C₁ * (64 * Q ^ 3) = 64 * C₁ * Q ^ 3 := by ring\n rwa [h'] at h\n linarith [h1, h2, h3]\n have hRBle : RB + ‖Gentire 0‖ ≤ C₀' + 64 * C₁ * Q ^ 3 := by\n rw [hRB, hC0']\n linarith [hbig]\n -- the real squeeze: (RB + ‖Gentire 0‖)/R·‖z₀‖ ≤ ε\n have hc1 : 128 * C₁ * ‖z₀‖ ≤ ε * Q := by\n have h1 : (128 * C₁ + 2 * C₀') * ‖z₀‖ / ε ≤ c := by rw [hc]; linarith\n have h2 : (128 * C₁) * ‖z₀‖ ≤ (128 * C₁ + 2 * C₀') * ‖z₀‖ := by\n apply mul_le_mul_of_nonneg_right _ (norm_nonneg _)\n linarith [hC₀'nn]\n have h3 : (128 * C₁) * ‖z₀‖ / ε ≤ c :=\n (div_le_div_of_nonneg_right h2 hε.le).trans h1\n calc (128 * C₁) * ‖z₀‖ = (128 * C₁) * ‖z₀‖ / ε * ε := by\n rw [div_mul_cancel₀ _ hε.ne']\n _ ≤ c * ε := mul_le_mul_of_nonneg_right h3 hε.le\n _ ≤ Q * ε := mul_le_mul_of_nonneg_right hQc hε.le\n _ = ε * Q := by ring\n have hA : 64 * C₁ * Q ^ 3 * ‖z₀‖ ≤ (ε / 2) * Q ^ 4 := by\n have h1 : (64 * C₁ * ‖z₀‖) * Q ^ 3 ≤ ((ε / 2) * Q) * Q ^ 3 := by\n apply mul_le_mul_of_nonneg_right _ (pow_nonneg hQnn 3)\n have h64 : (64 : ℝ) * C₁ * ‖z₀‖ = (128 * C₁ * ‖z₀‖) / 2 := by ring\n have hhalf : (ε / 2) * Q = (ε * Q) / 2 := by ring\n rw [h64, hhalf]\n linarith [hc1]\n have hL' : (64 * C₁ * ‖z₀‖) * Q ^ 3 = 64 * C₁ * Q ^ 3 * ‖z₀‖ := by ring\n have hR' : ((ε / 2) * Q) * Q ^ 3 = (ε / 2) * Q ^ 4 := by ring\n rwa [hL', hR'] at h1\n have hB : C₀' * ‖z₀‖ ≤ (ε / 2) * Q ^ 4 := by\n have h1 : (2 * C₀') * ‖z₀‖ ≤ ε * Q := by\n have h2 : (2 * C₀') * ‖z₀‖ ≤ (128 * C₁ + 2 * C₀') * ‖z₀‖ := by\n apply mul_le_mul_of_nonneg_right _ (norm_nonneg _)\n linarith [hC₁nn]\n have h3 : (128 * C₁ + 2 * C₀') * ‖z₀‖ / ε ≤ c := by rw [hc]; linarith\n have h4 : (2 * C₀') * ‖z₀‖ / ε ≤ c :=\n (div_le_div_of_nonneg_right h2 hε.le).trans h3\n calc (2 * C₀') * ‖z₀‖ = (2 * C₀') * ‖z₀‖ / ε * ε := by\n rw [div_mul_cancel₀ _ hε.ne']\n _ ≤ c * ε := mul_le_mul_of_nonneg_right h4 hε.le\n _ ≤ Q * ε := mul_le_mul_of_nonneg_right hQc hε.le\n _ = ε * Q := by ring\n have hQ2 : (2 : ℝ) ≤ Q := by linarith [hQc, hcz]\n have hQ3 : (2 : ℝ) ≤ Q ^ 3 := by\n have h := pow_le_pow_left₀ (by norm_num : (0 : ℝ) ≤ 2) hQ2 3\n norm_num at h\n linarith [h]\n have h2 : ε * Q ≤ (ε / 2) * Q ^ 4 := by\n have h3 : (ε / 2) * Q ^ 4 = ((ε / 2) * Q) * Q ^ 3 := by ring\n rw [h3]\n have h6 : (ε / 2) * Q * 2 ≤ (ε / 2) * Q * Q ^ 3 :=\n mul_le_mul_of_nonneg_left hQ3 (by positivity)\n have h5 : ε * Q = (ε / 2) * Q * 2 := by ring\n rw [h5]\n exact h6\n have h7 : C₀' * ‖z₀‖ ≤ 2 * C₀' * ‖z₀‖ := by\n have h : (0 : ℝ) ≤ C₀' * ‖z₀‖ := mul_nonneg hC₀'nn (norm_nonneg _)\n linarith [h]\n linarith [h7, h1, h2]\n have hsum : (RB + ‖Gentire 0‖) * ‖z₀‖ ≤ ε * Q ^ 4 := by\n have h1 : (RB + ‖Gentire 0‖) * ‖z₀‖ ≤ (C₀' + 64 * C₁ * Q ^ 3) * ‖z₀‖ :=\n mul_le_mul_of_nonneg_right hRBle (norm_nonneg _)\n have h2 : (C₀' + 64 * C₁ * Q ^ 3) * ‖z₀‖\n = C₀' * ‖z₀‖ + 64 * C₁ * Q ^ 3 * ‖z₀‖ := by ring\n linarith [h1, h2, hA, hB]\n have hmain : (RB + ‖Gentire 0‖) / R * ‖z₀‖ ≤ ε := by\n have hQ4pos : (0 : ℝ) < Q ^ 4 := pow_pos hQpos 4\n have h1 : (RB + ‖Gentire 0‖) / R * ‖z₀‖ = (RB + ‖Gentire 0‖) * ‖z₀‖ / Q ^ 4 := by\n rw [hR4]\n ring\n rw [h1, div_le_iff₀ hQ4pos]\n exact hsum\n -- assemble\n have hdz0 : dist z₀ (0 : ℂ) = ‖z₀‖ := by rw [dist_eq_norm, sub_zero]\n calc dist (Gentire z₀) (Gentire 0)\n ≤ (RB + ‖Gentire 0‖) / R * dist z₀ 0 := hschwarz\n _ = (RB + ‖Gentire 0‖) / R * ‖z₀‖ := by rw [hdz0]\n _ ≤ ε := hmain\n -- dist < every ε ⟹ dist = 0\n rcases le_or_lt (dist (Gentire z₀) (Gentire 0)) 0 with h | h\n · exact dist_eq_zero.mp (le_antisymm h dist_nonneg)\n · have h2 := key (dist (Gentire z₀) (Gentire 0) / 2) (by linarith)\n linarith\n\n/-! ## 5. The capstone: the partial-fraction identity -/\n\n/-- **The ii′-5e capstone** (D-068 §5): under the perimeter zero count\n`ZeroCountProp`, the completed partial-fraction identity\nζ′/ζ(s) = B + Σ_ρ m_ρ(1/(s−ρ) + 1/ρ) − 1/s − 1/(s−1) + ½log π − ½ψ(s/2)\nholds at every s off the excluded set. Proof: the difference Fexpr is\nentire (5e-iv) and O((log R)²·Ĉ₀) = o(R) on the γ-gap circles\n(`Fexpr_circle_le`), so the max-modulus + Schwarz squeeze (`gentire_const`)\nforces it constant. -/\ntheorem partialFraction_identity (hZC : ZeroCountProp) :\n ∃ B : ℂ, ∀ s : ℂ, riemannZeta s ≠ 0 → s ≠ 0 → s ≠ 1 →\n (∀ n : ℕ, 1 ≤ n → s ≠ -2 * (n : ℂ)) →\n logDeriv riemannZeta s\n = B + seriesFun s - 1 / s - 1 / (s - 1) + (Real.log Real.pi : ℂ) / 2\n - Complex.digamma (s / 2) / 2 := by\n refine ⟨Gentire 0, fun s hζ hs0 hs1 hsn => ?_⟩\n have hgood : ¬ badPoint s := by\n rintro (h | h | h | ⟨n, hn, h⟩)\n · exact hζ h.1\n · exact hs0 h\n · exact hs1 h\n · exact hsn n hn h\n have hG : Fexpr s = Gentire 0 := by\n rw [← gentire_eq_Fexpr hgood]\n exact gentire_const hZC s\n rw [Fexpr] at hG\n linear_combination hG\n\nend NguyenRH1\n\nend\n"},"extra_content":null}]