← Session 24 — ii′-2…4: swaps, (4.10) design, contour + website roadmap fixes
thinking (317 chars)
`Nat.natCast_floor_eq_intCast_floor (ha : 0 ≤ a) : (⌊a⌋₊ : R) = ⌊a⌋` (Ring.lean:895, in Nat namespace presumably — so `Nat.natCast_floor_eq_intCast_floor`).
Now write the file. I'll write §1 (b2Fun machinery) first and compile, then proceed section by section. Let me be careful about all the gotchas banked so far.
`Nat.natCast_floor_eq_intCast_floor` confirmed. Writing LiRBound.lean §1 (the B̃₂ machinery).
tool: Write
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiRBound.lean",
"content": "/-\nNguyenRH1/LiRBound.lean \u2014 tier ii\u2032 sub-stage ii\u2032-5 (design D-067):\nthe R-bound for \u2212\u03b6\u2032/\u03b6 off the near zeros, by the Davenport local route.\n\n\u00a71 (this file's first block, ii\u2032-5b): the second periodic Bernoulli\nfunction B\u0303\u2082 and the level-2 Euler\u2013Maclaurin representation\n\n \u03b6(s) = 1/2 + 1/(s\u22121) \u2212 s(s+1)\u00b7\u222b\u2081^\u221e B\u0303\u2082(x)\u00b7x^{\u2212s\u22122} dx (re s > \u22121, s \u2260 1)\n\ngiving the polynomial bound \u2016\u03b6(s)\u2016 \u2264 (3/4)|t|\u00b2 on the disc\nB(2+it, 5/2) (\u03c3 \u2265 \u22121/2, |t| \u2265 10) \u2014 the \u0393-free strip bound that the\nDavenport disc argument (ii\u2032-5c) consumes. B\u0303\u2082(x) = (u\u00b2\u2212u)/2 with\nu = Int.fract x: continuous (endpoint-matched via `ContinuousOn.comp_fract''`),\n1-periodic, values in [\u22121/8, 0]; HasDerivAt (fract x \u2212 1/2) off \u2124.\n\nRoute (D-067 \u00a72): one IBP level over Zeta23's B\u2081 representation\n`Zeta0EqZeta` (riemannZeta0 1 s = riemannZeta s for re s > 0), then the\nidentity principle across re s = 0. No complex Stirling, no Hadamard.\n\nArchive references: D-067, D-064 \u00a74 R3, journal-022.\n-/\nimport Mathlib\nimport Zeta23.FromPNTPlus.ZetaBounds\nimport NguyenRH1.LiContour\n\nopen Zeta23 Complex Filter Topology\nopen scoped Nat\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. The periodic Bernoulli primitive B\u0303\u2082 -/\n\n/-- The second periodic Bernoulli function: B\u0303\u2082(x) = (u\u00b2\u2212u)/2 with\nu = Int.fract x \u2208 [0,1). Continuous, 1-periodic, values in [\u22121/8, 0];\nan antiderivative of the sawtooth Int.fract x \u2212 1/2 off the integers. -/\ndef b2Fun (x : \u211d) : \u211d := (Int.fract x ^ 2 - Int.fract x) / 2\n\n/-- B\u0303\u2082 is 1-periodic (global \u2014 Int.fract is). -/\ntheorem b2Fun_add_one (x : \u211d) : b2Fun (x + 1) = b2Fun x := by\n unfold b2Fun\n rw [Int.fract_add_one]\n\n/-- The range of B\u0303\u2082: \u22121/8 \u2264 B\u0303\u2082(x) \u2264 0 (u(1\u2212u) \u2208 [0, 1/4] for u \u2208 [0,1)). -/\ntheorem b2Fun_range (x : \u211d) : -1/8 \u2264 b2Fun x \u2227 b2Fun x \u2264 0 := by\n have hu0 : 0 \u2264 Int.fract x := Int.fract_nonneg x\n have hu1 : Int.fract x < 1 := Int.fract_lt_one x\n unfold b2Fun\n constructor\n \u00b7 nlinarith [sq_nonneg (Int.fract x - 1/2)]\n \u00b7 nlinarith\n\ntheorem abs_b2Fun_le (x : \u211d) : |b2Fun x| \u2264 1/8 := by\n obtain \u27e8h1, h2\u27e9 := b2Fun_range x\n rw [abs_of_nonpos h2]\n linarith\n\n/-- B\u0303\u2082 vanishes at the integers (fract = 0 there). -/\ntheorem b2Fun_intCast (n : \u2124) : b2Fun (n : \u211d) = 0 := by\n unfold b2Fun\n rw [Int.fract_intCast]\n norm_num\n\ntheorem b2Fun_one : b2Fun 1 = 0 := by\n have := b2Fun_intCast 1\n norm_num at this\n exact this\n\n/-- B\u0303\u2082 is continuous everywhere: b2Fun = g \u2218 Int.fract with\ng(u) = (u\u00b2\u2212u)/2 on [0,1] satisfying g(0) = g(1). -/\ntheorem continuous_b2Fun : Continuous b2Fun :=\n ContinuousOn.comp_fract'' (f := fun u : \u211d => (u ^ 2 - u) / 2)\n ((continuous_fun_by_fun_prop := by fun_prop).continuousOn) (by norm_num)\n\n/-- Off the integers, B\u0303\u2082 has derivative fract x \u2212 1/2. -/\ntheorem hasDerivAt_b2Fun {x : \u211d} (hx : Int.fract x \u2260 0) :\n HasDerivAt b2Fun (Int.fract x - 1/2) x := by\n have hIco : Set.Ico (\u230ax\u230b : \u211d) (\u230ax\u230b + 1) \u2208 \ud835\udcdd x := by\n apply Set.Ico_mem_nhds _ (Int.lt_floor_add_one x)\n exact (Int.floor_le x).lt_of_ne (fun h => hx (by rw [Int.fract, h, sub_self]))\n have hEq : (Int.fract : \u211d \u2192 \u211d) =\u1da0[\ud835\udcdd x] fun y => y - (\u230ax\u230b : \u211d) := by\n filter_upwards [hIco] with y hy\n rw [Int.fract, Int.floor_eq_on_Ico _ _ hy]\n have hf : HasDerivAt (Int.fract : \u211d \u2192 \u211d) 1 x := by\n have h := (hasDerivAt_id x).sub_const (\u230ax\u230b : \u211d)\n rw [sub_zero] at h\n exact h.congr_of_eventuallyEq hEq\n unfold b2Fun\n have h2 := ((hf.pow 2).sub hf).div_const 2\n convert h2 using 1\n ring\n\nend NguyenRH1\n\nend\n"
}
raw content_json (database row)
[{"type":"thinking","thinking":"`Nat.natCast_floor_eq_intCast_floor (ha : 0 ≤ a) : (⌊a⌋₊ : R) = ⌊a⌋` (Ring.lean:895, in Nat namespace presumably — so `Nat.natCast_floor_eq_intCast_floor`). \n\nNow write the file. I'll write §1 (b2Fun machinery) first and compile, then proceed section by section. Let me be careful about all the gotchas banked so far.","signature":""},{"type":"text","text":"`Nat.natCast_floor_eq_intCast_floor` confirmed. Writing LiRBound.lean §1 (the B̃₂ machinery)."},{"type":"tool_use","id":"Write_190","name":"Write","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiRBound.lean","content":"/-\nNguyenRH1/LiRBound.lean — tier ii′ sub-stage ii′-5 (design D-067):\nthe R-bound for −ζ′/ζ off the near zeros, by the Davenport local route.\n\n§1 (this file's first block, ii′-5b): the second periodic Bernoulli\nfunction B̃₂ and the level-2 Euler–Maclaurin representation\n\n ζ(s) = 1/2 + 1/(s−1) − s(s+1)·∫₁^∞ B̃₂(x)·x^{−s−2} dx (re s > −1, s ≠ 1)\n\ngiving the polynomial bound ‖ζ(s)‖ ≤ (3/4)|t|² on the disc\nB(2+it, 5/2) (σ ≥ −1/2, |t| ≥ 10) — the Γ-free strip bound that the\nDavenport disc argument (ii′-5c) consumes. B̃₂(x) = (u²−u)/2 with\nu = Int.fract x: continuous (endpoint-matched via `ContinuousOn.comp_fract''`),\n1-periodic, values in [−1/8, 0]; HasDerivAt (fract x − 1/2) off ℤ.\n\nRoute (D-067 §2): one IBP level over Zeta23's B₁ representation\n`Zeta0EqZeta` (riemannZeta0 1 s = riemannZeta s for re s > 0), then the\nidentity principle across re s = 0. No complex Stirling, no Hadamard.\n\nArchive references: D-067, D-064 §4 R3, journal-022.\n-/\nimport Mathlib\nimport Zeta23.FromPNTPlus.ZetaBounds\nimport NguyenRH1.LiContour\n\nopen Zeta23 Complex Filter Topology\nopen scoped Nat\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. The periodic Bernoulli primitive B̃₂ -/\n\n/-- The second periodic Bernoulli function: B̃₂(x) = (u²−u)/2 with\nu = Int.fract x ∈ [0,1). Continuous, 1-periodic, values in [−1/8, 0];\nan antiderivative of the sawtooth Int.fract x − 1/2 off the integers. -/\ndef b2Fun (x : ℝ) : ℝ := (Int.fract x ^ 2 - Int.fract x) / 2\n\n/-- B̃₂ is 1-periodic (global — Int.fract is). -/\ntheorem b2Fun_add_one (x : ℝ) : b2Fun (x + 1) = b2Fun x := by\n unfold b2Fun\n rw [Int.fract_add_one]\n\n/-- The range of B̃₂: −1/8 ≤ B̃₂(x) ≤ 0 (u(1−u) ∈ [0, 1/4] for u ∈ [0,1)). -/\ntheorem b2Fun_range (x : ℝ) : -1/8 ≤ b2Fun x ∧ b2Fun x ≤ 0 := by\n have hu0 : 0 ≤ Int.fract x := Int.fract_nonneg x\n have hu1 : Int.fract x < 1 := Int.fract_lt_one x\n unfold b2Fun\n constructor\n · nlinarith [sq_nonneg (Int.fract x - 1/2)]\n · nlinarith\n\ntheorem abs_b2Fun_le (x : ℝ) : |b2Fun x| ≤ 1/8 := by\n obtain ⟨h1, h2⟩ := b2Fun_range x\n rw [abs_of_nonpos h2]\n linarith\n\n/-- B̃₂ vanishes at the integers (fract = 0 there). -/\ntheorem b2Fun_intCast (n : ℤ) : b2Fun (n : ℝ) = 0 := by\n unfold b2Fun\n rw [Int.fract_intCast]\n norm_num\n\ntheorem b2Fun_one : b2Fun 1 = 0 := by\n have := b2Fun_intCast 1\n norm_num at this\n exact this\n\n/-- B̃₂ is continuous everywhere: b2Fun = g ∘ Int.fract with\ng(u) = (u²−u)/2 on [0,1] satisfying g(0) = g(1). -/\ntheorem continuous_b2Fun : Continuous b2Fun :=\n ContinuousOn.comp_fract'' (f := fun u : ℝ => (u ^ 2 - u) / 2)\n ((continuous_fun_by_fun_prop := by fun_prop).continuousOn) (by norm_num)\n\n/-- Off the integers, B̃₂ has derivative fract x − 1/2. -/\ntheorem hasDerivAt_b2Fun {x : ℝ} (hx : Int.fract x ≠ 0) :\n HasDerivAt b2Fun (Int.fract x - 1/2) x := by\n have hIco : Set.Ico (⌊x⌋ : ℝ) (⌊x⌋ + 1) ∈ 𝓝 x := by\n apply Set.Ico_mem_nhds _ (Int.lt_floor_add_one x)\n exact (Int.floor_le x).lt_of_ne (fun h => hx (by rw [Int.fract, h, sub_self]))\n have hEq : (Int.fract : ℝ → ℝ) =ᶠ[𝓝 x] fun y => y - (⌊x⌋ : ℝ) := by\n filter_upwards [hIco] with y hy\n rw [Int.fract, Int.floor_eq_on_Ico _ _ hy]\n have hf : HasDerivAt (Int.fract : ℝ → ℝ) 1 x := by\n have h := (hasDerivAt_id x).sub_const (⌊x⌋ : ℝ)\n rw [sub_zero] at h\n exact h.congr_of_eventuallyEq hEq\n unfold b2Fun\n have h2 := ((hf.pow 2).sub hf).div_const 2\n convert h2 using 1\n ring\n\nend NguyenRH1\n\nend\n"},"extra_content":null}]