← Session 35 — ii′-6-R: Lagarias 6.1 right-tail re-proof (E-032/D-073)
thinking (23788 chars)
Remaining errors:
1. **Line 1118 (X_le_three_pow's `e` at 1117-1122)**: "unsolved goals" with context ending at hΛ — the field_simp at 1122 — the `rw [show (2·√↑n) = (2·√↑n−2)+2 by ring, Real.rpow_add hm2]; field_simp [hm2.ne']` — the field_simp's leftover. Hmm — the context shown ends at hΛ (line 1108-1110) — the goal at 1118:68 (the e statement's RHS line). The `field_simp [hm2.ne']` at 1122 — maybe it left goals. Let me look at what e's proof produces: e : Λ m / ↑m ^ (2√↑n) = (1/↑m ^ (2√↑n−2))·(Λ m / ↑m ^ 2) — after rw [show σ-form, rpow_add]: goal becomes Λ m / (↑m^{2√↑n−2}·↑m^2) = (1/↑m^{2√↑n−2})·(Λ m/↑m^2) — field_simp [hm2.ne'] clears ✓ should close by its internal ring ✓ — "unsolved goals"?? — hmm, the context shown is from BEFORE e (hΛ at 1108) — the error at 1118:68 is probably the `rw [show ... by ring, Real.rpow_add hm2]` — the rw [Real.rpow_add hm2] — hm2 : 0 < (m:ℝ) — Real.rpow_add (hx : 0 < x) : x ^ (y+z) = x^y · x^z ✓ — hmm.
Actually — the context display might be truncated (shows only up to hΛ). The `unsolved goals` with just that context suggests the whole `e` have failed. Let me look at the FULL goal state — I only see context, not the goal. The issue could be `Real.rpow_add hm2` — signature: `Real.rpow_add (hx : 0 < x) (y z : ℝ) : x ^ (y + z) = x ^ y * x ^ z` — with hm2 : 0 < ↑m ✓.
Hmm — wait, maybe the problem is the `show (2·√↑n) = (2·√↑n−2)+2 by ring` — 2√↑n = (2√↑n − 2) + 2 ⟺ 0 = −2 ✓?? NO: (2√↑n − 2) + 2 = 2√↑n ✓ ring proves it ✓.
Then `Real.rpow_add hm2` rewrites ↑m^((2√↑n−2)+2) → ↑m^(2√↑n−2)·↑m^2 ✓ then field_simp... The goal at that point: Λ m / (↑m^{2√↑n−2}·↑m^2) = (1/↑m^{2√↑n−2})·(Λ m/↑m^2) — field_simp [hm2.ne'] — clears denominators ✓ should close. "unsolved goals" — maybe field_simp left `Λ m = Λ m`?? which closes by rfl automatically...
Let me look at the actual goal text — the sed output only showed context (no ⊢ goal line for 1118). Let me get it.
2. **Line 1166 (hfin's rw [hΛ2])**: pattern `‖(fun n => ↑(Λ n)) 2‖` not found in `|ArithmeticFunction.vonMangoldt 2| / 2 ^ (2·√↑n) = ...` — the target has `|ArithmeticFunction.vonMangoldt 2|` — the norm-term output's norm is displayed as `|...|` — and my hΛ2's pattern is `‖(fun n => ↑(Λ n)) 2‖` — hmm — the goal shows `|ArithmeticFunction.vonMangoldt 2|` — that's `Complex.abs (Λ 2)`?? or the norm ‖·‖ displayed as |·|? — in Lean 4 the norm ‖x‖ prints as `‖x‖` (double bars) or `|x|`?? — Mathlib prints `‖x‖` as `‖x‖` typically... but the display shows `|ArithmeticFunction.vonMangoldt 2|` — single bars — that's `Complex.abs`?? no — it's the NORM of the cast, printed as |x|? Hmm — actually in Lean4/Mathlib, ‖x‖ displays as `‖x‖` usually, but `(‖x‖ : ℝ)` for complex might display as `|x|` — uncertain. The pattern mismatch means the goal's norm form differs from hΛ2's. The `simp [ArithmeticFunction.vonMangoldt_apply_one]` before hΛ2 — simp might have rewritten `‖(fun n => ↑(Λ n)) 2‖` into `|Λ 2|` (some norm-simp form!) — so the goal's norm is in a DIFFERENT form than hΛ2's. Fix: make hΛ2 match the goal's displayed form `|ArithmeticFunction.vonMangoldt 2|` — hmm — what IS that form? `Complex.abs (ArithmeticFunction.vonMangoldt 2)`?? or `‖(ArithmeticFunction.vonMangoldt 2 : ℂ)‖` displayed as |·|? — Complex.abs is DEFINED as the norm (Complex.abs z = ‖z‖ defeq — `Complex.abs z := norm z`?? — actually `Complex.abs` is notation/instance for the norm ✓ defeq). So `|Λ 2|` IS `‖(Λ 2 : ℂ)‖` in another display. My hΛ2's pattern `‖(fun n => ↑(Λ n)) 2‖` — the `(fun n => (↑(Λ n)):ℂ) 2` beta-redex — the goal's `|Λ 2|` is `‖(↑(Λ 2)):ℂ‖` — beta-reduced — MISMATCH (redex vs reduced). rw's matching: does it see through beta-redexes? NO. Fix: state hΛ2 with the beta-reduced form `‖(ArithmeticFunction.vonMangoldt 2 : ℂ)‖`... — wait, that's what I had ORIGINALLY and the 1168 error said pattern `‖↑(Λ 2)‖` not found in `|Λ 2| / ...` — the SAME display!! So `‖(ArithmeticFunction.vonMangoldt 2 : ℂ)‖` doesn't match `|ArithmeticFunction.vonMangoldt 2|` either?! — the display `|...|` vs `‖...‖` — if they were the same term, rw would match regardless of display. So the goal's norm is genuinely DIFFERENT: it must be `Complex.abs`?? no wait — or `Real.norm_eq_abs`-style `|x|` for a REAL?? — `|ArithmeticFunction.vonMangoldt 2|` — if Λ 2 is REAL, then `|Λ 2|` is Real.abs!! — the norm_term_eq produces `‖f n‖` with f n : ℂ — but simp might have rewritten the ℂ-norm of the real cast to the REAL abs: `Complex.norm_ofReal : ‖(x : ℂ)‖ = |x|`?? no wait — simp [vonMangoldt_apply_one] — that lemma is about Λ 1 — shouldn't touch Λ 2's norm form. Hmm — unless norm_term_eq's `‖f n‖` with f n = (↑(Λ n)):ℂ — the simp normalized it to `|Λ 2|`...
Let me check what the term actually is: the goal at 1166 is `|ArithmeticFunction.vonMangoldt 2| / 2 ^ (2·√↑n) = Real.log 2 * 2 ^ (-(2·√↑n))`. The `|...|` — hmm — actually in Mathlib 4, `‖(x : ℂ)‖` for a REAL-VALUED complex number — the norm — prints as `‖x‖`. `|x|` is for Real/Int abs OR `Complex.abs` (which is a DEF := norm?). Actually — `Complex.abs z` is defined as `norm z`?? No — `Complex.abs (z : ℂ) : ℝ := norm z`?? Hmm — Complex.abs is `abs z := Real.sqrt (normSq z)`?? — historically Complex.abs was its own definition but in current Mathlib `Complex.abs = norm` defeq. The display `|...|` for complex norms IS used for `Complex.abs`. Since norm_term_eq's norm is the normed-field norm ‖·‖, the display should be ‖·‖...
OK regardless — the issue is beta-redex vs reduced. The goal's `|Λ 2|` is the BETA-REDUCED norm ‖↑(Λ 2)‖ — and my hΛ2's pattern has the redex `(fun n => ↑(Λ n)) 2`. Fix: make hΛ2's LHS match the goal — state hΛ2 as `‖(ArithmeticFunction.vonMangoldt 2 : ℂ)‖ = Real.log 2`... — but that's what the ORIGINAL had and it failed too (1168 error: pattern `‖↑(Λ 2)‖` not found in `|Λ 2| / ...`). So `‖(ArithmeticFunction.vonMangoldt 2 : ℂ)‖` ≠ the goal's `|ArithmeticFunction.vonMangoldt 2|`?? — those should be the SAME term (cast of Λ 2, normed). UNLESS the goal's `|Λ 2|` is `Real.abs (ArithmeticFunction.vonMangoldt 2)` — REAL abs — meaning simp rewrote the complex norm of the real cast to a REAL abs — `Complex.norm_ofReal : ‖(x : ℂ)‖ = |x|` — is that a simp lemma?? — `Complex.norm_ofReal (x : ℝ) : ‖(x : ℂ)‖ = |x|` — might be simp-tagged!! So after `simp [vonMangoldt_apply_one]`, the norm became `|Λ 2|` (real abs of the real Λ 2). Then the correct hΛ2 form: `|ArithmeticFunction.vonMangoldt 2| = Real.log 2` — via abs_of_nonneg: `abs_of_nonneg (h : 0 ≤ a) : |a| = a` ✓ — with Λ 2 = log 2 ≥ 0 ✓:
```
have hΛ2 : |ArithmeticFunction.vonMangoldt 2| = Real.log 2 := by
rw [ArithmeticFunction.vonMangoldt_apply_prime Nat.prime_two]
exact abs_of_nonneg (by linarith [Real.log_two_gt_d9] : (0 : ℝ) ≤ Real.log 2)
rw [hΛ2]
```
abs_of_nonneg (hx : 0 ≤ x) : |x| = x ✓.
Hmm — but the goal might not have gone through norm_ofReal — the display `|...|` might just be how Lean prints ‖·‖ for these. The safest: match the goal's EXACT form — since the goal displays `|ArithmeticFunction.vonMangoldt 2|`, and if it's ‖(Λ 2 : ℂ)‖ the hΛ2 with `‖(Λ 2 : ℂ)‖` should match... it didn't. So it's the Real abs. Use the abs form.
Actually — hmm, `LSeries.norm_term_eq` produces `‖f n‖ / n ^ s.re` with f n : ℂ and the norm being the ℂ norm — the display as `|...|` is probably just the pretty-printer for ‖·‖ on complex with real content?? I'm not sure. Try both: if `‖(Λ 2 : ℂ)‖` fails and `|Λ 2|` (Real abs) works, use the abs. The previous hΛ2 edit used `(fun n => (↑(Λ n)):ℂ) 2` — redex — fails. The goal's form is beta-reduced. Use:
```
have hΛ2 : (‖(ArithmeticFunction.vonMangoldt 2 : ℂ)‖ : ℝ) = Real.log 2 := by
rw [ArithmeticFunction.vonMangoldt_apply_prime Nat.prime_two,
Complex.norm_of_nonneg (by linarith [Real.log_two_gt_d9] : (0 : ℝ) ≤ Real.log 2)]
```
if the goal's |·| is the ℂ norm — if it's Real.abs, use abs_of_nonneg. Ugh — let me determine which by probing: the display in the error: `|ArithmeticFunction.vonMangoldt 2| / 2 ^ (2 * √↑n)` — in Lean 4, the pretty printer renders `‖x‖` as `‖x‖` and `|x|` for Real.abs — a complex norm of a REAL-number-typed expression: Λ 2 : ℝ cast to ℂ, its norm is ℂ-norm, rendered `‖↑(Λ 2)‖` usually. The error displays `|ArithmeticFunction.vonMangoldt 2|` — single bars with the REAL Λ 2 inside (not `↑(Λ 2)` cast!) — so it IS Real.abs (the argument is the REAL vonMangoldt 2, not the complex cast). So simp rewrote ‖↑(Λ 2)‖ → |Λ 2| (via Complex.norm_ofReal as a simp lemma — wait — `Complex.norm_ofReal : ‖(x : ℂ)‖ = |x|`?? — hmm, actually it's `Complex.norm_ofReal (x : ℝ) : ‖(x : ℂ)‖ = ‖x‖`?? — there's `Complex.norm_ofReal` and also the simp might use `Complex.abs_ofReal`... whatever — the goal has the REAL abs form.
Fix hΛ2 as `|ArithmeticFunction.vonMangoldt 2| = Real.log 2` with abs_of_nonneg ✓.
3. **Line 1235 (log_nine_quarters_ge's rwa)**: "Tactic `assumption` failed" — the rwa [Real.log_exp] at h2 — h2 : log(9/4) ≤ 0.811 — the GOAL of log_nine_quarters_ge is `(0.811 : ℝ) ≤ Real.log (9 / 4)` — h2 gives the WRONG DIRECTION (log(9/4) ≤ 0.811 vs goal 0.811 ≤ log(9/4))!! — I proved log(9/4) ≤ 0.811 but the lemma wants 0.811 ≤ log(9/4). And Real.log_le_log (0 < 9/4) (hprod : 9/4 ≤ exp 0.811) : log(9/4) ≤ log(exp 0.811) = 0.811 — that's log(9/4) ≤ 0.811 — WRONG direction again! I need 9/4 ≤ exp 0.811 ⟹ log(9/4) ≤ 0.811 — hmm — but I want log(9/4) ≥ 0.811 — which needs exp 0.811 ≤ 9/4?? NO: log(9/4) ≥ 0.811 ⟺ 9/4 ≥ e^{0.811} ⟺ e^{0.811} ≤ 2.25!! — I had it BACKWARD: log(9/4) ≥ 0.811 ⟺ e^{0.811} ≤ 9/4 — the hprod should be `Real.exp 0.811 ≤ 9/4`?? — wait: log x ≥ 0.811 ⟺ x ≥ e^{0.811} — so 9/4 ≥ e^{0.811} ⟹ log(9/4) ≥ 0.811 ✓. And e^{0.811} ≤ 2.2254·1.01106·... — wait, e^{0.811} = e^{0.8}·e^{0.011} ≤ ??? — for an UPPER bound on e^{0.811}: e^{0.8} ≤ 2.2256?? — hmm — my h08 is `(2.2254 : ℝ) ≤ Real.exp 0.8` (LOWER bound on exp!). For e^{0.811} ≤ 9/4 I need e^{0.811} ≤ 2.25 ⟸ e^{0.8}·e^{0.011} ≤ 2.25 — upper bounds: e^{0.8} ≤ 2.2256 (upper) and e^{0.011} ≤ 1.01107: product ≤ 2.2501 — too fat?? — 2.2256·1.01107 = 2.25023 > 2.25 ✗. Hmm — but the TRUE e^{0.811} = 2.24995 < 2.25 ✓ — slack 0.00005. The certification needs e^{0.811} ≤ 2.25 with slack 5e-5: e^{0.8} ≤ 2.22554 (true 2.2255409) and e^{0.011} ≤ 1.0110607 (true 1.0110607): product 2.25014 > 2.25 ✗ — the upper bounds are too fat individually. Split differently: e^{0.811} ≤ 2.25 ⟺ 0.811 ≤ log 2.25 ⟺ ... — or bound e^{0.811} directly via the partial-sum LOWER bound?? — for UPPER bounds on e^x (x > 0): the (1−x/16)⁻¹⁶ trick: e^{0.811} ≤ (1−0.811/16)⁻¹⁶ = (0.9493125)⁻¹⁶ = (1.05339...)^16: ln: −16·ln(0.9493125) = 16·0.052011 = 0.832176: e^{0.832176} = 2.29843 — way too fat (true 2.24995). e^{0.811} = e^{0.8}·e^{0.011}: e^{0.8} ≤ (1−0.8/16)⁻¹⁶ = (0.95)⁻¹⁶ = (1.052632)¹⁶ = e^{16·0.0512933} = e^{0.820693} = 2.27206 — fat. e^{0.8} ≤ 2.2256 via partial sums?? — partial sums give LOWER bounds (Σ ≤ e^x). For UPPER bounds at x > 0 the only tool is the (1−x/16)⁻¹⁶ (fat at x ~ 0.8).
Alternative: e^{0.811} ≤ 2.25 ⟺ 0.811 ≤ log 2.25: certify log(9/4) ≥ 0.811 directly via log's Taylor/integral?? — or via e^{0.811} ≤ 2.25 with a better decomposition: e^{0.811} = e^{0.75}·e^{0.061}: e^{0.75} ≤ 2.1170 (upper via trick: (1−0.75/16)⁻¹⁶ = (0.953125)⁻¹⁶ = (1.049180)¹⁶ = e^{16·0.048008} = e^{0.768131} = 2.15579 — fat). e^{0.75} ≥ 2.1169 (the h075 from LiBasePoints ✓). Ugh — upper bounds on exp are systematically fat with this machinery.
DIFFERENT approach for log(9/4) ≥ 0.811: use log(9/4) = log 9 − log 4 = 2(log 3 − log 2) — log 3 ≥ 1.0987 (needs e^{1.0987} ≤ 3: e^{1.0987} = e·e^{0.0987} ≤ 2.7182818·1.10373 = 2.99997 ≤ 3 ✓ — e^{0.0987} ≤ 1.10373 via partial... — e^{0.0987}: partial sums give LOWER bound 1+0.0987+0.004871+0.000160 = 1.103731 — that's LOWER; UPPER via trick (1−0.0987/16)⁻¹⁶ = (0.993831)⁻¹⁶ = e^{16·0.006188} = e^{0.099014} = 1.104083 — then e^{1.0987} ≤ 2.7182818·1.104083 = 3.001342 ≥ 3 ✗ fat again!!) — hmm — the e^small upper bounds keep overshooting the tight thresholds.
Hmm hmm. Let me think about what log-bound directions the machinery CAN do tightly:
- log x ≥ B ⟺ x ≥ e^B ⟸ e^B ≤ x — needs e^B ≤ x certified: partial-sum LOWER bounds on e^B (tight!): e^B ≥ Σ₀ᴷ B^i/i! — with enough terms this is TIGHT (error ~B^{K+1}/(K+1)! tiny). For B = 0.811: Σ₀⁹(0.811^i/i!) = ? — the tail beyond 9: 0.811^10/10! ~ 0.811^10/3628800 ~ 0.125/3628800 ~ 3.4e-8 — plus the geometric continuation — the partial sum Σ₀⁹ ≈ e^{0.811} − ~5e-8 ≈ 2.24990. So e^{0.811} ≥ 2.2499 — that's a LOWER bound (e^B ≥ partial). For e^B ≤ x (x = 2.25): need e^{0.811} ≤ 2.25 — the lower bound 2.2499 ≤ 2.25 doesn't give it.
For log x ≥ B, the cleanest tight route: x·e^{−B} ≥ 1 ⟺ ... no. OR use log(1+y) ≥ y − y²/2 (the standard log bound): log(9/4) = log(1+5/4) with y = 5/4 > 1 — the y−y²/2 bound fails for y > 1. log(9/4) = log 9 − log 4: log 9 = 2 log 3, log 4 = 2 log 2: = 2(log 3 − log 2). log 3 ≥ 1.098612 (certifiable tightly how?): log 3 ≥ B ⟺ 3 ≥ e^B: e^{1.0986} ≥ Σ₀⁹(1.0986^i/i!) — tight partial ≈ e^{1.0986} − small ≈ 2.9996 ≤ 3 ✓!! — e^{1.0986} ≤ 3 certified by the partial sum giving e^{1.0986} ≥ ... — NO — the partial sum is a LOWER bound on e^B: e^{1.0986} ≥ 2.9996 — that says e^{1.0986} is AT LEAST 2.9996 — for e^{1.0986} ≤ 3 I need an UPPER bound. DAMN.
For log x ≥ B (lower bound on log): x ≥ e^B — I need e^B ≤ x — UPPER bound on e^B. The partial sums give lower bounds only. The (1−x/16)⁻¹⁶ trick gives upper bounds but FAT (error ~(x/16)·16·(x/2)·... = x²/32·... ≈ x²/32·1 = for x = 1.0986: 1.0986²/32 = 0.0377 (3.7% fat) — e^{1.0986} ≤ 2.9996·1.0377 = 3.1127 ≥ 3 ✗ USELESS.
Hmm — so how did LiBasePoints certify log 80000 ≥ 11.263?! Line 83: `log80000_ge : (11.263 : ℝ) ≤ Real.log 80000 := by have h1 : Real.exp 11 ≤ 59874.31; have h2 : Real.exp 0.263 ≤ 1.3037; ...` — e^{11.263} = e^{11}·e^{0.263} ≤ 59874.31·1.3037 = 78057 ≤ 80000 ✓ — e^{11} ≤ 59874.31 (upper via exp_one_pow_le 11 : e^11 = (e^1)^11 ≤ 2.7182818286^11 = 59874.30...) ✓ and e^{0.263} ≤ 1.3037 via the (1−x/16)⁻¹⁶ trick (small x = 0.263: trick error ~(0.263²/32)·... = 0.0022 (0.22%) ✓ acceptable there). So the trick works for SMALL x (≤ 0.3). For x = 0.811 the trick's error is ~2-4% — too fat for my 5e-5 slack.
For log(9/4) ≥ 0.811: write it as log(9/4) = log 9 − log 4 with log 9 ≥ 2.1972 and log 4 ≤ 1.3863: log(9/4) ≥ 2.1972 − 1.3863 = 0.8109 ≥ 0.811?? — 0.8109 < 0.811 ✗!!! — log(9/4) = 0.8109302 < 0.811 — WAIT — is 0.8109302 < 0.811? YES! So log(9/4) ≥ 0.811 is FALSE!!! Let me recompute: log(9/4) = log 2.25 = 0.810930216... — indeed < 0.811!! So my target bound is WRONG. Use 0.8109 instead: log(9/4) ≥ 0.8109 ⟺ 9/4 ≥ e^{0.8109}: e^{0.8109} = e^{0.8}·e^{0.0109}: e^{0.8} ≥ 2.2254 (h08 ✓), e^{0.0109} ≥ 1.01096 (partial): product ≥ 2.2254·1.01096 = 2.249795?? — that's e^{0.8109} ≥ 2.249795 — and I need e^{0.8109} ≤ 2.25 for log(9/4) ≥ 0.8109?? — NO WAIT: log(9/4) ≥ 0.8109 ⟺ 9/4 = 2.25 ≥ e^{0.8109} — the partial gives e^{0.8109} ≥ 2.249795 ≤ 2.25 ✓?? — the LOWER bound on exp is ≤ the true exp ≤ 2.25 ✓ but that's the LOWER bound, not the value — I need the VALUE ≤ 2.25 — the lower bound 2.249795 < 2.25 doesn't certify the value ≤ 2.25!! ARGH — same issue: certifying e^B ≤ x needs UPPER bounds on e^B.
Hmm OK wait — let me reconsider. log(9/4) ≥ 0.8109 ⟺ e^{0.8109} ≤ 2.25. To certify e^{0.8109} ≤ 2.25: e^{0.8109} = e^{0.8}·e^{0.0109}: e^{0.8} ≤ UPPER(0.8), e^{0.0109} ≤ UPPER(0.0109): need UPPER(0.8)·UPPER(0.0109) ≤ 2.25. e^{0.8} upper via trick: 2.27206 (fat) ✗. e^{0.8} upper another way: e^{0.8} = e/e^{0.2}: e ≤ 2.7182818286 (d9 ✓); e^{0.2} ≥ Σ₀⁷(0.2^i/i!) = 1+0.2+0.02+0.0013333+0.0000667+0.00000267+0.0000000893+0.00000000255 = 1.2214027 (LOWER ✓): e^{0.8} ≤ 2.7182818286/1.2214027 = 2.22554 ✓✓ TIGHT!! (the e/e^{small} trick — divide by a tight LOWER bound!). Then e^{0.8109} ≤ 2.22554·UPPER(0.0109): e^{0.0109} ≤ (1−0.0109/16)⁻¹⁶ = (0.999319)⁻¹⁶ = e^{16·0.000681} = e^{0.010899} = 1.01096 — tight (small x)! Product: 2.22554·1.01096 = 2.24992 ≤ 2.25 ✓✓✓ (slack 0.00008 — tight but works!).
Actually even simpler: e^{0.8109} = e/e^{0.1891}: e^{0.1891} ≥ Σ₀⁶(0.1891^i/i!) = 1+0.1891+0.01788+0.001127+0.0000533+0.00000202 = 1.20816: e^{0.8109} ≤ 2.7182818286/1.20816 = 2.25000 ≤ 2.25 ✓ (slack ~0.000005 — VERY tight — check: 2.7182818286/1.20816 = 2.249994 ≤ 2.25 ✓ norm_num can verify 2.249994·1.20816 ≤ 2.25·... hmm — the division bound: e/e^{0.1891} ≤ 2.7182818286/1.20816 ⟸ e^{0.1891} ≥ 1.20816 ✓ (partial ✓): then 2.7182818286/1.20816 ≤ 2.25 ⟺ 2.7182818286 ≤ 2.25·1.20816 = 2.71836 ✓ (2.7182818 ≤ 2.71836 ✓ norm_num ✓).
So the cleanest: log(9/4) ≥ 0.8109 via e^{0.8109} = e/e^{0.1891} ≤ 2.7182818286/1.20816 ≤ 2.25 ✓. And log(4/9) = −log(9/4) ≤ −0.8109. Then (4/9)^{√n} ≤ e^{−0.8109·2.236} = e^{−1.8131}·... — the final assembly needs log2 + 9·(4/9)^{√n} ≤ 2.28: (4/9)^{√n} ≤ e^{−0.8109·2.236} = e^{−1.81317}: 1/e^{1.81317} ≤ 1/5.6721-ish — e^{1.81317} ≥ Σ₀⁷(1.81317^i/i!) = 1+1.81317+1.64379+0.99354+0.45042+0.16334+0.04937+0.01279 = 6.12642 ≥ 5.6721 ✓: (4/9)^{√n} ≤ 1/6.12642·... hmm wait — (4/9)^{√n} = e^{√n·log(4/9)} ≤ e^{2.236·log(4/9)} (base < 1, exponent ≥ 2.236 ✓) ≤ e^{2.236·(−0.8109)} = e^{−1.81317} ≤ 1/6.12642 = 0.16323?? — 1/6.12642 = 0.163227 — vs my target 0.17631: 0.16323 ≤ 0.17631 ✓ fine (tighter). Then 9·(4/9)^{√n} ≤ 9·0.16323 = 1.46907: log2 + 9·(4/9)^{√n} ≤ 0.6932+1.46907 = 2.16227 ≤ 2.28 ✓✓ LOTS of slack.
Hmm wait — but I need (4/9)^{√n} ≤ 0.17631-ish for the assembly log2 + 9·(4/9)^{√n} ≤ 2.28: with the tighter 0.16323: 0.6932+1.46907 = 2.16227 ≤ 2.28 ✓ big slack. But the (4/9)^{√n} bound's OWN statement: (4/9)^{√n} ≤ 0.16323 — hmm — let me re-derive: (4/9)^{√n} ≤ (4/9)^{2.236} = e^{2.236·log(4/9)} ≤ e^{2.236·(−0.8109)} = e^{−1.81316}: certify e^{−1.81316} ≤ 0.16323 ⟺ e^{1.81316} ≥ 1/0.16323 = 6.1264: e^{1.81316} ≥ Σ₀⁷(1.81316^i/i!) ≈ 6.1264-ish: partial: 1+1.81316+1.64378+0.99353+0.45042+0.16334+0.04937+0.01279 = 6.12639 ≥ 6.1264?? — 6.12639 < 6.1264 ✗ TIGHT-FAIL. Use more terms or relax to 0.1635: 1/6.12639 = 0.163230 ≤ 0.1635 ✓: then (4/9)^{√n} ≤ 0.1635, 9·0.1635 = 1.4715, log2+1.4715 = 2.1647 ≤ 2.28 ✓✓.
Hmm — this is getting fiddly. Let me just relax the (4/9) bound to something comfortable: (4/9)^{√n} ≤ 0.164 (from e^{1.81316} ≥ 6.12639 ⟹ e^{−1.81316} ≤ 1/6.12639 = 0.163230 ≤ 0.164 ✓ big slack): 9·0.164 = 1.476, +0.6932 = 2.1692 ≤ 2.28 ✓✓.
And log(9/4) ≥ 0.8109 via the e/e^{0.1891} route. Let me rewrite log_nine_quarters_ge cleanly:
```
lemma log_nine_quarters_ge : (0.8109 : ℝ) ≤ Real.log (9 / 4) := by
-- e^{0.8109} = e/e^{0.1891} ≤ 2.7182818286/1.20816 ≤ 2.25
have h01891 : (1.20816 : ℝ) ≤ Real.exp 0.1891 :=
le_trans (by norm_num [Finset.sum_range_succ])
(Real.sum_le_exp_of_nonneg (by norm_num : (0 : ℝ) ≤ 0.1891) 6)
have h1 : Real.exp 0.8109 = Real.exp 1 / Real.exp 0.1891 := by
rw [show (0.8109 : ℝ) = 1 - 0.1891 by norm_num, Real.exp_sub, Real.exp_one]
have h2 : Real.exp 0.8109 ≤ 9 / 4 := by
rw [h1]
calc Real.exp 1 / Real.exp 0.1891
≤ 2.7182818286 / 1.20816 :=
div_le_div₀ Real.exp_one_lt_d9.le h01891 (by norm_num) (by norm_num)
_ ≤ 9 / 4 := by norm_num
have h3 := Real.log_le_log (Real.exp_pos _) h2
rwa [Real.log_exp] at h3
```
div_le_div₀ (hc : 0 ≤ c) (hac : a ≤ c) (hd : 0 < d) (hdb : d ≤ b) : a/b ≤ c/d ✓ — with a := exp 1, b := exp 0.1891, c := 2.7182818286, d := 1.20816: div_le_div₀ (by norm_num : 0 ≤ 2.7182818286) Real.exp_one_lt_d9.le (by norm_num : (0:ℝ) < 1.20816) h01891?? — div_le_div₀'s signature: div_le_div₀ (hc : 0 ≤ c) (hac : a ≤ c) (hd : 0 < d) (hdb : d ≤ b) : a / b ≤ c / d — the args: hc : 0 ≤ c = 2.7182818286 ✓ norm_num; hac : a ≤ c := exp 1 ≤ 2.7182818286 = Real.exp_one_lt_d9.le ✓; hd : 0 < d = 1.20816 ✓ norm_num; hdb : d ≤ b := 1.20816 ≤ exp 0.1891 = h01891 ✓. Then 2.7182818286/1.20816 ≤ 9/4 ⟺ 2.7182818286·4 ≤ 9·1.20816 ⟺ 10.8731273 ≤ 10.87344 ✓ norm_num ✓.
Wait — div_le_div₀ signature order: (hc : 0 ≤ c) (hac : a ≤ c) (hd : 0 < d) (hdb : d ≤ b) — hmm from the earlier grep: `lemma div_le_div₀ (hc : 0 ≤ c) (hac : a ≤ c) (hd : 0 < d) (hdb : d ≤ b) : a / b ≤ c / d` ✓ — so args are (hc, hac, hd, hdb) ✓.
And h3 := Real.log_le_log (Real.exp_pos _) h2 — log_le_log (hx : 0 < x) (hxy : x ≤ y)?? — for log(exp 0.8109) ≤ log(9/4): need `Real.log_le_log (h1 : 0 < exp 0.8109) (h2 : exp 0.8109 ≤ 9/4)` : log(exp 0.8109) ≤ log(9/4) ✓ then rw [Real.log_exp] at h3 : 0.8109 ≤ log(9/4) ✓✓ — the goal of log_nine_quarters_ge : (0.8109 : ℝ) ≤ Real.log (9 / 4) ✓ rwa closes ✓.
Then log_four_ninths_le : log(4/9) = −log(9/4) ≤ −0.8109.
And four_ninths_rpow_sqrt_le with target 0.164:
```
lemma four_ninths_rpow_sqrt_le {x : ℝ} (hx : (2.236 : ℝ) ≤ x) :
(4 / 9 : ℝ) ^ x ≤ (0.164 : ℝ) := by
... h2 : Real.log (4 / 9) * x ≤ (-1.81316 : ℝ) := ...
have h3 : Real.exp (-1.81316) ≤ (0.164 : ℝ) := by
have hsum : (6.12639 : ℝ) ≤ Real.exp 1.81316 := by
calc (6.12639 : ℝ) ≤ ∑ i ∈ Finset.range 7, (1.81316 : ℝ) ^ i / (Nat.factorial i : ℝ) := by
norm_num [Finset.sum_range_succ]
_ ≤ Real.exp 1.81316 := Real.sum_le_exp_of_nonneg (by norm_num) 7
rw [show Real.exp (-1.81316) = 1 / Real.exp 1.81316 by rw [Real.exp_neg, one_div]]
calc 1 / Real.exp 1.81316 ≤ 1 / 6.12639 := one_div_le_one_div_of_le (by norm_num) hsum
_ ≤ 0.164 := by norm_num
...
```
1/6.12639 = 0.1632302 ≤ 0.164 ✓ norm_num ✓.
And the h2's constant: 2.236·(−0.8109) = −1.81316 — h2b : Real.log(4/9)·2.236 ≤ (−0.8109)·2.236 = −1.81316 ✓.
Let me now rewrite these three lemmas cleanly (replace the broken versions). Also fix the remaining errors:
4. **Line 1297 (three_pow_neg identity's rpow_def_of_pos)**: type mismatch with the norm_num-generated positivity proof — `Real.rpow_def_of_pos (by norm_num : (0 : ℝ) < 4 / 9) x` — the elaborated term's type mismatch — hmm — the error shows a giant norm_num proof term — maybe rpow_def_of_pos's signature differs: `Real.rpow_def_of_pos (hx : 0 < x) (y : ℝ) : x ^ y = Real.exp (Real.log x * y)` ✓ — hmm, maybe the issue is rpow_def_of_pos has implicit y and the application order... — the error at 1297:4 "Type mismatch" with the huge term — probably the (by norm_num : (0:ℝ) < 4/9) elaborated to a proof of something else (0 < 4/9 as NNRat division — the norm_num proves it ✓ should be fine). The mismatch is downstream (cascade). Let me look after fixing the others.
5. **Line 1346 (h5's hlog2)**: `Real.log_two_lt_d9.le` has type `log 2 ≤ 0.6931471808` but expected `log 2 ≤ 0.6932` — log_two_lt_d9 gives the d9 bound 0.6931471808 — my 0.6932 ≠ 0.6931471808! Fix: use the d9 constant 0.6931471808 in the h5's assembly (0.6931471808 + 9·0.164 = 0.6931471808+1.476 = 2.1691471808 ≤ 2.28 ✓).
6. **Line 1334 (norm_logDeriv_zeta_le_iimZeta's h3 add_le_add_left)**: "unsolved goals" — add_le_add_left (mul_le_mul_of_nonneg_left hC2 ...) _ — the h3's form: dirichletCX ≤ log2·2^{−2√n} + 3^{−(2√n−2)}·dirichletC2 — h2 gives that; h3 wants dirichletCX ≤ log2·2^{−2√n} + 3^{−(2√n−2)}·... — wait, h3's stated form: `dirichletCX n ≤ Real.log 2 * 2^{−(2√n)} + (3:ℝ)^{−(2√n−2)}` — but h2 gives `... + 3^{−(2√n−2)} * dirichletC2` — the refine h2.trans ?_ expects `log2·2^{−2√n} + 3^{−(2√n−2)}·dirichletC2 ≤ log2·2^{−2√n} + 3^{−(2√n−2)}` — via add_le_add_left (mul_le_mul_of_nonneg_left hC2 (rpow_nonneg) : 3^{−(2√n−2)}·dirichletC2 ≤ 3^{−(2√n−2)}·1) _ — the `_` at the end — add_le_add_left (h : b ≤ c) (a : α) : a + b ≤ a + c ✓ — the trailing `_` should be the `a` = `Real.log 2 * 2^{−(2√n)}` ✓ — hmm, mul_le_mul_of_nonneg_left : a ≤ b → 0 ≤ c → c·a ≤ c·b — with c := 3^{−(2√n−2)}, a := dirichletC2, b := 1: gives 3^{−(2√n−2)}·dirichletC2 ≤ 3^{−(2√n−2)}·1 ✓ — and add_le_add_left that _ ✓. The "unsolved goals" might be a cascade. Let me look after the other fixes.
Let me now rewrite the three problem lemmas (log_nine_quarters_ge, log_four_ninths_le, four_ninths_rpow_sqrt_le) cleanly and fix the remaining spots.
Key realization: `log(9/4) = 0.81093 < 0.811` — my constant was wrong. Rewriting the three certification lemmas with the e/e^{0.1891} tight route and bound 0.8109, plus the remaining fixes.
tool: Edit
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDogLeg.lean",
"old_string": "/-- log(9/4) \u2265 0.811 (via e^{0.811} \u2265 9/4 with e^{0.8} \u2265 2.2254). -/\nlemma log_nine_quarters_ge : (0.811 : \u211d) \u2264 Real.log (9 / 4) := by\n have h08 : (2.2254 : \u211d) \u2264 Real.exp 0.8 :=\n le_trans (by norm_num [Finset.sum_range_succ])\n (Real.sum_le_exp_of_nonneg (by norm_num : (0 : \u211d) \u2264 0.8) 7)\n have h011 : (1.01106 : \u211d) \u2264 Real.exp 0.011 :=\n le_trans (by norm_num [Finset.sum_range_succ])\n (Real.sum_le_exp_of_nonneg (by norm_num : (0 : \u211d) \u2264 0.011) 4)\n have hprod : (9 / 4 : \u211d) \u2264 Real.exp 0.8 * Real.exp 0.011 := by\n calc (9 / 4 : \u211d) = 2.25 := by norm_num\n _ \u2264 2.2254 * 1.01106 := by norm_num\n _ \u2264 Real.exp 0.8 * Real.exp 0.011 :=\n mul_le_mul h08 h011 (by norm_num : (0 : \u211d) \u2264 1.01106) (Real.exp_pos _).le\n have h1 : Real.exp 0.811 = Real.exp 0.8 * Real.exp 0.011 := by\n rw [show (0.811 : \u211d) = 0.8 + 0.011 by norm_num, Real.exp_add]\n rw [\u2190 h1] at hprod\n have h2 := Real.log_le_log (by norm_num : (0 : \u211d) < 9 / 4) hprod\n rwa [Real.log_exp] at h2\n\n/-- log(4/9) \u2264 \u22120.811 (the negation). -/\nlemma log_four_ninths_le : Real.log (4 / 9) \u2264 (-0.811 : \u211d) := by\n have h1 := log_nine_quarters_ge\n have h2 : Real.log (4 / 9) = -Real.log (9 / 4) := by\n rw [show ((4 : \u211d) / 9) = (9 / 4)\u207b\u00b9 by norm_num, Real.log_inv]\n rw [h2]\n linarith [h1]",
"new_string": "/-- log(9/4) \u2265 0.8109 (via e^{0.8109} = e/e^{0.1891} \u2264 2.25, the tight\ne/e^{small} division-by-partial-sum route). -/\nlemma log_nine_quarters_ge : (0.8109 : \u211d) \u2264 Real.log (9 / 4) := by\n have h01891 : (1.20816 : \u211d) \u2264 Real.exp 0.1891 :=\n le_trans (by norm_num [Finset.sum_range_succ])\n (Real.sum_le_exp_of_nonneg (by norm_num : (0 : \u211d) \u2264 0.1891) 6)\n have h1 : Real.exp 0.8109 = Real.exp 1 / Real.exp 0.1891 := by\n rw [show (0.8109 : \u211d) = 1 - 0.1891 by norm_num, Real.exp_sub, Real.exp_one]\n have h2 : Real.exp 0.8109 \u2264 9 / 4 := by\n rw [h1]\n calc Real.exp 1 / Real.exp 0.1891\n \u2264 2.7182818286 / 1.20816 :=\n div_le_div\u2080 (by norm_num) Real.exp_one_lt_d9.le (by norm_num) h01891\n _ \u2264 9 / 4 := by norm_num\n have h3 := Real.log_le_log (Real.exp_pos _) h2\n rwa [Real.log_exp] at h3\n\n/-- log(4/9) \u2264 \u22120.8109 (the negation). -/\nlemma log_four_ninths_le : Real.log (4 / 9) \u2264 (-0.8109 : \u211d) := by\n have h1 := log_nine_quarters_ge\n have h2 : Real.log (4 / 9) = -Real.log (9 / 4) := by\n rw [show ((4 : \u211d) / 9) = (9 / 4)\u207b\u00b9 by norm_num, Real.log_inv]\n rw [h2]\n linarith [h1]"
}
tool: Edit
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDogLeg.lean",
"old_string": "/-- The certified (4/9)^{\u221an} \u2264 0.17631 for \u221an \u2265 2.236. -/\nlemma four_ninths_rpow_sqrt_le {x : \u211d} (hx : (2.236 : \u211d) \u2264 x) :\n (4 / 9 : \u211d) ^ x \u2264 (0.17631 : \u211d) := by\n have hlog49 := log_four_ninths_le\n have hlogneg : Real.log (4 / 9) < 0 :=\n Real.log_neg (by norm_num : (0 : \u211d) < 4 / 9) (by norm_num : (4 / 9 : \u211d) < 1)\n have h1 : (4 / 9 : \u211d) ^ x = Real.exp (Real.log (4 / 9) * x) :=\n Real.rpow_def_of_pos (by norm_num : (0 : \u211d) < 4 / 9) x\n rw [h1]\n have h2 : Real.log (4 / 9) * x \u2264 (-1.8135 : \u211d) := by\n have h2a : Real.log (4 / 9) * x \u2264 Real.log (4 / 9) * 2.236 :=\n mul_le_mul_of_nonpos_left hx hlogneg.le\n have h2b : Real.log (4 / 9) * 2.236 \u2264 (-0.811) * 2.236 :=\n mul_le_mul_of_nonneg_right hlog49 (by norm_num)\n calc Real.log (4 / 9) * x \u2264 Real.log (4 / 9) * 2.236 := h2a\n _ \u2264 (-0.811) * 2.236 := h2b\n _ \u2264 -1.8135 := by norm_num\n have h3 : Real.exp (-1.8135) \u2264 (0.17631 : \u211d) := by\n have hsum : (5.6721 : \u211d) \u2264 Real.exp 1.8135 := by\n calc (5.6721 : \u211d) \u2264 \u2211 i \u2208 Finset.range 7, (1.8135 : \u211d) ^ i / (Nat.factorial i : \u211d) := by\n norm_num [Finset.sum_range_succ]\n _ \u2264 Real.exp 1.8135 :=\n Real.sum_le_exp_of_nonneg (by norm_num : (0 : \u211d) \u2264 1.8135) 7\n rw [show Real.exp (-1.8135) = 1 / Real.exp 1.8135 by\n rw [Real.exp_neg, one_div]]\n calc 1 / Real.exp 1.8135 \u2264 1 / 5.6721 :=\n one_div_le_one_div_of_le (by positivity : (0 : \u211d) < 5.6721) hsum\n _ \u2264 0.17631 := by norm_num\n calc Real.exp (Real.log (4 / 9) * x) \u2264 Real.exp (-1.8135) :=\n Real.exp_le_exp.mpr h2\n _ \u2264 0.17631 := h3",
"new_string": "/-- The certified (4/9)^{\u221an} \u2264 0.164 for \u221an \u2265 2.236. -/\nlemma four_ninths_rpow_sqrt_le {x : \u211d} (hx : (2.236 : \u211d) \u2264 x) :\n (4 / 9 : \u211d) ^ x \u2264 (0.164 : \u211d) := by\n have hlog49 := log_four_ninths_le\n have hlogneg : Real.log (4 / 9) < 0 :=\n Real.log_neg (by norm_num : (0 : \u211d) < 4 / 9) (by norm_num : (4 / 9 : \u211d) < 1)\n have h1 : (4 / 9 : \u211d) ^ x = Real.exp (Real.log (4 / 9) * x) :=\n Real.rpow_def_of_pos (by norm_num : (0 : \u211d) < 4 / 9) x\n rw [h1]\n have h2 : Real.log (4 / 9) * x \u2264 (-1.81316 : \u211d) := by\n have h2a : Real.log (4 / 9) * x \u2264 Real.log (4 / 9) * 2.236 :=\n mul_le_mul_of_nonpos_left hx hlogneg.le\n have h2b : Real.log (4 / 9) * 2.236 \u2264 (-0.8109) * 2.236 :=\n mul_le_mul_of_nonneg_right hlog49 (by norm_num)\n calc Real.log (4 / 9) * x \u2264 Real.log (4 / 9) * 2.236 := h2a\n _ \u2264 (-0.8109) * 2.236 := h2b\n _ \u2264 -1.81316 := by norm_num\n have h3 : Real.exp (-1.81316) \u2264 (0.164 : \u211d) := by\n have hsum : (6.12639 : \u211d) \u2264 Real.exp 1.81316 := by\n calc (6.12639 : \u211d) \u2264 \u2211 i \u2208 Finset.range 7, (1.81316 : \u211d) ^ i / (Nat.factorial i : \u211d) := by\n norm_num [Finset.sum_range_succ]\n _ \u2264 Real.exp 1.81316 :=\n Real.sum_le_exp_of_nonneg (by norm_num : (0 : \u211d) \u2264 1.81316) 7\n rw [show Real.exp (-1.81316) = 1 / Real.exp 1.81316 by\n rw [Real.exp_neg, one_div]]\n calc 1 / Real.exp 1.81316 \u2264 1 / 6.12639 :=\n one_div_le_one_div_of_le (by norm_num : (0 : \u211d) < 6.12639) hsum\n _ \u2264 0.164 := by norm_num\n calc Real.exp (Real.log (4 / 9) * x) \u2264 Real.exp (-1.81316) :=\n Real.exp_le_exp.mpr h2\n _ \u2264 0.164 := h3"
}
tool: Edit ok
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDogLeg.lean",
"old_string": " have h49 := four_ninths_rpow_sqrt_le hsqrt5\n have h3 : dirichletCX n \u2264 Real.log 2 * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d))) +\n (3 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) := by\n refine h2.trans ?_\n exact add_le_add_left (mul_le_mul_of_nonneg_left hC2\n (Real.rpow_nonneg (by norm_num) _)) _",
"new_string": " have h49 := four_ninths_rpow_sqrt_le hsqrt5\n have h3 : dirichletCX n \u2264 Real.log 2 * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d))) +\n (3 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) := by\n refine h2.trans ?_\n exact add_le_add_left (mul_le_mul_of_nonneg_left hC2\n (Real.rpow_nonneg (by norm_num) _)) (Real.log 2 * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d))))"
}
result 2026-08-26 09:36:57Z → 2026-08-26 09:36:57Z
{
"filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDogLeg.lean",
"oldString": " have h49 := four_ninths_rpow_sqrt_le hsqrt5\n have h3 : dirichletCX n \u2264 Real.log 2 * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d))) +\n (3 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) := by\n refine h2.trans ?_\n exact add_le_add_left (mul_le_mul_of_nonneg_left hC2\n (Real.rpow_nonneg (by norm_num) _)) _",
"newString": " have h49 := four_ninths_rpow_sqrt_le hsqrt5\n have h3 : dirichletCX n \u2264 Real.log 2 * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d))) +\n (3 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) := by\n refine h2.trans ?_\n exact add_le_add_left (mul_le_mul_of_nonneg_left hC2\n (Real.rpow_nonneg (by norm_num) _)) (Real.log 2 * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d))))",
"originalFile": "/-\nNguyenRH1/LiDogLeg.lean \u2014 ii\u2032-6-DL-1 (D-074, session 040): the zero-free\ndog-leg deformation of the Lagarias horizontal right tail.\n\nTHE CONTENT (D-074 \u00a73.1\u20133.2): on the dog-leg rectangle [3, X_R]\u00d7[T, U]\n(T > 0), the Lagarias integrand Jlag n s = (s/(s\u22121))\u207f\u22121 \u00b7 (\u2212\u03b6\u2032/\u03b6(s)) is\nholomorphic UNCONDITIONALLY (s \u2260 1 since im > 0; \u03b6 s \u2260 0 for re s \u2265 3 > 1\nby Mathlib's Euler-product nonvanishing `riemannZeta_ne_zero_of_one_lt_re`\n\u2014 NO perimeter hypothesis, no zero-avoidance at U). Cauchy's theorem\n(`HolomorphicOn.vanishesOnRectangle`) then gives the EXACT deformation\nidentity\n H(3\u2192X_R, T) = H(3\u2192X_R, U) \u2212 V(X_R, T\u2192U) + V(3, T\u2192U)\n(the upper right tail = the high horizontal \u2212 the right drop + the left\nlift), plus the Jlag conjugation identity for the lower-side transfer.\n\nThis is the repair of Finding F-D (D-072): the broken low-path envelope\nis ABANDONED (not bounded) \u2014 the magnitude bound comes later from the\nthree dog-leg pieces, all in the unconditionally zero-free region.\n-/\nimport Mathlib\nimport NguyenRH1.LiSides\nimport NguyenRH1.LiTightR\nimport NguyenRH1.LiBasePoints\n\nopen Zeta23 Complex Filter Topology\nopen scoped Nat\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. Dog-leg analyticity (D-074 \u00a73.1; no perimeter) -/\n\n/-- The dog-leg corners (same real-part/imaginary-part form as rectZ/rectW). -/\ndef dogZ (T : \u211d) : \u2102 := ((3 : \u211d) : \u2102) + (T : \u211d) * Complex.I\ndef dogW (XR U : \u211d) : \u2102 := ((XR : \u211d) : \u2102) + (U : \u211d) * Complex.I\n\nlemma dogZ_re (T : \u211d) : (dogZ T).re = 3 := by simp [dogZ]\nlemma dogZ_im (T : \u211d) : (dogZ T).im = T := by simp [dogZ]\nlemma dogW_re (XR U : \u211d) : (dogW XR U).re = XR := by simp [dogW]\nlemma dogW_im (XR U : \u211d) : (dogW XR U).im = U := by simp [dogW]\n\n/-- Jlag is differentiable at every point with 3 \u2264 re, 0 < im:\n\u03b6 is zero-free for 1 < re (Mathlib `riemannZeta_ne_zero_of_one_lt_re`,\nUNCONDITIONAL \u2014 the Euler-product region) and s \u2260 1 (im \u2260 0).\nNO perimeter hypothesis. -/\ntheorem Jlag_differentiableAt_dogleg {n : \u2115} {s : \u2102}\n (hre : 3 \u2264 s.re) (him : 0 < s.im) :\n DifferentiableAt \u2102 (Jlag n) s := by\n apply Jlag_differentiableAt\n \u00b7 rintro rfl\n simp at him\n \u00b7 exact riemannZeta_ne_zero_of_one_lt_re (by linarith)\n\n/-- Jlag is holomorphic on the whole dog-leg rectangle\n[3, X_R]\u00d7[T, U] (T > 0). -/\ntheorem holomorphicOn_Jlag_dogleg {n : \u2115} {T U XR : \u211d}\n (hT : 0 < T) (hTU : T \u2264 U) (hXR : 3 \u2264 XR) :\n HolomorphicOn (Jlag n) (Rectangle (dogZ T) (dogW XR U)) := by\n intro s hs\n rw [Rectangle, Complex.mem_reProdIm, dogZ_re, dogW_re, dogZ_im, dogW_im] at hs\n rw [Set.uIcc_of_le hXR, Set.uIcc_of_le hTU] at hs\n exact (Jlag_differentiableAt_dogleg hs.1.1 (by linarith [hs.2.1])).differentiableWithinAt\n\n/-- **The dog-leg rectangle integral vanishes** (Cauchy; the region is\nunconditionally zero-free \u2014 the residue sum is EMPTY, no perimeter). -/\ntheorem rectangleIntegral_Jlag_dogleg_eq_zero {n : \u2115} {T U XR : \u211d}\n (hT : 0 < T) (hTU : T \u2264 U) (hXR : 3 \u2264 XR) :\n RectangleIntegral (Jlag n) (dogZ T) (dogW XR U) = 0 :=\n (holomorphicOn_Jlag_dogleg hT hTU hXR).vanishesOnRectangle subset_rfl\n\n/-- The (2\u03c0i)\u207b\u00b9-normalized form (API symmetry with rectInt'_Jlag). -/\ntheorem rectangleIntegral'_Jlag_dogleg_eq_zero {n : \u2115} {T U XR : \u211d}\n (hT : 0 < T) (hTU : T \u2264 U) (hXR : 3 \u2264 XR) :\n RectangleIntegral' (Jlag n) (dogZ T) (dogW XR U) = 0 := by\n rw [RectangleIntegral', rectangleIntegral_Jlag_dogleg_eq_zero hT hTU hXR,\n smul_zero]\n\n/-- **THE EXACT DOG-LEG DEFORMATION IDENTITY** (D-074 \u00a73.2 (\u2605), the\ncapstone for ii\u2032-6-c): the low right-horizontal equals the high\nhorizontal minus the right drop plus the left lift. Orientations: all\nH-integrals left-to-right, all V-integrals upward (the main contour's\ntop side is their reversal, handled at the fold site). -/\ntheorem upper_right_horizontal_eq_dogleg {n : \u2115} {T U XR : \u211d}\n (hT : 0 < T) (hTU : T \u2264 U) (hXR : 3 \u2264 XR) :\n HIntegral (Jlag n) 3 XR T =\n HIntegral (Jlag n) 3 XR U - VIntegral (Jlag n) XR T U +\n VIntegral (Jlag n) 3 T U := by\n have h0 := rectangleIntegral_Jlag_dogleg_eq_zero (n := n) hT hTU hXR\n unfold RectangleIntegral at h0\n rw [dogZ_re, dogZ_im, dogW_re, dogW_im] at h0\n linear_combination h0\n\n/-! ## 2. The conjugation identity (for the lower-side transfer, DL-5) -/\n\n/-- kFun is conjugation-symmetric (real-coefficient rational function). -/\ntheorem kFun_conj (n : \u2115) (s : \u2102) :\n kFun n ((starRingEnd \u2102) s) = (starRingEnd \u2102) (kFun n s) := by\n unfold kFun\n simp [map_sub, map_pow, map_one]\n\n/-- **Jlag is conjugation-symmetric** (from `riemannZeta_conj` +\n`iteratedDeriv_riemannZeta_conj`): Jlag n (s\u0304) = conj (Jlag n s).\nNeeded for the lower-horizontal transfer (DL-5). -/\ntheorem Jlag_conj (n : \u2115) {s : \u2102} (hs : s \u2260 1) :\n Jlag n ((starRingEnd \u2102) s) = (starRingEnd \u2102) (Jlag n s) := by\n have h1 : deriv riemannZeta ((starRingEnd \u2102) s) =\n (starRingEnd \u2102) (deriv riemannZeta s) := by\n have h := iteratedDeriv_riemannZeta_conj 1 hs\n rwa [iteratedDeriv_one] at h\n unfold Jlag\n rw [kFun_conj, _root_.riemannZeta_conj, h1]\n simp only [map_mul, map_neg, map_div\u2080]\n\n/-! ## 3. The left-lift bound (DL-2, D-074 \u00a73.3 V_left) -/\n\n/-- **Kernel on the lift**: \u2016kFun n (3+it)\u2016 \u2264 e^{5/2}+1 for n \u2264 t\u00b2\n(D-074 \u00a76: |(3+it)/(2+it)|\u00b2 = (9+t\u00b2)/(4+t\u00b2) = 1 + 5/(4+t\u00b2), whose n-th\npower is \u2264 e^{5n/(2(4+t\u00b2))} \u2264 e^{5/2}). -/\ntheorem kFun_three_add_it_norm_le_exp_five_halves_add_one {n : \u2115} {t : \u211d}\n (hT : (n : \u211d) \u2264 t ^ 2) :\n \u2016kFun n ((3 : \u211d) + t * Complex.I)\u2016 \u2264 Real.exp (5 / 2) + 1 := by\n rcases Nat.eq_zero_or_pos n with hn | hn\n \u00b7 subst hn\n simp only [kFun, pow_zero, sub_self, norm_zero]\n positivity\n \u00b7 have hnR : (1 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n have ht2 : (0 : \u211d) < 4 + t ^ 2 := by positivity\n have hn4t2 : (n : \u211d) \u2264 4 + t ^ 2 := by linarith [hT]\n have hQpos : (0 : \u211d) \u2264 (9 + t ^ 2) / (4 + t ^ 2) := by positivity\n have hQle : (9 + t ^ 2) / (4 + t ^ 2) \u2264 Real.exp (5 / (n : \u211d)) := by\n have h1 : (9 + t ^ 2) / (4 + t ^ 2) = 1 + 5 / (4 + t ^ 2) := by\n field_simp [ht2.ne']\n ring\n rw [h1]\n have h2 : 5 / (4 + t ^ 2) \u2264 5 / (n : \u211d) :=\n (div_le_div_iff_of_pos_left (by norm_num) ht2 (by positivity)).mpr hn4t2\n have h3 := Real.add_one_le_exp (5 / (n : \u211d))\n linarith\n have hQn : ((9 + t ^ 2) / (4 + t ^ 2)) ^ n \u2264 Real.exp 5 := by\n calc ((9 + t ^ 2) / (4 + t ^ 2)) ^ n \u2264 (Real.exp (5 / (n : \u211d))) ^ n :=\n pow_le_pow_left\u2080 hQpos hQle n\n _ = Real.exp 5 := by\n rw [\u2190 Real.exp_nat_mul]\n congr 1\n have hn0 : (n : \u211d) \u2260 0 := by exact_mod_cast hn.ne'\n field_simp [hn0]\n have hns3 : Complex.normSq ((3 : \u211d) + t * Complex.I) = 9 + t ^ 2 := by\n simp [Complex.normSq_apply]\n ring\n have hns2 : Complex.normSq ((2 : \u211d) + t * Complex.I) = 4 + t ^ 2 := by\n simp [Complex.normSq_apply]\n ring\n have hnormA : \u2016((3 : \u211d) + t * Complex.I)\u2016 = Real.sqrt (9 + t ^ 2) := by\n have h1 : \u2016((3 : \u211d) + t * Complex.I)\u2016 =\n Real.sqrt (Complex.normSq ((3 : \u211d) + t * Complex.I)) := by\n rw [Complex.normSq_eq_norm_sq, Real.sqrt_sq (norm_nonneg _)]\n rw [h1, hns3]\n have hnormB : \u2016((2 : \u211d) + t * Complex.I)\u2016 = Real.sqrt (4 + t ^ 2) := by\n have h1 : \u2016((2 : \u211d) + t * Complex.I)\u2016 =\n Real.sqrt (Complex.normSq ((2 : \u211d) + t * Complex.I)) := by\n rw [Complex.normSq_eq_norm_sq, Real.sqrt_sq (norm_nonneg _)]\n rw [h1, hns2]\n have hnorm : \u2016((3 : \u211d) + t * Complex.I) / ((2 : \u211d) + t * Complex.I)\u2016 =\n Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2)) := by\n rw [norm_div, hnormA, hnormB,\n \u2190 Real.sqrt_div (by positivity : (0 : \u211d) \u2264 9 + t ^ 2)]\n have hs1 : ((3 : \u211d) + t * Complex.I) - 1 = (2 : \u211d) + t * Complex.I := by\n push_cast\n ring\n unfold kFun\n rw [hs1]\n calc \u2016(((3 : \u211d) + t * Complex.I) / ((2 : \u211d) + t * Complex.I)) ^ n - 1\u2016\n \u2264 \u2016(((3 : \u211d) + t * Complex.I) / ((2 : \u211d) + t * Complex.I)) ^ n\u2016 + \u2016(1 : \u2102)\u2016 :=\n norm_sub_le _ _\n _ = (Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n + 1 := by\n rw [norm_pow, hnorm, norm_one]\n _ \u2264 Real.exp (5 / 2) + 1 := by\n have h4 : (Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n \u2264 Real.exp (5 / 2) := by\n have hx0 : (0 : \u211d) \u2264 Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2)) :=\n Real.sqrt_nonneg _\n have hx : (0 : \u211d) \u2264 (Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n :=\n pow_nonneg hx0 n\n have h5 : ((Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n) ^ 2 \u2264 Real.exp 5 := by\n have e : ((Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n) ^ 2 =\n ((9 + t ^ 2) / (4 + t ^ 2)) ^ n := by\n rw [\u2190 pow_mul, mul_comm n 2, pow_mul, Real.sq_sqrt hQpos]\n rw [e]\n exact hQn\n have h8 : (Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n =\n Real.sqrt (((Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n) ^ 2) := by\n rw [Real.sqrt_sq hx]\n rw [h8]\n calc Real.sqrt (((Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n) ^ 2)\n \u2264 Real.sqrt (Real.exp 5) := Real.sqrt_le_sqrt h5\n _ = Real.exp (5 / 2) := (Real.exp_half 5).symm\n linarith [h4]\n\n/-- The Dirichlet majorant at s = 3 (summable since 3 > 1). -/\ndef dirichletC3 : \u211d :=\n \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (3 : \u2102) n\u2016\n\n/-- Termwise 3-vs-2 comparison for the \u039b L-series: \u039b(n)/n\u00b3 \u2264 (1/2)\u00b7\u039b(n)/n\u00b2. -/\nlemma norm_term_vonMangoldt_three_le_half (n : \u2115) :\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (3 : \u2102) n\u2016 \u2264\n (1 / 2) * \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016 := by\n have h3re : ((3 : \u2102).re) = 3 := rfl\n have h2re : ((2 : \u2102).re) = 2 := rfl\n simp only [LSeries.norm_term_eq, h3re, h2re]\n split\n \u00b7 norm_num\n \u00b7 next hn =>\n rcases eq_or_ne n 1 with rfl | hn1\n \u00b7 simp [ArithmeticFunction.vonMangoldt_apply_one]\n \u00b7 have hn2 : 2 \u2264 n := by omega\n have h\u039b : \u2016(ArithmeticFunction.vonMangoldt n : \u2102)\u2016 =\n ArithmeticFunction.vonMangoldt n :=\n Complex.norm_of_nonneg ArithmeticFunction.vonMangoldt_nonneg\n rw [h\u039b]\n have e : ArithmeticFunction.vonMangoldt n / (n : \u211d) ^ (3 : \u211d) =\n (1 / (n : \u211d)) * (ArithmeticFunction.vonMangoldt n / (n : \u211d) ^ (2 : \u211d)) := by\n rw [show (3 : \u211d) = 2 + 1 by norm_num,\n Real.rpow_add (by positivity : (0 : \u211d) < (n : \u211d)), Real.rpow_one]\n field_simp [show (n : \u211d) \u2260 0 by positivity]\n have h12 : (1 : \u211d) / (n : \u211d) \u2264 1 / 2 :=\n one_div_le_one_div_of_le (by norm_num : (0 : \u211d) < 2)\n (by exact_mod_cast hn2 : (2 : \u211d) \u2264 (n : \u211d))\n have hpos : (0 : \u211d) \u2264 ArithmeticFunction.vonMangoldt n / (n : \u211d) ^ (2 : \u211d) :=\n div_nonneg ArithmeticFunction.vonMangoldt_nonneg\n (Real.rpow_nonneg (by positivity : (0 : \u211d) \u2264 (n : \u211d)) _)\n calc ArithmeticFunction.vonMangoldt n / (n : \u211d) ^ (3 : \u211d)\n = (1 / (n : \u211d)) * (ArithmeticFunction.vonMangoldt n / (n : \u211d) ^ (2 : \u211d)) := e\n _ \u2264 (1 / 2) * (ArithmeticFunction.vonMangoldt n / (n : \u211d) ^ (2 : \u211d)) :=\n mul_le_mul_of_nonneg_right h12 hpos\n\n/-- dirichletC3 \u2264 1/2 (the termwise comparison + dirichletC2 \u2264 1) \u2014\nthe certified C_zeta3 = 0.5 of D-074 \u00a74. (A tighter 0.17 build is\npossible via a 6-prime partial sum + antitone-integral tail; the fold\nis indifferent to the constant, so the cheap certified 0.5 is charged.) -/\nlemma dirichletC3_le_half : dirichletC3 \u2264 1 / 2 := by\n have hsum3 : Summable (fun n : \u2115 =>\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (3 : \u2102) n\u2016) := by\n rw [summable_norm_iff]\n exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)\n have hsum2 : Summable (fun n : \u2115 =>\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016) := by\n rw [summable_norm_iff]\n exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)\n calc dirichletC3\n = \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (3 : \u2102) n\u2016 := rfl\n _ \u2264 \u2211' n : \u2115, (1 / 2) *\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016 :=\n Summable.tsum_le_tsum (fun n => norm_term_vonMangoldt_three_le_half n) hsum3\n (hsum2.mul_left (1 / 2))\n _ = (1 / 2) * dirichletC2 := by rw [dirichletC2, tsum_mul_left]\n _ \u2264 1 / 2 := by linarith [dirichletC2_le_one]\n\n/-- \u2016\u03b6\u2032/\u03b6 s\u2016 \u2264 dirichletC3 for re s \u2265 3 (the s = 3 clone of the\nDirichlet-series majorant). -/\nlemma norm_logDeriv_zeta_le_dirichletC3 {s : \u2102} (hs : 3 \u2264 s.re) :\n \u2016logDeriv riemannZeta s\u2016 \u2264 dirichletC3 := by\n have hs1 : (1 : \u211d) < s.re := by linarith\n have h1 : -logDeriv riemannZeta s\n = LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s := by\n have h2 := ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div hs1\n rw [logDeriv, Pi.div_apply, h2]\n ring\n have hsum3 : Summable (fun n : \u2115 =>\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (3 : \u2102) n\u2016) := by\n rw [summable_norm_iff]\n exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)\n have hsumS : Summable (fun n : \u2115 =>\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016) := by\n rw [summable_norm_iff]\n exact ArithmeticFunction.LSeriesSummable_vonMangoldt hs1\n have hle : \u2016LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s\u2016\n \u2264 dirichletC3 := by\n show \u2016\u2211' n : \u2115, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016 \u2264 _\n calc \u2016\u2211' n : \u2115, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016\n \u2264 \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016 :=\n norm_tsum_le_tsum_norm hsumS\n _ \u2264 \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (3 : \u2102) n\u2016 :=\n Summable.tsum_le_tsum (fun n => LSeries.norm_term_le_of_re_le_re _ (by\n simp\n exact hs) n) hsumS hsum3\n _ = dirichletC3 := rfl\n calc \u2016logDeriv riemannZeta s\u2016\n = \u2016LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s\u2016 := by\n rw [\u2190 h1, norm_neg]\n _ \u2264 dirichletC3 := hle\n\n/-- \u2016\u03b6\u2032/\u03b6 s\u2016 \u2264 1/2 for re s \u2265 3 (the charged C_zeta3 = 0.5). -/\nlemma norm_logDeriv_zeta_le_half {s : \u2102} (hs : 3 \u2264 s.re) :\n \u2016logDeriv riemannZeta s\u2016 \u2264 1 / 2 :=\n (norm_logDeriv_zeta_le_dirichletC3 hs).trans dirichletC3_le_half\n\n/-- **The left-lift bound** (D-074 \u00a73.3 V_left): for 0 < T \u2264 U and\nn \u2264 T\u00b2, \u2016VIntegral (Jlag n) 3 T U\u2016 \u2264 (U \u2212 T)\u00b7(e^{5/2}+1)/2. The kernel\n\u2264 e^{5/2}+1 (the 1+5/(4+t\u00b2) computation), the zeta factor \u2264 1/2\n(certified, no perimeter). -/\ntheorem vIntegral_Jlag_three_norm_le {n : \u2115} {T U : \u211d}\n (hT0 : (0 : \u211d) < T) (hTU : T \u2264 U) (hTn : (n : \u211d) \u2264 T ^ 2) :\n \u2016VIntegral (Jlag n) 3 T U\u2016 \u2264 (U - T) * (Real.exp (5 / 2) + 1) / 2 := by\n have hnorm : \u2016VIntegral (Jlag n) 3 T U\u2016 =\n \u2016\u222b t in T..U, Jlag n ((3 : \u211d) + t * Complex.I)\u2016 := by\n unfold VIntegral\n rw [norm_smul, Complex.norm_I, one_mul]\n rw [hnorm]\n have hbound : \u2200 t \u2208 Set.Ioc T U,\n \u2016Jlag n ((3 : \u211d) + t * Complex.I)\u2016 \u2264 (Real.exp (5 / 2) + 1) * (1 / 2) := by\n intro t ht\n have htT : T < t := ht.1\n have ht2 : (n : \u211d) \u2264 t ^ 2 := by nlinarith [hTn, hT0]\n have hre : (3 : \u211d) \u2264 ((3 : \u211d) + t * Complex.I).re := by simp\n have h1 := kFun_three_add_it_norm_le_exp_five_halves_add_one ht2\n have h2 := norm_logDeriv_zeta_le_half (s := (3 : \u211d) + t * Complex.I) hre\n have hnorm3 : \u2016Jlag n ((3 : \u211d) + t * Complex.I)\u2016 =\n \u2016kFun n ((3 : \u211d) + t * Complex.I)\u2016 *\n \u2016logDeriv riemannZeta ((3 : \u211d) + t * Complex.I)\u2016 := by\n show \u2016kFun n ((3 : \u211d) + t * Complex.I) *\n (-logDeriv riemannZeta ((3 : \u211d) + t * Complex.I))\u2016 = _\n rw [norm_mul, norm_neg]\n rw [hnorm3]\n exact mul_le_mul h1 h2 (norm_nonneg _) (by positivity)\n have hint : \u2016\u222b t in T..U, Jlag n ((3 : \u211d) + t * Complex.I)\u2016 \u2264\n ((Real.exp (5 / 2) + 1) * (1 / 2)) * |U - T| := by\n apply intervalIntegral.norm_integral_le_of_norm_le_const\n intro t ht\n rw [Set.uIoc_of_le hTU] at ht\n exact hbound t ht\n have habs : |U - T| = U - T := abs_of_nonneg (by linarith)\n rw [habs] at hint\n calc \u2016\u222b t in T..U, Jlag n ((3 : \u211d) + t * Complex.I)\u2016\n \u2264 ((Real.exp (5 / 2) + 1) * (1 / 2)) * (U - T) := hint\n _ = (U - T) * (Real.exp (5 / 2) + 1) / 2 := by ring\n\n/-! ## 4. The high-horizontal stepping (DL-3, D-074 \u00a77 + D-073 \u00a74) -/\n\n/-- Termwise \u03c3-vs-2 comparison for the \u039b L-series (the (6.10) halving):\n\u039b(m)/m^\u03c3 \u2264 2^{\u2212(\u03c3\u22122)}\u00b7\u039b(m)/m\u00b2 for \u03c3 \u2265 2. -/\nlemma norm_term_vonMangoldt_le_two_pow {\u03c3 t : \u211d} (h\u03c3 : 2 \u2264 \u03c3) (m : \u2115) :\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n ((\u03c3 : \u211d) + t * Complex.I) m\u2016 \u2264\n (2 : \u211d) ^ (-(\u03c3 - 2)) * \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) m\u2016 := by\n have h\u03c3re : ((\u03c3 : \u211d) + t * Complex.I).re = \u03c3 := by simp\n have h2re : ((2 : \u2102).re) = 2 := rfl\n simp only [LSeries.norm_term_eq, h\u03c3re, h2re]\n split\n \u00b7 norm_num\n \u00b7 next hm =>\n have h\u039b : \u2016(ArithmeticFunction.vonMangoldt m : \u2102)\u2016 =\n ArithmeticFunction.vonMangoldt m :=\n Complex.norm_of_nonneg ArithmeticFunction.vonMangoldt_nonneg\n rw [h\u039b]\n rcases eq_or_ne m 1 with rfl | hm1\n \u00b7 simp [ArithmeticFunction.vonMangoldt_apply_one]\n \u00b7 have hm2 : 2 \u2264 m := by omega\n have e : ArithmeticFunction.vonMangoldt m / (m : \u211d) ^ \u03c3 =\n (1 / (m : \u211d) ^ (\u03c3 - 2)) * (ArithmeticFunction.vonMangoldt m / (m : \u211d) ^ (2 : \u211d)) := by\n rw [show (\u03c3 : \u211d) = (\u03c3 - 2) + 2 by ring,\n Real.rpow_add (by positivity : (0 : \u211d) < (m : \u211d))]\n field_simp [show (m : \u211d) \u2260 0 by positivity]\n ring_nf\n rw [e]\n have hle : (1 : \u211d) / (m : \u211d) ^ (\u03c3 - 2) \u2264 (2 : \u211d) ^ (-(\u03c3 - 2)) := by\n rw [Real.rpow_neg (by norm_num : (0 : \u211d) \u2264 2), \u2190 one_div]\n apply one_div_le_one_div_of_le (Real.rpow_pos_of_pos (by norm_num : (0 : \u211d) < 2) _)\n exact Real.rpow_le_rpow (by norm_num : (0 : \u211d) \u2264 2)\n (by exact_mod_cast hm2 : (2 : \u211d) \u2264 (m : \u211d)) (by linarith : (0 : \u211d) \u2264 \u03c3 - 2)\n have hpos : (0 : \u211d) \u2264 ArithmeticFunction.vonMangoldt m / (m : \u211d) ^ (2 : \u211d) :=\n div_nonneg ArithmeticFunction.vonMangoldt_nonneg\n (Real.rpow_nonneg (by positivity : (0 : \u211d) \u2264 (m : \u211d)) _)\n exact mul_le_mul_of_nonneg_right hle hpos\n\n/-- \u2016\u03b6\u2032/\u03b6(\u03c3+it)\u2016 \u2264 2^{\u2212(\u03c3\u22122)}\u00b7dirichletC2 for \u03c3 \u2265 2 (the (6.10)\nhalving in LSeries form; dirichletC2 \u2264 1 makes the tail free). -/\nlemma norm_logDeriv_zeta_le_two_pow {\u03c3 t : \u211d} (h\u03c3 : 2 \u2264 \u03c3) :\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + t * Complex.I)\u2016 \u2264\n (2 : \u211d) ^ (-(\u03c3 - 2)) * dirichletC2 := by\n have hs1 : (1 : \u211d) < ((\u03c3 : \u211d) + t * Complex.I).re := by simp; linarith\n have h1 : -logDeriv riemannZeta ((\u03c3 : \u211d) + t * Complex.I)\n = LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) ((\u03c3 : \u211d) + t * Complex.I) := by\n have h2 := ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div hs1\n rw [logDeriv, Pi.div_apply, h2]\n ring\n have hsum2 : Summable (fun n : \u2115 =>\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016) := by\n rw [summable_norm_iff]\n exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)\n have hsumS : Summable (fun n : \u2115 =>\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n ((\u03c3 : \u211d) + t * Complex.I) n\u2016) := by\n rw [summable_norm_iff]\n exact ArithmeticFunction.LSeriesSummable_vonMangoldt hs1\n have hle : \u2016LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n ((\u03c3 : \u211d) + t * Complex.I)\u2016 \u2264 (2 : \u211d) ^ (-(\u03c3 - 2)) * dirichletC2 := by\n show \u2016\u2211' n : \u2115, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n ((\u03c3 : \u211d) + t * Complex.I) n\u2016 \u2264 _\n calc \u2016\u2211' n : \u2115, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n ((\u03c3 : \u211d) + t * Complex.I) n\u2016\n \u2264 \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n ((\u03c3 : \u211d) + t * Complex.I) n\u2016 :=\n norm_tsum_le_tsum_norm hsumS\n _ \u2264 \u2211' n : \u2115, (2 : \u211d) ^ (-(\u03c3 - 2)) *\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016 :=\n Summable.tsum_le_tsum (fun n => norm_term_vonMangoldt_le_two_pow h\u03c3 n) hsumS\n (hsum2.mul_left _)\n _ = (2 : \u211d) ^ (-(\u03c3 - 2)) * dirichletC2 := by rw [dirichletC2, tsum_mul_left]\n calc \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + t * Complex.I)\u2016\n = \u2016LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n ((\u03c3 : \u211d) + t * Complex.I)\u2016 := by\n rw [\u2190 h1, norm_neg]\n _ \u2264 (2 : \u211d) ^ (-(\u03c3 - 2)) * dirichletC2 := hle\n\n/-- **Kernel envelope** (D-074 \u00a77, the single-exponential form that\nreplaces the unit-step geometric series): \u2016(1+1/((\u03c3\u22121)+iU))\u207f\u2016 \u2264\ne^{(4/9)\u03c3} for \u03c3 \u2265 3 and n \u2264 (4/9)U\u00b2. From the (6.11) core\n\u20161+1/s\u2016 \u2264 1+(re s+1)/normSq s \u2264 1+\u03c3/U\u00b2. -/\ntheorem one_add_div_pow_norm_le_exp_four_ninths {n : \u2115} {\u03c3 U : \u211d}\n (h\u03c3 : 3 \u2264 \u03c3) (hU : 0 < U) (hnU : (n : \u211d) \u2264 (4 / 9) * U ^ 2) :\n \u2016(1 + 1/(((\u03c3 : \u211d) - 1) + U * Complex.I))\u2016 ^ n \u2264 Real.exp ((4 / 9) * \u03c3) := by\n have hs0 : (((\u03c3 : \u211d) - 1) + U * Complex.I) \u2260 0 := by\n intro h\n have him : (((\u03c3 : \u211d) - 1) + U * Complex.I).im = 0 := by rw [h]; simp\n simp at him\n linarith\n have hle := norm_one_add_one_div_le hs0\n have hre : (((\u03c3 : \u211d) - 1) + U * Complex.I).re + 1 = \u03c3 := by\n simp [Complex.add_re, Complex.ofReal_re, Complex.mul_re, Complex.I_re, Complex.I_im,\n Complex.sub_re, Complex.one_re]\n have hns : Complex.normSq (((\u03c3 : \u211d) - 1) + U * Complex.I) = (\u03c3 - 1) ^ 2 + U ^ 2 := by\n simp [Complex.normSq_apply]\n ring\n have hstep : ((((\u03c3 : \u211d) - 1) + U * Complex.I).re + 1) /\n Complex.normSq (((\u03c3 : \u211d) - 1) + U * Complex.I) \u2264 \u03c3 / U ^ 2 := by\n rw [hre, hns]\n have hU2 : (0 : \u211d) < U ^ 2 := by positivity\n have h1 : (0 : \u211d) \u2264 (\u03c3 - 1) ^ 2 := sq_nonneg _\n exact (div_le_div_iff_of_pos_left (by linarith : (0 : \u211d) < \u03c3)\n (by positivity) hU2).mpr (by linarith [h1])\n have hstep1 : 1 + ((((\u03c3 : \u211d) - 1) + U * Complex.I).re + 1) /\n Complex.normSq (((\u03c3 : \u211d) - 1) + U * Complex.I) \u2264 1 + \u03c3 / U ^ 2 := by\n linarith [hstep]\n have hpow1 : \u2016(1 + 1/(((\u03c3 : \u211d) - 1) + U * Complex.I))\u2016 ^ n \u2264 (1 + \u03c3 / U ^ 2) ^ n :=\n pow_le_pow_left\u2080 (norm_nonneg _) (hle.trans hstep1) n\n have hpow2 : (1 + \u03c3 / U ^ 2) ^ n \u2264 Real.exp ((n : \u211d) * (\u03c3 / U ^ 2)) := by\n calc (1 + \u03c3 / U ^ 2) ^ n \u2264 (Real.exp (\u03c3 / U ^ 2)) ^ n := by\n have h := Real.add_one_le_exp (\u03c3 / U ^ 2)\n exact pow_le_pow_left\u2080 (by positivity) (by linarith) n\n _ = Real.exp ((n : \u211d) * (\u03c3 / U ^ 2)) := (Real.exp_nat_mul (\u03c3 / U ^ 2) n).symm\n have hexp : (n : \u211d) * (\u03c3 / U ^ 2) \u2264 (4 / 9) * \u03c3 := by\n have hU2 : (0 : \u211d) < U ^ 2 := by positivity\n have h\u03c30 : (0 : \u211d) < \u03c3 := by linarith\n have h1 : (n : \u211d) / U ^ 2 \u2264 4 / 9 := by\n have h2 := div_le_div_of_nonneg_right hnU hU2.le\n rwa [mul_div_cancel_right\u2080 _ hU2.ne'] at h2\n rw [show (n : \u211d) * (\u03c3 / U ^ 2) = ((n : \u211d) / U ^ 2) * \u03c3 by ring]\n exact mul_le_mul_of_nonneg_right h1 h\u03c30.le\n calc \u2016(1 + 1/(((\u03c3 : \u211d) - 1) + U * Complex.I))\u2016 ^ n\n \u2264 Real.exp ((n : \u211d) * (\u03c3 / U ^ 2)) := hpow1.trans hpow2\n _ \u2264 Real.exp ((4 / 9) * \u03c3) := Real.exp_le_exp.mpr hexp\n\n/-! ## 5. The product envelope and the integral assembly (DL-3c/d) -/\n\n/-- **The product envelope** (D-074 \u00a77): for \u03c3 \u2265 3, 0 < t, n \u2264 (4/9)t\u00b2,\n\u2016Jlag n (\u03c3+it)\u2016 \u2264 (4\u00b7e^{\u2212c\u03c3} + 4\u00b72^{\u2212\u03c3})\u00b7dirichletC2, c = log 2 \u2212 4/9.\nThe kernel envelope (e^{(4/9)\u03c3}) times the zeta halving (2^{\u2212(\u03c3\u22122)})\ncollapses to the single exponential 4\u00b7e^{\u2212c\u03c3}: no geometric series. -/\ntheorem Jlag_dogleg_norm_le_envelope {n : \u2115} {\u03c3 t : \u211d}\n (h\u03c3 : 3 \u2264 \u03c3) (ht : 0 < t) (hnU : (n : \u211d) \u2264 (4 / 9) * t ^ 2) :\n \u2016Jlag n ((\u03c3 : \u211d) + t * Complex.I)\u2016 \u2264\n dirichletC2 * (4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) + 4 * (2 : \u211d) ^ (-\u03c3)) := by\n have hw1 : ((\u03c3 : \u211d) + t * Complex.I) - 1 = ((\u03c3 : \u211d) - 1) + t * Complex.I := by\n ring\n have hs1ne : (((\u03c3 : \u211d) - 1) + t * Complex.I) \u2260 0 := by\n intro h\n have him : (((\u03c3 : \u211d) - 1) + t * Complex.I).im = 0 := by rw [h]; simp\n simp at him\n linarith\n have hwid : ((\u03c3 : \u211d) + t * Complex.I) / (((\u03c3 : \u211d) + t * Complex.I) - 1) =\n 1 + 1 / (((\u03c3 : \u211d) - 1) + t * Complex.I) := by\n rw [hw1]\n field_simp [hs1ne]\n ring\n have hker := one_add_div_pow_norm_le_exp_four_ninths h\u03c3 ht hnU\n have hzeta := norm_logDeriv_zeta_le_two_pow (show (2 : \u211d) \u2264 \u03c3 by linarith) (t := t)\n have hk : \u2016kFun n ((\u03c3 : \u211d) + t * Complex.I)\u2016 \u2264 Real.exp ((4 / 9) * \u03c3) + 1 := by\n unfold kFun\n rw [hwid]\n calc \u2016(1 + 1 / (((\u03c3 : \u211d) - 1) + t * Complex.I)) ^ n - 1\u2016\n \u2264 \u2016(1 + 1 / (((\u03c3 : \u211d) - 1) + t * Complex.I)) ^ n\u2016 + \u2016(1 : \u2102)\u2016 := norm_sub_le _ _\n _ = \u2016(1 + 1 / (((\u03c3 : \u211d) - 1) + t * Complex.I))\u2016 ^ n + 1 := by rw [norm_pow, norm_one]\n _ \u2264 Real.exp ((4 / 9) * \u03c3) + 1 := by linarith [hker]\n have hprod : \u2016Jlag n ((\u03c3 : \u211d) + t * Complex.I)\u2016 \u2264\n (Real.exp ((4 / 9) * \u03c3) + 1) * ((2 : \u211d) ^ (-(\u03c3 - 2)) * dirichletC2) := by\n have hn3 : \u2016Jlag n ((\u03c3 : \u211d) + t * Complex.I)\u2016 =\n \u2016kFun n ((\u03c3 : \u211d) + t * Complex.I)\u2016 *\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + t * Complex.I)\u2016 := by\n show \u2016kFun n ((\u03c3 : \u211d) + t * Complex.I) *\n (-logDeriv riemannZeta ((\u03c3 : \u211d) + t * Complex.I))\u2016 = _\n rw [norm_mul, norm_neg]\n rw [hn3]\n exact mul_le_mul hk hzeta (norm_nonneg _)\n (add_nonneg (Real.exp_nonneg _) (by norm_num))\n have h2b : (2 : \u211d) ^ (-\u03c3) = Real.exp (-(Real.log 2) * \u03c3) := by\n rw [Real.rpow_def_of_pos (by norm_num : (0 : \u211d) < 2)]\n congr 1\n ring\n have h22 : (2 : \u211d) ^ (2 : \u211d) = 4 := by\n rw [Real.rpow_two]\n norm_num\n have h2a : (2 : \u211d) ^ (-(\u03c3 - 2)) = 4 * (2 : \u211d) ^ (-\u03c3) := by\n rw [show (-(\u03c3 - 2)) = -\u03c3 + 2 by ring, Real.rpow_add (by norm_num : (0 : \u211d) < 2), h2b, h22]\n ring\n have hexp_alg : Real.exp ((4 / 9) * \u03c3) * Real.exp (-(Real.log 2) * \u03c3) =\n Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) := by\n rw [\u2190 Real.exp_add]\n congr 1\n ring\n have halg : (Real.exp ((4 / 9) * \u03c3) + 1) * ((2 : \u211d) ^ (-(\u03c3 - 2))) =\n 4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) + 4 * (2 : \u211d) ^ (-\u03c3) := by\n rw [h2a, h2b]\n calc (Real.exp ((4 / 9) * \u03c3) + 1) * (4 * Real.exp (-(Real.log 2) * \u03c3))\n = 4 * (Real.exp ((4 / 9) * \u03c3) * Real.exp (-(Real.log 2) * \u03c3)) +\n 4 * Real.exp (-(Real.log 2) * \u03c3) := by ring\n _ = 4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) + 4 * Real.exp (-(Real.log 2) * \u03c3) := by\n rw [hexp_alg]\n calc \u2016Jlag n ((\u03c3 : \u211d) + t * Complex.I)\u2016\n \u2264 (Real.exp ((4 / 9) * \u03c3) + 1) * ((2 : \u211d) ^ (-(\u03c3 - 2)) * dirichletC2) := hprod\n _ = dirichletC2 * ((Real.exp ((4 / 9) * \u03c3) + 1) * (2 : \u211d) ^ (-(\u03c3 - 2))) := by ring\n _ = dirichletC2 * (4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) + 4 * (2 : \u211d) ^ (-\u03c3)) := by\n rw [halg]\n\n/-- The FTC-bound \u222b\u2083^XR e^{\u2212c\u03c3}d\u03c3 \u2264 e^{\u22123c}/c for c > 0. -/\nlemma integral_exp_neg_le {c XR : \u211d} (hc : 0 < c) (_hXR : 3 \u2264 XR) :\n \u222b \u03c3 in (3 : \u211d)..XR, Real.exp (-c * \u03c3) \u2264 Real.exp (-3 * c) / c := by\n have hF : \u2200 x \u2208 Set.uIcc (3 : \u211d) XR,\n HasDerivAt (fun \u03c3 => -Real.exp (-c * \u03c3) / c) (Real.exp (-c * x)) x := by\n intro x hx\n have h2 : HasDerivAt (fun \u03c3 => Real.exp (-c * \u03c3)) (Real.exp (-c * x) * (-c)) x := by\n have h := ((hasDerivAt_id' x).const_mul (-c)).exp\n rwa [mul_one] at h\n have h3 := h2.const_mul (-1 / c)\n rw [show (-1 / c) * (Real.exp (-c * x) * (-c)) = Real.exp (-c * x) by\n field_simp [hc.ne']] at h3\n have h5 : (fun \u03c3 => (-1 / c) * Real.exp (-c * \u03c3)) =\n (fun \u03c3 => -Real.exp (-c * \u03c3) / c) := by\n funext \u03c3\n field_simp [hc.ne']\n rw [h5] at h3\n exact h3\n have hint : IntervalIntegrable (fun \u03c3 => Real.exp (-c * \u03c3)) MeasureTheory.volume 3 XR := by\n apply ContinuousOn.intervalIntegrable\n exact (Real.continuous_exp.comp (continuous_const.mul continuous_id)).continuousOn\n have e : Real.exp (-c * 3) = Real.exp (-3 * c) := by\n congr 1\n ring\n rw [intervalIntegral.integral_eq_sub_of_hasDerivAt hF hint, e]\n have h1 : (0 : \u211d) \u2264 Real.exp (-c * XR) := (Real.exp_pos _).le\n have h2 : (0 : \u211d) < c := hc\n rw [show -Real.exp (-c * XR) / c - -Real.exp (-3 * c) / c =\n (Real.exp (-3 * c) - Real.exp (-c * XR)) / c by\n field_simp [h2.ne']\n ring]\n rw [show Real.exp (-3 * c) / c = (Real.exp (-3 * c) - (0 : \u211d)) / c by ring]\n exact div_le_div_of_nonneg_right (by linarith [h1]) h2.le\n\n/-- The certified exponent-decay constant c = log 2 \u2212 4/9 \u2265 0.2487. -/\nlemma cdog_gt : (0.2487 : \u211d) \u2264 Real.log 2 - 4 / 9 := by\n have h := Real.log_two_gt_d9\n norm_num at h\n linarith\n\n/-- The certified e^{4/3} \u2264 3.8073 (the (1\u2212x/16)\u207b\u00b9\u2076 route + d9 e). -/\nlemma exp_four_thirds_le : Real.exp (4 / 3) \u2264 (3.8073 : \u211d) := by\n have he13 : Real.exp (1 / 3) \u2264 (1.4006 : \u211d) :=\n le_trans (exp_le_inv_sub_sixteen (by norm_num) (by norm_num)) (by norm_num)\n rw [show (4 / 3 : \u211d) = 1 + 1 / 3 by norm_num, Real.exp_add]\n calc Real.exp 1 * Real.exp (1 / 3) \u2264 2.7182818286 * 1.4006 :=\n mul_le_mul Real.exp_one_lt_d9.le he13 (Real.exp_pos _).le (by norm_num)\n _ \u2264 3.8073 := by norm_num\n\n/-- **THE HIGH-HORIZONTAL BOUND** (D-074 \u00a77 capstone; D-073 Cor 4.2's\nR(1.5) in single-exponential-envelope form): for 0 < U, n \u2264 (4/9)U\u00b2\n(i.e. U \u2265 (3/2)\u221an) and 3 \u2264 XR, \u2016HIntegral (Jlag n) 3 XR U\u2016 \u2264 8.38\n(charged; the true value \u2264 1.2 at n = 10\u2075, E-034 V5). Charged with\ndirichletC2 \u2264 1 \u2014 the tight R(1.5) = 5.94 would need a dirichletC2 \u2264\n0.57 build (documented as the tightening path; the fold is\nindifferent: \u0394 \u2248 +2.4 per side). -/\ntheorem hIntegral_Jlag_dogleg_norm_le {n : \u2115} {U XR : \u211d}\n (hU : 0 < U) (hnU : (n : \u211d) \u2264 (4 / 9) * U ^ 2) (hXR : 3 \u2264 XR) :\n \u2016HIntegral (Jlag n) 3 XR U\u2016 \u2264 (8.38 : \u211d) := by\n have hc : (0 : \u211d) < Real.log 2 - 4 / 9 := by\n have h := cdog_gt\n linarith\n have hpt : \u2200 \u03c3 \u2208 Set.Ioc 3 XR,\n \u2016Jlag n ((\u03c3 : \u211d) + U * Complex.I)\u2016 \u2264\n dirichletC2 * (4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) + 4 * (2 : \u211d) ^ (-\u03c3)) :=\n fun \u03c3 h\u03c3 => Jlag_dogleg_norm_le_envelope (by linarith [h\u03c3.1]) hU hnU\n have hcontA : Continuous (fun \u03c3 : \u211d => Real.exp (-(Real.log 2 - 4 / 9) * \u03c3)) :=\n Real.continuous_exp.comp (continuous_const.mul continuous_id)\n have hcontB : Continuous (fun \u03c3 : \u211d => (2 : \u211d) ^ (-\u03c3)) := by\n have h1 : Continuous (fun \u03c3 : \u211d => Real.exp (-(Real.log 2) * \u03c3)) :=\n Real.continuous_exp.comp (continuous_const.mul continuous_id)\n have h2 : (fun \u03c3 : \u211d => (2 : \u211d) ^ (-\u03c3)) =\n (fun \u03c3 : \u211d => Real.exp (-(Real.log 2) * \u03c3)) := by\n funext \u03c3\n rw [Real.rpow_def_of_pos (by norm_num : (0 : \u211d) < 2)]\n congr 1\n ring\n rw [h2]\n exact h1\n have hIntA : IntervalIntegrable (fun \u03c3 : \u211d => 4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3))\n MeasureTheory.volume 3 XR := by\n apply ContinuousOn.intervalIntegrable\n exact (hcontA.const_mul 4).continuousOn\n have hIntB : IntervalIntegrable (fun \u03c3 : \u211d => 4 * (2 : \u211d) ^ (-\u03c3)) MeasureTheory.volume 3 XR := by\n apply ContinuousOn.intervalIntegrable\n exact (hcontB.const_mul 4).continuousOn\n have hIntG : IntervalIntegrable (fun \u03c3 : \u211d =>\n dirichletC2 * (4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) + 4 * (2 : \u211d) ^ (-\u03c3)))\n MeasureTheory.volume 3 XR := by\n have h := (hIntA.add hIntB).const_mul dirichletC2\n convert h using 1\n -- step 1: \u2016H\u2016 \u2264 \u222b envelope\n have h1 : \u2016HIntegral (Jlag n) 3 XR U\u2016 \u2264\n \u222b \u03c3 in (3 : \u211d)..XR,\n dirichletC2 * (4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) + 4 * (2 : \u211d) ^ (-\u03c3)) := by\n unfold HIntegral\n apply intervalIntegral.norm_integral_le_of_norm_le hXR _ hIntG\n exact Filter.Eventually.of_forall (fun \u03c3 h\u03c3 => hpt \u03c3 h\u03c3)\n -- step 2: \u222b envelope = dirichletC2\u00b7(4\u222be^{\u2212c\u03c3} + 4\u222b2^{\u2212\u03c3})\n have h2 : \u222b \u03c3 in (3 : \u211d)..XR,\n dirichletC2 * (4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) + 4 * (2 : \u211d) ^ (-\u03c3))\n = dirichletC2 * ((\u222b \u03c3 in (3 : \u211d)..XR, 4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3)) +\n (\u222b \u03c3 in (3 : \u211d)..XR, 4 * (2 : \u211d) ^ (-\u03c3))) := by\n rw [intervalIntegral.integral_const_mul, intervalIntegral.integral_add hIntA hIntB]\n -- step 3: the two integral bounds\n have h3a : \u222b \u03c3 in (3 : \u211d)..XR, 4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) \u2264\n Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9)) := by\n rw [intervalIntegral.integral_const_mul]\n have h := integral_exp_neg_le hc hXR\n have he3c : Real.exp (-3 * (Real.log 2 - 4 / 9)) = Real.exp (4 / 3) / 8 := by\n have h3l2 : Real.exp (-(3 * Real.log 2)) = 1 / 8 := by\n have e1 : -(3 * Real.log 2) = Real.log (1 / 8) := by\n rw [show ((1 : \u211d) / 8) = (2 ^ 3 : \u211d)\u207b\u00b9 by norm_num, Real.log_inv, Real.log_pow,\n Nat.cast_ofNat]\n rw [e1, Real.exp_log (by norm_num : (0 : \u211d) < 1 / 8)]\n calc Real.exp (-3 * (Real.log 2 - 4 / 9))\n = Real.exp ((4 / 3) + -(3 * Real.log 2)) := by congr 1; ring\n _ = Real.exp (4 / 3) * Real.exp (-(3 * Real.log 2)) := by rw [Real.exp_add]\n _ = Real.exp (4 / 3) / 8 := by rw [h3l2]; ring\n rw [he3c] at h\n calc 4 * \u222b \u03c3 in (3 : \u211d)..XR, Real.exp (-(Real.log 2 - 4 / 9) * \u03c3)\n \u2264 4 * ((Real.exp (4 / 3) / 8) / (Real.log 2 - 4 / 9)) :=\n mul_le_mul_of_nonneg_left h (by norm_num)\n _ = Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9)) := by\n field_simp [hc.ne']\n ring\n have h3b : \u222b \u03c3 in (3 : \u211d)..XR, 4 * (2 : \u211d) ^ (-\u03c3) \u2264 1 / (2 * Real.log 2) := by\n have h2e : (fun \u03c3 : \u211d => 4 * (2 : \u211d) ^ (-\u03c3)) =\n (fun \u03c3 : \u211d => 4 * Real.exp (-(Real.log 2) * \u03c3)) := by\n funext \u03c3\n rw [Real.rpow_def_of_pos (by norm_num : (0 : \u211d) < 2)]\n congr 1\n ring\n rw [h2e, intervalIntegral.integral_const_mul]\n have h := integral_exp_neg_le (Real.log_pos (by norm_num : (1 : \u211d) < 2)) hXR\n have h3l2 : Real.exp (-3 * Real.log 2) = 1 / 8 := by\n have e1 : (-3 * Real.log 2) = Real.log (1 / 8) := by\n rw [show ((1 : \u211d) / 8) = (2 ^ 3 : \u211d)\u207b\u00b9 by norm_num, Real.log_inv, Real.log_pow,\n Nat.cast_ofNat]\n ring\n rw [e1, Real.exp_log (by norm_num : (0 : \u211d) < 1 / 8)]\n rw [h3l2] at h\n calc 4 * \u222b \u03c3 in (3 : \u211d)..XR, Real.exp (-(Real.log 2) * \u03c3)\n \u2264 4 * ((1 / 8) / Real.log 2) := by\n apply mul_le_mul_of_nonneg_left h (by norm_num : (0 : \u211d) \u2264 4)\n _ = 1 / (2 * Real.log 2) := by\n field_simp [(Real.log_pos (by norm_num : (1 : \u211d) < 2)).ne']\n norm_num\n -- step 4: the certified assembly\n have hlog2 : (0.6931471803 : \u211d) \u2264 Real.log 2 := Real.log_two_gt_d9.le\n have h48 : Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9)) \u2264 (7.6545 : \u211d) := by\n have hcge := cdog_gt\n have h1 : Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9)) \u2264 3.8073 / (2 * 0.2487) :=\n div_le_div\u2080 (by norm_num : (0 : \u211d) \u2264 3.8073) exp_four_thirds_le\n (by norm_num : (0 : \u211d) < 2 * 0.2487) (by linarith [hcge])\n calc Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9))\n \u2264 3.8073 / (2 * 0.2487) := h1\n _ \u2264 7.6545 := by norm_num\n have h72 : 1 / (2 * Real.log 2) \u2264 (0.7214 : \u211d) := by\n have h1 : 1 / (2 * Real.log 2) \u2264 1 / (2 * 0.6931471803) :=\n one_div_le_one_div_of_le (by positivity) (by linarith)\n calc 1 / (2 * Real.log 2) \u2264 1 / (2 * 0.6931471803) := h1\n _ \u2264 0.7214 := by norm_num\n have hC2 : dirichletC2 \u2264 1 := dirichletC2_le_one\n have hsum : dirichletC2 * ((\u222b \u03c3 in (3 : \u211d)..XR, 4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3)) +\n (\u222b \u03c3 in (3 : \u211d)..XR, 4 * (2 : \u211d) ^ (-\u03c3))) \u2264 (8.38 : \u211d) := by\n have hA0 : (0 : \u211d) \u2264 Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9)) := by positivity\n have hB0 : (0 : \u211d) \u2264 1 / (2 * Real.log 2) := by positivity\n have hIntAB : (0 : \u211d) \u2264 (\u222b \u03c3 in (3 : \u211d)..XR, 4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3)) +\n (\u222b \u03c3 in (3 : \u211d)..XR, 4 * (2 : \u211d) ^ (-\u03c3)) := by\n apply add_nonneg\n \u00b7 apply intervalIntegral.integral_nonneg hXR\n intro \u03c3 h\u03c3\n positivity\n \u00b7 apply intervalIntegral.integral_nonneg hXR\n intro \u03c3 h\u03c3\n positivity\n calc dirichletC2 * ((\u222b \u03c3 in (3 : \u211d)..XR, 4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3)) +\n (\u222b \u03c3 in (3 : \u211d)..XR, 4 * (2 : \u211d) ^ (-\u03c3)))\n \u2264 1 * (Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9)) + 1 / (2 * Real.log 2)) := by\n apply mul_le_mul hC2 (add_le_add h3a h3b) hIntAB (by norm_num)\n _ = Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9)) + 1 / (2 * Real.log 2) := by ring\n _ \u2264 7.6545 + 0.7214 := add_le_add h48 h72\n _ \u2264 8.38 := by norm_num\n calc \u2016HIntegral (Jlag n) 3 XR U\u2016\n \u2264 \u222b \u03c3 in (3 : \u211d)..XR,\n dirichletC2 * (4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) + 4 * (2 : \u211d) ^ (-\u03c3)) := h1\n _ = dirichletC2 * ((\u222b \u03c3 in (3 : \u211d)..XR, 4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3)) +\n (\u222b \u03c3 in (3 : \u211d)..XR, 4 * (2 : \u211d) ^ (-\u03c3))) := h2\n _ \u2264 8.38 := hsum\n\n/-! ## 6. The far-right vertical drop (DL-4, D-074 \u00a78) -/\n\n/-- **Kernel at the far-right vertical** (D-074 \u00a78): for n \u2265 16 and\nt\u00b2 \u2265 n, \u2016kFun n (2\u221an+it)\u2016 \u2264 e^{\u221an/2}+1. (The ii\u2032-4 lemma\n`kFun_shift_norm_le_exp_sqrt_half_add_one` takes re s \u2265 2\u221an, i.e.\nre w \u2265 2\u221an+1 \u2014 this is the w = 2\u221an variant: |1+1/(w\u22121)| \u2264\n1+(2\u221an)/((2\u221an\u22121)\u00b2+t\u00b2) \u2264 1+1/(2\u221an) since 4\u221an\u22121 \u2264 t\u00b2.) -/\ntheorem kFun_right_vertical_norm_le_exp_sqrt_half_add_one {n : \u2115} {t : \u211d}\n (hn : 16 \u2264 n) (ht : (n : \u211d) \u2264 t ^ 2) :\n \u2016kFun n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 \u2264\n Real.exp (Real.sqrt (n : \u211d) / 2) + 1 := by\n have hnR : (16 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n have hsq : (0 : \u211d) < Real.sqrt (n : \u211d) := Real.sqrt_pos.mpr (by linarith)\n have hw1 : (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) - 1 =\n ((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I := by\n push_cast\n ring\n have hs0 : ((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I \u2260 0 := by\n intro h\n have him : (((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I).im = 0 := by\n rw [h]; simp\n simp at him\n have ht0 : t = 0 := by\n have h1 : (((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I).im = t := by simp\n linarith\n rw [ht0] at ht\n nlinarith [hnR]\n have hle := norm_one_add_one_div_le hs0\n have hre : (((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I).re + 1 =\n 2 * Real.sqrt (n : \u211d) := by\n simp [Complex.add_re, Complex.ofReal_re, Complex.mul_re, Complex.I_re, Complex.I_im,\n Complex.sub_re, Complex.one_re]\n have hns : Complex.normSq (((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I) =\n (2 * Real.sqrt (n : \u211d) - 1) ^ 2 + t ^ 2 := by\n simp [Complex.normSq_apply]\n ring\n have hkey : (2 * Real.sqrt (n : \u211d)) /\n Complex.normSq (((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I) \u2264\n 1 / (2 * Real.sqrt (n : \u211d)) := by\n rw [hns]\n have hsqn : Real.sqrt (n : \u211d) ^ 2 = (n : \u211d) := Real.sq_sqrt (by linarith)\n have h1 : 4 * Real.sqrt (n : \u211d) - 1 \u2264 t ^ 2 := by\n have h2 : 4 * Real.sqrt (n : \u211d) \u2264 (n : \u211d) + 1 := by\n have h3 : (4 * Real.sqrt (n : \u211d)) ^ 2 \u2264 ((n : \u211d) + 1) ^ 2 := by\n rw [show (4 * Real.sqrt (n : \u211d)) ^ 2 = 16 * (Real.sqrt (n : \u211d) ^ 2) by ring, hsqn]\n nlinarith [sq_nonneg ((n : \u211d) - 1), hnR]\n nlinarith [hsq]\n nlinarith [ht, h2]\n rw [show (2 * Real.sqrt (n : \u211d) - 1) ^ 2 + t ^ 2 =\n 4 * (Real.sqrt (n : \u211d) ^ 2) - 4 * Real.sqrt (n : \u211d) + 1 + t ^ 2 by ring, hsqn]\n have h4 : (0 : \u211d) < 4 * (n : \u211d) - 4 * Real.sqrt (n : \u211d) + 1 + t ^ 2 := by\n nlinarith [ht, sq_nonneg t, hsq]\n rw [div_le_iff\u2080 h4,\n show (1 / (2 * Real.sqrt (n : \u211d))) * (4 * (n : \u211d) - 4 * Real.sqrt (n : \u211d) + 1 + t ^ 2) =\n (4 * (n : \u211d) - 4 * Real.sqrt (n : \u211d) + 1 + t ^ 2) / (2 * Real.sqrt (n : \u211d)) by\n field_simp [hsq.ne'],\n le_div_iff\u2080 (by linarith [hsq] : (0 : \u211d) < 2 * Real.sqrt (n : \u211d))]\n nlinarith [h1, ht, hsq, hsqn]\n have hstep : 1 + ((((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I).re + 1) /\n Complex.normSq (((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I) \u2264\n 1 + 1 / (2 * Real.sqrt (n : \u211d)) := by\n rw [hre]\n have h1 : (2 * Real.sqrt (n : \u211d)) /\n Complex.normSq (((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I) \u2264\n 1 / (2 * Real.sqrt (n : \u211d)) := hkey\n linarith [h1]\n have hpow1 : \u2016(1 + 1/(((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I))\u2016 ^ n \u2264\n (1 + 1 / (2 * Real.sqrt (n : \u211d))) ^ n :=\n pow_le_pow_left\u2080 (norm_nonneg _) (hle.trans hstep) n\n have hpow2 : (1 + 1 / (2 * Real.sqrt (n : \u211d))) ^ n \u2264\n Real.exp (Real.sqrt (n : \u211d) / 2) := by\n calc (1 + 1 / (2 * Real.sqrt (n : \u211d))) ^ n\n \u2264 (Real.exp (1 / (2 * Real.sqrt (n : \u211d)))) ^ n := by\n have h := Real.add_one_le_exp (1 / (2 * Real.sqrt (n : \u211d)))\n exact pow_le_pow_left\u2080 (by positivity) (by linarith) n\n _ = Real.exp ((n : \u211d) * (1 / (2 * Real.sqrt (n : \u211d)))) :=\n (Real.exp_nat_mul _ n).symm\n _ = Real.exp (Real.sqrt (n : \u211d) / 2) := by\n congr 1\n have hsqn : Real.sqrt (n : \u211d) ^ 2 = (n : \u211d) := Real.sq_sqrt (by linarith)\n field_simp [hsq.ne']\n nlinarith [hsqn]\n have hwid : (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) /\n ((((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) - 1) =\n 1 + 1 / (((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I) := by\n rw [hw1]\n field_simp [hs0]\n push_cast\n ring\n unfold kFun\n rw [hwid]\n calc \u2016(1 + 1/(((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I)) ^ n - 1\u2016\n \u2264 \u2016(1 + 1/(((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I)) ^ n\u2016 + \u2016(1 : \u2102)\u2016 :=\n norm_sub_le _ _\n _ = \u2016(1 + 1/(((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I))\u2016 ^ n + 1 := by\n rw [norm_pow, norm_one]\n _ \u2264 Real.exp (Real.sqrt (n : \u211d) / 2) + 1 := by linarith [hpow1.trans hpow2]\n\n/-- **The far-right vertical drop** (D-074 \u00a78 V_right): for n \u2265 16,\n0 < T \u2264 U, T\u00b2 \u2265 n, \u2016VIntegral (Jlag n) (2\u221an) T U\u2016 \u2264\n(U\u2212T)\u00b7(e^{\u221an/2}+1)\u00b72^{\u2212(2\u221an\u22122)}\u00b7dirichletC2 \u2014 exponentially tiny. -/\ntheorem vIntegral_Jlag_right_norm_le {n : \u2115} {T U : \u211d}\n (hn : 16 \u2264 n) (hT0 : (0 : \u211d) < T) (hTU : T \u2264 U) (hTn : (n : \u211d) \u2264 T ^ 2) :\n \u2016VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) T U\u2016 \u2264\n (U - T) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * dirichletC2) := by\n have hnorm : \u2016VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) T U\u2016 =\n \u2016\u222b t in T..U, Jlag n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 := by\n unfold VIntegral\n rw [norm_smul, Complex.norm_I, one_mul]\n rw [hnorm]\n have hbound : \u2200 t \u2208 Set.Ioc T U,\n \u2016Jlag n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 \u2264\n (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * dirichletC2) := by\n intro t ht\n have htT : T < t := ht.1\n have ht2 : (n : \u211d) \u2264 t ^ 2 := by nlinarith [hTn, hT0]\n have h1 := kFun_right_vertical_norm_le_exp_sqrt_half_add_one hn ht2\n have h2 := norm_logDeriv_zeta_le_two_pow\n (show (2 : \u211d) \u2264 2 * Real.sqrt (n : \u211d) by\n have hnR : (16 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n have hsq : (4 : \u211d) \u2264 Real.sqrt (n : \u211d) := by\n have h1 : Real.sqrt 16 \u2264 Real.sqrt (n : \u211d) :=\n Real.sqrt_le_sqrt (by exact_mod_cast hn : (16 : \u211d) \u2264 (n : \u211d))\n have h2 : Real.sqrt 16 = 4 := by\n rw [Real.sqrt_eq_iff_eq_sq (by norm_num) (by norm_num)]; norm_num\n rwa [h2] at h1\n linarith) (t := t)\n have hnorm3 : \u2016Jlag n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 =\n \u2016kFun n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 *\n \u2016logDeriv riemannZeta (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 := by\n show \u2016kFun n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) *\n (-logDeriv riemannZeta (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I))\u2016 = _\n rw [norm_mul, norm_neg]\n rw [hnorm3]\n exact mul_le_mul h1 h2 (norm_nonneg _)\n (add_nonneg (Real.exp_nonneg _) (by norm_num))\n have hint : \u2016\u222b t in T..U, Jlag n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 \u2264\n ((Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * dirichletC2)) * |U - T| := by\n apply intervalIntegral.norm_integral_le_of_norm_le_const\n intro t ht\n rw [Set.uIoc_of_le hTU] at ht\n exact hbound t ht\n have habs : |U - T| = U - T := abs_of_nonneg (by linarith)\n rw [habs] at hint\n calc \u2016\u222b t in T..U, Jlag n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016\n \u2264 ((Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * dirichletC2)) * (U - T) := hint\n _ = (U - T) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * dirichletC2) := by ring\n\n/-! ## 7. The total right-horizontal bound (DL-5, D-074 \u00a73.4) -/\n\n/-- **The upper right-tail bound** (D-074 \u00a73.4): for n \u2265 16 and\nT \u2208 [\u221an, \u221an+1] (the T_cut window), U = (3/2)\u00b7T,\n\u2016HIntegral (Jlag n) 3 (2\u221an) T\u2016 \u2264 ((\u221an+1)/2)\u00b7(e^{5/2}+1)/2 + 8.38 +\nIIMaj(n)/2 \u2014 the exact deformation identity +\nV_left/H_high/V_right piece bounds, all in the zero-free region. -/\ntheorem hIntegral_Jlag_low_le_dogLegUpper {n : \u2115} {T : \u211d}\n (hn : 16 \u2264 n) (hTn : Real.sqrt (n : \u211d) \u2264 T) (hTn1 : T \u2264 Real.sqrt (n : \u211d) + 1) :\n \u2016HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) T\u2016 \u2264\n ((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : \u211d) +\n IIMaj (n : \u211d) / 2 := by\n have hnR : (16 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n have hsqrt4 : (4 : \u211d) \u2264 Real.sqrt (n : \u211d) := by\n have h1 : Real.sqrt 16 \u2264 Real.sqrt (n : \u211d) :=\n Real.sqrt_le_sqrt (by exact_mod_cast hn : (16 : \u211d) \u2264 (n : \u211d))\n have h2 : Real.sqrt 16 = 4 := by\n rw [Real.sqrt_eq_iff_eq_sq (by norm_num) (by norm_num)]; norm_num\n rwa [h2] at h1\n have hT0 : (0 : \u211d) < T := by linarith\n have hTn2 : (n : \u211d) \u2264 T ^ 2 := by\n have h1 : (Real.sqrt (n : \u211d)) ^ 2 \u2264 T ^ 2 :=\n pow_le_pow_left\u2080 (Real.sqrt_nonneg _) hTn 2\n rwa [Real.sq_sqrt (by linarith [Real.sqrt_nonneg (n : \u211d)])] at h1\n have hU0 : (0 : \u211d) < (3 / 2) * T := by linarith [hT0]\n have hTU : T \u2264 (3 / 2) * T := by linarith [hT0]\n have hnU : (n : \u211d) \u2264 (4 / 9) * ((3 / 2) * T) ^ 2 := by\n have h1 : (4 / 9) * ((3 / 2) * T) ^ 2 = T ^ 2 := by\n field_simp\n ring\n rw [h1]\n exact hTn2\n have hXR : (3 : \u211d) \u2264 2 * Real.sqrt (n : \u211d) := by linarith\n have hid := upper_right_horizontal_eq_dogleg hT0 hTU hXR (n := n)\n have hH := hIntegral_Jlag_dogleg_norm_le hU0 hnU hXR (n := n)\n have hVr := vIntegral_Jlag_right_norm_le hn hT0 hTU hTn2 (n := n)\n have hVl := vIntegral_Jlag_three_norm_le hT0 hTU hTn2 (n := n)\n have hlen : (3 / 2) * T - T \u2264 (Real.sqrt (n : \u211d) + 1) / 2 := by linarith [hTn1, hTn]\n have hlen0 : (0 : \u211d) \u2264 (3 / 2) * T - T := by linarith [hT0]\n -- V_left \u2264 ((\u221an+1)/2)\u00b7(e^{5/2}+1)/2\n have hVl2 : \u2016VIntegral (Jlag n) 3 T ((3 / 2) * T)\u2016 \u2264\n ((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 := by\n refine hVl.trans ?_\n exact div_le_div_of_nonneg_right\n (mul_le_mul hlen (le_refl _) (by positivity) (by positivity)) (by norm_num)\n -- V_right \u2264 IIMaj/2\n have hVr2 : \u2016VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) T ((3 / 2) * T)\u2016 \u2264\n IIMaj (n : \u211d) / 2 := by\n have hC2 : dirichletC2 \u2264 1 := dirichletC2_le_one\n have hK : (0 : \u211d) < (Real.sqrt (n : \u211d) + 1) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2))) := by positivity\n have eA : ((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * (1 : \u211d)) =\n (1 / 2) * ((Real.sqrt (n : \u211d) + 1) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)))) := by ring\n have eB : IIMaj (n : \u211d) / 2 =\n (0.57 : \u211d) * ((Real.sqrt (n : \u211d) + 1) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)))) := by\n unfold IIMaj\n ring\n calc \u2016VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) T ((3 / 2) * T)\u2016\n \u2264 ((3 / 2) * T - T) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * dirichletC2) := hVr\n _ \u2264 ((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * (1 : \u211d)) := by\n have h1 : ((3 / 2) * T - T) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) \u2264\n ((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) :=\n mul_le_mul hlen (le_refl _) (by positivity) (by positivity)\n have h2 : (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * dirichletC2 \u2264\n (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * (1 : \u211d) :=\n mul_le_mul_of_nonneg_left hC2 (Real.rpow_nonneg (by norm_num) _)\n exact mul_le_mul h1 h2\n (mul_nonneg (Real.rpow_nonneg (by norm_num) _) dirichletC2_nonneg)\n (by positivity)\n _ \u2264 IIMaj (n : \u211d) / 2 := by\n rw [eA, eB]\n apply mul_le_mul_of_nonneg_right _ hK.le\n norm_num\n -- assemble via the exact identity\n rw [hid]\n calc \u2016HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) ((3 / 2) * T) -\n VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) T ((3 / 2) * T) +\n VIntegral (Jlag n) 3 T ((3 / 2) * T)\u2016\n \u2264 \u2016HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) ((3 / 2) * T)\u2016 +\n \u2016VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) T ((3 / 2) * T)\u2016 +\n \u2016VIntegral (Jlag n) 3 T ((3 / 2) * T)\u2016 := by\n have h1 := norm_add_le\n (HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) ((3 / 2) * T) -\n VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) T ((3 / 2) * T))\n (VIntegral (Jlag n) 3 T ((3 / 2) * T))\n have h2 := norm_sub_le\n (HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) ((3 / 2) * T))\n (VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) T ((3 / 2) * T))\n linarith [h1, h2]\n _ \u2264 (8.38 : \u211d) + IIMaj (n : \u211d) / 2 +\n ((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 :=\n add_le_add (add_le_add hH hVr2) hVl2\n _ = ((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : \u211d) +\n IIMaj (n : \u211d) / 2 := by ring\n\n/-- **The lower right-tail bound by conjugation** (D-074 \u00a73.4): the\nsame bound holds at im = \u2212T (the integrand is conjugation-symmetric,\nJlag_conj; the interval integral maps conj through). -/\ntheorem hIntegral_Jlag_low_neg_norm_le_dogLegUpper {n : \u2115} {T : \u211d}\n (hn : 16 \u2264 n) (hTn : Real.sqrt (n : \u211d) \u2264 T) (hTn1 : T \u2264 Real.sqrt (n : \u211d) + 1) :\n \u2016HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) (-T)\u2016 \u2264\n ((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : \u211d) +\n IIMaj (n : \u211d) / 2 := by\n have hT0 : (0 : \u211d) < T := by\n have hnR : (16 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n have hsqrt4 : (4 : \u211d) \u2264 Real.sqrt (n : \u211d) := by\n have h1 : Real.sqrt 16 \u2264 Real.sqrt (n : \u211d) :=\n Real.sqrt_le_sqrt (by exact_mod_cast hn : (16 : \u211d) \u2264 (n : \u211d))\n have h2 : Real.sqrt 16 = 4 := by\n rw [Real.sqrt_eq_iff_eq_sq (by norm_num) (by norm_num)]; norm_num\n rwa [h2] at h1\n linarith\n have hconj : HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) (-T) =\n (starRingEnd \u2102) (HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) T) := by\n unfold HIntegral\n rw [\u2190 intervalIntegral.intervalIntegral_conj]\n apply intervalIntegral.integral_congr\n intro \u03c3 h\u03c3\n show Jlag n ((\u03c3 : \u211d) + (((-T : \u211d)) : \u2102) * Complex.I) =\n (starRingEnd \u2102) (Jlag n ((\u03c3 : \u211d) + T * Complex.I))\n have hid2 : ((\u03c3 : \u211d) + (((-T : \u211d)) : \u2102) * Complex.I) =\n (starRingEnd \u2102) ((\u03c3 : \u211d) + T * Complex.I) := by\n simp [Complex.ext_iff]\n rw [hid2]\n exact Jlag_conj n (by\n intro h\n have him : (((\u03c3 : \u211d) + T * Complex.I)).im = T := by simp\n rw [h] at him\n simp at him\n linarith [hT0])\n rw [hconj, Complex.norm_conj]\n exact hIntegral_Jlag_low_le_dogLegUpper hn hTn hTn1\n\n/-- **THE TWO-SIDE RIGHT-HORIZONTAL BOUND** (the DL capstone for\nii\u2032-6-c): both horizontal right tails bounded by the dog-leg charge. -/\ntheorem dogLegUpper_two_sides {n : \u2115} {T : \u211d}\n (hn : 16 \u2264 n) (hTn : Real.sqrt (n : \u211d) \u2264 T) (hTn1 : T \u2264 Real.sqrt (n : \u211d) + 1) :\n \u2016HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) T\u2016 +\n \u2016HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) (-T)\u2016 \u2264\n 2 * (((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : \u211d) +\n IIMaj (n : \u211d) / 2) := by\n rw [show (2 : \u211d) * (((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 +\n (8.38 : \u211d) + IIMaj (n : \u211d) / 2) =\n (((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : \u211d) +\n IIMaj (n : \u211d) / 2) +\n (((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : \u211d) +\n IIMaj (n : \u211d) / 2) by ring]\n exact add_le_add (hIntegral_Jlag_low_le_dogLegUpper hn hTn hTn1)\n (hIntegral_Jlag_low_neg_norm_le_dogLegUpper hn hTn hTn1)\n\n/-! ## 8. The direct Dirichlet bound at re = 2\u221an (DL-6) \u2014 the I_I /\nV_right zeta factor WITHOUT certifying dirichletC2 \u2264 0.57.\n\nThe I_I charge in IIMaj is 0.57\u00b72^{\u2212(2\u221an\u22122)} = 2.28\u00b72^{\u22122\u221an} (the\n(6.10)-route constant |\u03b6\u2032/\u03b6(2)|). Proving dirichletC2 \u2264 0.57 directly\nneeds a ~100-prime partial-sum build (the antitone-integral tail is too\nfat). AVOIDED here: the DIRECT Dirichlet-series bound at re = 2\u221an gives\nlog2-leading + a 3^{\u2212(2\u221an\u22122)} tail (dirichletC2 \u2264 1), which is \u2264\n0.57\u00b72^{\u2212(2\u221an\u22122)} for n \u2265 5 \u2014 the IIMaj charge exactly. -/\n\n/-- The Dirichlet majorant at s = 2\u221an (summable since 2\u221an > 1). -/\ndef dirichletCX (n : \u2115) : \u211d :=\n \u2211' m : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n ((2 * Real.sqrt (n : \u211d) : \u211d) : \u2102) m\u2016\n\n/-- \u2016\u03b6\u2032/\u03b6(2\u221an+it)\u2016 \u2264 dirichletCX n for n \u2265 1 (the LSeries majorant). -/\nlemma norm_logDeriv_zeta_le_dirichletCX {n : \u2115} (hn : 1 \u2264 n) {t : \u211d} :\n \u2016logDeriv riemannZeta (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 \u2264\n dirichletCX n := by\n have h1 : (1 : \u211d) \u2264 Real.sqrt (n : \u211d) := Real.one_le_sqrt.mpr (by exact_mod_cast hn)\n have hs1 : (1 : \u211d) < (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I).re := by\n simp\n linarith\n have h1' : -logDeriv riemannZeta (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\n = LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) := by\n have h2 := ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div hs1\n rw [logDeriv, Pi.div_apply, h2]\n ring\n have hsumX : Summable (fun m : \u2115 =>\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n (((2 * Real.sqrt (n : \u211d)) : \u211d) : \u2102) m\u2016) := by\n rw [summable_norm_iff]\n apply ArithmeticFunction.LSeriesSummable_vonMangoldt\n rw [show (((2 * Real.sqrt (n : \u211d) : \u211d) : \u2102).re) = 2 * Real.sqrt (n : \u211d) from by simp]\n linarith\n have hsumS : Summable (fun m : \u2115 =>\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) m\u2016) := by\n rw [summable_norm_iff]\n exact ArithmeticFunction.LSeriesSummable_vonMangoldt hs1\n have hle : \u2016LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 \u2264 dirichletCX n := by\n show \u2016\u2211' m : \u2115, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) m\u2016 \u2264 _\n calc \u2016\u2211' m : \u2115, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) m\u2016\n \u2264 \u2211' m : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) m\u2016 :=\n norm_tsum_le_tsum_norm hsumS\n _ \u2264 \u2211' m : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n (((2 * Real.sqrt (n : \u211d)) : \u211d) : \u2102) m\u2016 :=\n Summable.tsum_le_tsum (fun m => LSeries.norm_term_le_of_re_le_re _ (by\n simp) m) hsumS hsumX\n _ = dirichletCX n := rfl\n calc \u2016logDeriv riemannZeta (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016\n = \u2016LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 := by\n rw [\u2190 h1', norm_neg]\n _ \u2264 dirichletCX n := hle\n\n/-- Termwise tail comparison: for m \u2265 3, the term at 2\u221an is \u2264\n3^{\u2212(2\u221an\u22122)}\u00b7(the term at 2). -/\nlemma norm_term_vonMangoldt_X_le_three_pow {n : \u2115} (hn : 1 \u2264 n) {m : \u2115} (hm : 3 \u2264 m) :\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n (((2 * Real.sqrt (n : \u211d)) : \u211d) : \u2102) m\u2016 \u2264\n (3 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) *\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) m\u2016 := by\n have hXre : ((((2 * Real.sqrt (n : \u211d)) : \u211d) : \u2102).re) = 2 * Real.sqrt (n : \u211d) := by simp\n have h2re : ((2 : \u2102).re) = 2 := rfl\n simp only [LSeries.norm_term_eq, hXre, h2re]\n split\n \u00b7 norm_num\n \u00b7 next hm0 =>\n have h\u039b : \u2016(ArithmeticFunction.vonMangoldt m : \u2102)\u2016 =\n ArithmeticFunction.vonMangoldt m :=\n Complex.norm_of_nonneg ArithmeticFunction.vonMangoldt_nonneg\n rw [h\u039b]\n have hm2 : (0 : \u211d) < (m : \u211d) := by exact_mod_cast (by omega : 0 < m)\n have hsqrt2 : (2 : \u211d) \u2264 2 * Real.sqrt (n : \u211d) := by\n have h1 : (1 : \u211d) \u2264 Real.sqrt (n : \u211d) := Real.one_le_sqrt.mpr (by exact_mod_cast hn)\n linarith\n have hexp_nn : (0 : \u211d) \u2264 2 * Real.sqrt (n : \u211d) - 2 := by linarith\n have e : ArithmeticFunction.vonMangoldt m / (m : \u211d) ^ (2 * Real.sqrt (n : \u211d)) =\n (1 / (m : \u211d) ^ (2 * Real.sqrt (n : \u211d) - 2)) *\n (ArithmeticFunction.vonMangoldt m / (m : \u211d) ^ (2 : \u211d)) := by\n rw [show (2 * Real.sqrt (n : \u211d)) = (2 * Real.sqrt (n : \u211d) - 2) + 2 by ring,\n Real.rpow_add hm2]\n field_simp [hm2.ne']\n rw [e]\n have hle : (1 : \u211d) / (m : \u211d) ^ (2 * Real.sqrt (n : \u211d) - 2) \u2264\n (3 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) := by\n rw [Real.rpow_neg (by norm_num : (0 : \u211d) \u2264 3), \u2190 one_div]\n apply one_div_le_one_div_of_le (Real.rpow_pos_of_pos (by norm_num : (0 : \u211d) < 3) _)\n exact Real.rpow_le_rpow (by norm_num : (0 : \u211d) \u2264 3)\n (by exact_mod_cast hm : (3 : \u211d) \u2264 (m : \u211d)) hexp_nn\n have hpos : (0 : \u211d) \u2264 ArithmeticFunction.vonMangoldt m / (m : \u211d) ^ (2 : \u211d) :=\n div_nonneg ArithmeticFunction.vonMangoldt_nonneg\n (Real.rpow_nonneg (by positivity : (0 : \u211d) \u2264 (m : \u211d)) _)\n exact mul_le_mul_of_nonneg_right hle hpos\n\n/-- The split: dirichletCX n = log 2\u00b72^{\u22122\u221an} + (the m \u2265 3 tail). -/\nlemma dirichletCX_le {n : \u2115} (hn : 1 \u2264 n) :\n dirichletCX n \u2264 Real.log 2 * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d))) +\n (3 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * dirichletC2 := by\n have hsumX : Summable (fun m : \u2115 =>\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n (((2 * Real.sqrt (n : \u211d)) : \u211d) : \u2102) m\u2016) := by\n rw [summable_norm_iff]\n apply ArithmeticFunction.LSeriesSummable_vonMangoldt\n rw [show (((2 * Real.sqrt (n : \u211d) : \u211d) : \u2102).re) = 2 * Real.sqrt (n : \u211d) from by simp]\n have h1 : (1 : \u211d) \u2264 Real.sqrt (n : \u211d) := Real.one_le_sqrt.mpr (by exact_mod_cast hn)\n linarith\n have hsplit := tsum_split_finset hsumX {0, 1, 2}\n have hsum2 : Summable (fun m : \u2115 =>\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) m\u2016) := by\n rw [summable_norm_iff]\n exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)\n have hfin : \u2211 i \u2208 ({0, 1, 2} : Finset \u2115),\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n (((2 * Real.sqrt (n : \u211d)) : \u211d) : \u2102) i\u2016 =\n Real.log 2 * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d))) := by\n have hXre : ((((2 * Real.sqrt (n : \u211d)) : \u211d) : \u2102).re) = 2 * Real.sqrt (n : \u211d) := by simp\n rw [Finset.sum_insert (by norm_num), Finset.sum_insert (by norm_num),\n Finset.sum_singleton]\n simp only [LSeries.norm_term_eq, hXre]\n rw [if_pos (by norm_num), if_neg (by norm_num : (1 : \u2115) \u2260 0),\n if_neg (by norm_num : (2 : \u2115) \u2260 0)]\n simp [ArithmeticFunction.vonMangoldt_apply_one]\n have h\u039b2 : \u2016(fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) 2\u2016 = Real.log 2 := by\n show \u2016(ArithmeticFunction.vonMangoldt 2 : \u2102)\u2016 = Real.log 2\n rw [ArithmeticFunction.vonMangoldt_apply_prime Nat.prime_two]\n exact Complex.norm_of_nonneg (by linarith [Real.log_two_gt_d9] : (0 : \u211d) \u2264 Real.log 2)\n rw [h\u039b2]\n have e : (2 : \u211d) ^ (2 * Real.sqrt (n : \u211d)) = (2 : \u211d) ^ (2 * Real.sqrt (n : \u211d)) := rfl\n rw [show Real.log 2 / (2 : \u211d) ^ (2 * Real.sqrt (n : \u211d)) =\n Real.log 2 * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d))) by\n rw [Real.rpow_neg (by norm_num : (0 : \u211d) \u2264 2)]\n field_simp [Real.rpow_pos_of_pos (by norm_num : (0 : \u211d) < 2)\n (2 * Real.sqrt (n : \u211d)).ne']]\n ring\n have htail : (\u2211' i : \u2115, (if i \u2208 ({0, 1, 2} : Finset \u2115) then 0\n else \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n (((2 * Real.sqrt (n : \u211d)) : \u211d) : \u2102) i\u2016)) \u2264\n (3 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * dirichletC2 := by\n have hterm : \u2200 m : \u2115, (if m \u2208 ({0, 1, 2} : Finset \u2115) then 0\n else \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n (((2 * Real.sqrt (n : \u211d)) : \u211d) : \u2102) m\u2016) \u2264\n (3 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) *\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) m\u2016 := by\n intro m\n by_cases hm : m \u2208 ({0, 1, 2} : Finset \u2115)\n \u00b7 rw [if_pos hm]\n positivity\n \u00b7 rw [if_neg hm]\n have hm3 : 3 \u2264 m := by\n have h : m \u2209 ({0, 1, 2} : Finset \u2115) := hm\n simp at h\n omega\n exact norm_term_vonMangoldt_X_le_three_pow hn hm3\n have hsum_tail : Summable (fun m : \u2115 => (if m \u2208 ({0, 1, 2} : Finset \u2115) then 0\n else \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n (((2 * Real.sqrt (n : \u211d)) : \u211d) : \u2102) m\u2016)) := by\n apply Summable.of_norm_bounded hsumX.norm\n intro m\n by_cases hm : m \u2208 ({0, 1, 2} : Finset \u2115) <;> simp [hm]\n calc (\u2211' m : \u2115, (if m \u2208 ({0, 1, 2} : Finset \u2115) then 0\n else \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n (((2 * Real.sqrt (n : \u211d)) : \u211d) : \u2102) m\u2016))\n \u2264 \u2211' m : \u2115, (3 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) *\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) m\u2016 :=\n Summable.tsum_le_tsum hterm hsum_tail (hsum2.mul_left _)\n _ = (3 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * dirichletC2 := by\n rw [dirichletC2, tsum_mul_left]\n calc dirichletCX n\n = \u2211 i \u2208 ({0, 1, 2} : Finset \u2115),\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n (((2 * Real.sqrt (n : \u211d)) : \u211d) : \u2102) i\u2016 +\n \u2211' i : \u2115, (if i \u2208 ({0, 1, 2} : Finset \u2115) then 0\n else \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n (((2 * Real.sqrt (n : \u211d)) : \u211d) : \u2102) i\u2016) := hsplit\n _ \u2264 Real.log 2 * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d))) +\n (3 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * dirichletC2 :=\n add_le_add (le_of_eq hfin) htail\n\n/-- log(9/4) \u2265 0.8109 (via e^{0.8109} = e/e^{0.1891} \u2264 2.25, the tight\ne/e^{small} division-by-partial-sum route). -/\nlemma log_nine_quarters_ge : (0.8109 : \u211d) \u2264 Real.log (9 / 4) := by\n have h01891 : (1.20816 : \u211d) \u2264 Real.exp 0.1891 :=\n le_trans (by norm_num [Finset.sum_range_succ])\n (Real.sum_le_exp_of_nonneg (by norm_num : (0 : \u211d) \u2264 0.1891) 6)\n have h1 : Real.exp 0.8109 = Real.exp 1 / Real.exp 0.1891 := by\n rw [show (0.8109 : \u211d) = 1 - 0.1891 by norm_num, Real.exp_sub, Real.exp_one]\n have h2 : Real.exp 0.8109 \u2264 9 / 4 := by\n rw [h1]\n calc Real.exp 1 / Real.exp 0.1891\n \u2264 2.7182818286 / 1.20816 :=\n div_le_div\u2080 (by norm_num) Real.exp_one_lt_d9.le (by norm_num) h01891\n _ \u2264 9 / 4 := by norm_num\n have h3 := Real.log_le_log (Real.exp_pos _) h2\n rwa [Real.log_exp] at h3\n\n/-- log(4/9) \u2264 \u22120.8109 (the negation). -/\nlemma log_four_ninths_le : Real.log (4 / 9) \u2264 (-0.8109 : \u211d) := by\n have h1 := log_nine_quarters_ge\n have h2 : Real.log (4 / 9) = -Real.log (9 / 4) := by\n rw [show ((4 : \u211d) / 9) = (9 / 4)\u207b\u00b9 by norm_num, Real.log_inv]\n rw [h2]\n linarith [h1]\n\n/-- The certified (4/9)^{\u221an} \u2264 0.164 for \u221an \u2265 2.236. -/\nlemma four_ninths_rpow_sqrt_le {x : \u211d} (hx : (2.236 : \u211d) \u2264 x) :\n (4 / 9 : \u211d) ^ x \u2264 (0.164 : \u211d) := by\n have hlog49 := log_four_ninths_le\n have hlogneg : Real.log (4 / 9) < 0 :=\n Real.log_neg (by norm_num : (0 : \u211d) < 4 / 9) (by norm_num : (4 / 9 : \u211d) < 1)\n have h1 : (4 / 9 : \u211d) ^ x = Real.exp (Real.log (4 / 9) * x) :=\n Real.rpow_def_of_pos (by norm_num : (0 : \u211d) < 4 / 9) x\n rw [h1]\n have h2 : Real.log (4 / 9) * x \u2264 (-1.81316 : \u211d) := by\n have h2a : Real.log (4 / 9) * x \u2264 Real.log (4 / 9) * 2.236 :=\n mul_le_mul_of_nonpos_left hx hlogneg.le\n have h2b : Real.log (4 / 9) * 2.236 \u2264 (-0.8109) * 2.236 :=\n mul_le_mul_of_nonneg_right hlog49 (by norm_num)\n calc Real.log (4 / 9) * x \u2264 Real.log (4 / 9) * 2.236 := h2a\n _ \u2264 (-0.8109) * 2.236 := h2b\n _ \u2264 -1.81316 := by norm_num\n have h3 : Real.exp (-1.81316) \u2264 (0.164 : \u211d) := by\n have hsum : (6.12639 : \u211d) \u2264 Real.exp 1.81316 := by\n calc (6.12639 : \u211d) \u2264 \u2211 i \u2208 Finset.range 7, (1.81316 : \u211d) ^ i / (Nat.factorial i : \u211d) := by\n norm_num [Finset.sum_range_succ]\n _ \u2264 Real.exp 1.81316 :=\n Real.sum_le_exp_of_nonneg (by norm_num : (0 : \u211d) \u2264 1.81316) 7\n rw [show Real.exp (-1.81316) = 1 / Real.exp 1.81316 by\n rw [Real.exp_neg, one_div]]\n calc 1 / Real.exp 1.81316 \u2264 1 / 6.12639 :=\n one_div_le_one_div_of_le (by norm_num : (0 : \u211d) < 6.12639) hsum\n _ \u2264 0.164 := by norm_num\n calc Real.exp (Real.log (4 / 9) * x) \u2264 Real.exp (-1.81316) :=\n Real.exp_le_exp.mpr h2\n _ \u2264 0.164 := h3\n\n/-- The 3^{\u2212(2\u221an\u22122)} = 9\u00b7(4/9)^{\u221an}\u00b72^{\u22122\u221an} identity. -/\nlemma three_pow_neg_two_sqrt_sub_two_eq {n : \u2115} :\n (3 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) =\n 9 * ((4 / 9 : \u211d) ^ Real.sqrt (n : \u211d)) * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d))) := by\n have h9 : Real.log 9 = 2 * Real.log 3 := by\n rw [show (9 : \u211d) = 3 ^ 2 by norm_num, Real.log_pow]\n push_cast\n ring\n have h2 : (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d))) =\n Real.exp (-(Real.log 2) * (2 * Real.sqrt (n : \u211d))) := by\n rw [Real.rpow_def_of_pos (by norm_num : (0 : \u211d) < 2)]\n congr 1\n ring\n have h3 : (3 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) =\n Real.exp (-(Real.log 3) * (2 * Real.sqrt (n : \u211d) - 2)) := by\n rw [Real.rpow_def_of_pos (by norm_num : (0 : \u211d) < 3)]\n congr 1\n ring\n have h49 : (4 / 9 : \u211d) ^ Real.sqrt (n : \u211d) =\n Real.exp (Real.sqrt (n : \u211d) * Real.log (4 / 9)) :=\n Real.rpow_def_of_pos (by norm_num : (0 : \u211d) < 4 / 9) _\n rw [h2, h3, h49]\n have hlog49 : Real.log (4 / 9) = Real.log 2 - Real.log 9 + Real.log 2 := by\n rw [Real.log_div (by norm_num : (4 : \u211d) \u2260 0) (by norm_num : (9 : \u211d) \u2260 0)]\n ring\n rw [hlog49, h9]\n rw [\u2190 Real.exp_add, \u2190 Real.exp_add]\n congr 1\n rw [show (9 : \u211d) = Real.exp (Real.log 9) from (Real.exp_log (by norm_num : (0 : \u211d) < 9)).symm]\n rw [\u2190 Real.exp_add]\n congr 1\n ring\n\n/-- **The I_I zeta charge WITHOUT dirichletC2 \u2264 0.57** (DL-6 capstone):\nfor n \u2265 5, \u2016\u03b6\u2032/\u03b6(2\u221an+it)\u2016 \u2264 0.57\u00b72^{\u2212(2\u221an\u22122)} \u2014 the IIMaj zeta form,\nvia the direct log2-leading + 3^{\u2212(2\u221an\u22122)} tail (dirichletC2 \u2264 1) with\nthe certified (4/9)^{\u221an} \u2264 0.17631 bound at \u221an \u2265 \u221a5. -/\ntheorem norm_logDeriv_zeta_le_iimZeta {n : \u2115} (hn : 5 \u2264 n) {t : \u211d} :\n \u2016logDeriv riemannZeta (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 \u2264\n (0.57 : \u211d) * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) := by\n have hn1 : 1 \u2264 n := by omega\n have h1 := norm_logDeriv_zeta_le_dirichletCX hn1 (t := t)\n have h2 := dirichletCX_le hn1\n have hC2 : dirichletC2 \u2264 1 := dirichletC2_le_one\n have hC2nn : (0 : \u211d) \u2264 dirichletC2 := dirichletC2_nonneg\n have hsqrt5 : (2.236 : \u211d) \u2264 Real.sqrt (n : \u211d) := by\n have hnR : (5 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n have h1 : Real.sqrt 5 \u2264 Real.sqrt (n : \u211d) := Real.sqrt_le_sqrt hnR\n have h2 : (2.236 : \u211d) \u2264 Real.sqrt 5 := by\n rw [Real.le_sqrt (by norm_num) (by norm_num)]\n norm_num\n linarith\n have h49 := four_ninths_rpow_sqrt_le hsqrt5\n have h3 : dirichletCX n \u2264 Real.log 2 * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d))) +\n (3 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) := by\n refine h2.trans ?_\n exact add_le_add_left (mul_le_mul_of_nonneg_left hC2\n (Real.rpow_nonneg (by norm_num) _)) _\n have h4 : (3 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) \u2264\n (1.58679 : \u211d) * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d))) := by\n rw [three_pow_neg_two_sqrt_sub_two_eq]\n calc 9 * ((4 / 9 : \u211d) ^ Real.sqrt (n : \u211d)) * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d)))\n \u2264 9 * (0.17631 : \u211d) * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d))) := by\n apply mul_le_mul_of_nonneg_right _ (Real.rpow_nonneg (by norm_num) _)\n apply mul_le_mul_of_nonneg_left h49 (by norm_num)\n _ = (1.58679 : \u211d) * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d))) := by ring\n have h5 : Real.log 2 * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d))) +\n (3 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) \u2264\n (0.57 : \u211d) * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) := by\n have hlog2 : Real.log 2 \u2264 (0.6932 : \u211d) := Real.log_two_lt_d9.le\n have hpos2 : (0 : \u211d) < (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d))) := by positivity\n have e : (0.57 : \u211d) * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) =\n (2.28 : \u211d) * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d))) := by\n rw [show (-(2 * Real.sqrt (n : \u211d) - 2)) = -2 * Real.sqrt (n : \u211d) + 2 by ring,\n Real.rpow_add (by norm_num : (0 : \u211d) < 2), Real.rpow_two]\n ring\n rw [e]\n calc Real.log 2 * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d))) +\n (3 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2))\n \u2264 0.6932 * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d))) +\n (1.58679 : \u211d) * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d))) := by\n apply add_le_add _ h4\n exact mul_le_mul_of_nonneg_right hlog2 hpos2.le\n _ = (0.6932 + 1.58679 : \u211d) * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d))) := by ring\n _ \u2264 (2.28 : \u211d) * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d))) := by\n apply mul_le_mul_of_nonneg_right _ hpos2.le\n norm_num\n exact h1.trans (h3.trans h5)\n\nend NguyenRH1\n\nend\n",
"structuredPatch": [
{
"oldStart": 1329,
"oldLines": 7,
"newStart": 1329,
"newLines": 7,
"lines": [
" (3 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) := by",
" refine h2.trans ?_",
" exact add_le_add_left (mul_le_mul_of_nonneg_left hC2",
"- (Real.rpow_nonneg (by norm_num) _)) _",
"+ (Real.rpow_nonneg (by norm_num) _)) (Real.log 2 * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d))))",
" have h4 : (3 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) \u2264",
" (1.58679 : \u211d) * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d))) := by",
" rw [three_pow_neg_two_sqrt_sub_two_eq]"
]
}
],
"userModified": false,
"replaceAll": false
}
raw content_json (database row)
[{"type":"thinking","thinking":"Remaining errors:\n\n1. **Line 1118 (X_le_three_pow's `e` at 1117-1122)**: \"unsolved goals\" with context ending at hΛ — the field_simp at 1122 — the `rw [show (2·√↑n) = (2·√↑n−2)+2 by ring, Real.rpow_add hm2]; field_simp [hm2.ne']` — the field_simp's leftover. Hmm — the context shown ends at hΛ (line 1108-1110) — the goal at 1118:68 (the e statement's RHS line). The `field_simp [hm2.ne']` at 1122 — maybe it left goals. Let me look at what e's proof produces: e : Λ m / ↑m ^ (2√↑n) = (1/↑m ^ (2√↑n−2))·(Λ m / ↑m ^ 2) — after rw [show σ-form, rpow_add]: goal becomes Λ m / (↑m^{2√↑n−2}·↑m^2) = (1/↑m^{2√↑n−2})·(Λ m/↑m^2) — field_simp [hm2.ne'] clears ✓ should close by its internal ring ✓ — \"unsolved goals\"?? — hmm, the context shown is from BEFORE e (hΛ at 1108) — the error at 1118:68 is probably the `rw [show ... by ring, Real.rpow_add hm2]` — the rw [Real.rpow_add hm2] — hm2 : 0 < (m:ℝ) — Real.rpow_add (hx : 0 < x) : x ^ (y+z) = x^y · x^z ✓ — hmm.\n\nActually — the context display might be truncated (shows only up to hΛ). The `unsolved goals` with just that context suggests the whole `e` have failed. Let me look at the FULL goal state — I only see context, not the goal. The issue could be `Real.rpow_add hm2` — signature: `Real.rpow_add (hx : 0 < x) (y z : ℝ) : x ^ (y + z) = x ^ y * x ^ z` — with hm2 : 0 < ↑m ✓.\n\nHmm — wait, maybe the problem is the `show (2·√↑n) = (2·√↑n−2)+2 by ring` — 2√↑n = (2√↑n − 2) + 2 ⟺ 0 = −2 ✓?? NO: (2√↑n − 2) + 2 = 2√↑n ✓ ring proves it ✓.\n\nThen `Real.rpow_add hm2` rewrites ↑m^((2√↑n−2)+2) → ↑m^(2√↑n−2)·↑m^2 ✓ then field_simp... The goal at that point: Λ m / (↑m^{2√↑n−2}·↑m^2) = (1/↑m^{2√↑n−2})·(Λ m/↑m^2) — field_simp [hm2.ne'] — clears denominators ✓ should close. \"unsolved goals\" — maybe field_simp left `Λ m = Λ m`?? which closes by rfl automatically...\n\nLet me look at the actual goal text — the sed output only showed context (no ⊢ goal line for 1118). Let me get it.\n\n2. **Line 1166 (hfin's rw [hΛ2])**: pattern `‖(fun n => ↑(Λ n)) 2‖` not found in `|ArithmeticFunction.vonMangoldt 2| / 2 ^ (2·√↑n) = ...` — the target has `|ArithmeticFunction.vonMangoldt 2|` — the norm-term output's norm is displayed as `|...|` — and my hΛ2's pattern is `‖(fun n => ↑(Λ n)) 2‖` — hmm — the goal shows `|ArithmeticFunction.vonMangoldt 2|` — that's `Complex.abs (Λ 2)`?? or the norm ‖·‖ displayed as |·|? — in Lean 4 the norm ‖x‖ prints as `‖x‖` (double bars) or `|x|`?? — Mathlib prints `‖x‖` as `‖x‖` typically... but the display shows `|ArithmeticFunction.vonMangoldt 2|` — single bars — that's `Complex.abs`?? no — it's the NORM of the cast, printed as |x|? Hmm — actually in Lean4/Mathlib, ‖x‖ displays as `‖x‖` usually, but `(‖x‖ : ℝ)` for complex might display as `|x|` — uncertain. The pattern mismatch means the goal's norm form differs from hΛ2's. The `simp [ArithmeticFunction.vonMangoldt_apply_one]` before hΛ2 — simp might have rewritten `‖(fun n => ↑(Λ n)) 2‖` into `|Λ 2|` (some norm-simp form!) — so the goal's norm is in a DIFFERENT form than hΛ2's. Fix: make hΛ2 match the goal's displayed form `|ArithmeticFunction.vonMangoldt 2|` — hmm — what IS that form? `Complex.abs (ArithmeticFunction.vonMangoldt 2)`?? or `‖(ArithmeticFunction.vonMangoldt 2 : ℂ)‖` displayed as |·|? — Complex.abs is DEFINED as the norm (Complex.abs z = ‖z‖ defeq — `Complex.abs z := norm z`?? — actually `Complex.abs` is notation/instance for the norm ✓ defeq). So `|Λ 2|` IS `‖(Λ 2 : ℂ)‖` in another display. My hΛ2's pattern `‖(fun n => ↑(Λ n)) 2‖` — the `(fun n => (↑(Λ n)):ℂ) 2` beta-redex — the goal's `|Λ 2|` is `‖(↑(Λ 2)):ℂ‖` — beta-reduced — MISMATCH (redex vs reduced). rw's matching: does it see through beta-redexes? NO. Fix: state hΛ2 with the beta-reduced form `‖(ArithmeticFunction.vonMangoldt 2 : ℂ)‖`... — wait, that's what I had ORIGINALLY and the 1168 error said pattern `‖↑(Λ 2)‖` not found in `|Λ 2| / ...` — the SAME display!! So `‖(ArithmeticFunction.vonMangoldt 2 : ℂ)‖` doesn't match `|ArithmeticFunction.vonMangoldt 2|` either?! — the display `|...|` vs `‖...‖` — if they were the same term, rw would match regardless of display. So the goal's norm is genuinely DIFFERENT: it must be `Complex.abs`?? no wait — or `Real.norm_eq_abs`-style `|x|` for a REAL?? — `|ArithmeticFunction.vonMangoldt 2|` — if Λ 2 is REAL, then `|Λ 2|` is Real.abs!! — the norm_term_eq produces `‖f n‖` with f n : ℂ — but simp might have rewritten the ℂ-norm of the real cast to the REAL abs: `Complex.norm_ofReal : ‖(x : ℂ)‖ = |x|`?? no wait — simp [vonMangoldt_apply_one] — that lemma is about Λ 1 — shouldn't touch Λ 2's norm form. Hmm — unless norm_term_eq's `‖f n‖` with f n = (↑(Λ n)):ℂ — the simp normalized it to `|Λ 2|`... \n\nLet me check what the term actually is: the goal at 1166 is `|ArithmeticFunction.vonMangoldt 2| / 2 ^ (2·√↑n) = Real.log 2 * 2 ^ (-(2·√↑n))`. The `|...|` — hmm — actually in Mathlib 4, `‖(x : ℂ)‖` for a REAL-VALUED complex number — the norm — prints as `‖x‖`. `|x|` is for Real/Int abs OR `Complex.abs` (which is a DEF := norm?). Actually — `Complex.abs z` is defined as `norm z`?? No — `Complex.abs (z : ℂ) : ℝ := norm z`?? Hmm — Complex.abs is `abs z := Real.sqrt (normSq z)`?? — historically Complex.abs was its own definition but in current Mathlib `Complex.abs = norm` defeq. The display `|...|` for complex norms IS used for `Complex.abs`. Since norm_term_eq's norm is the normed-field norm ‖·‖, the display should be ‖·‖...\n\nOK regardless — the issue is beta-redex vs reduced. The goal's `|Λ 2|` is the BETA-REDUCED norm ‖↑(Λ 2)‖ — and my hΛ2's pattern has the redex `(fun n => ↑(Λ n)) 2`. Fix: make hΛ2's LHS match the goal — state hΛ2 as `‖(ArithmeticFunction.vonMangoldt 2 : ℂ)‖ = Real.log 2`... — but that's what the ORIGINAL had and it failed too (1168 error: pattern `‖↑(Λ 2)‖` not found in `|Λ 2| / ...`). So `‖(ArithmeticFunction.vonMangoldt 2 : ℂ)‖` ≠ the goal's `|ArithmeticFunction.vonMangoldt 2|`?? — those should be the SAME term (cast of Λ 2, normed). UNLESS the goal's `|Λ 2|` is `Real.abs (ArithmeticFunction.vonMangoldt 2)` — REAL abs — meaning simp rewrote the complex norm of the real cast to a REAL abs — `Complex.norm_ofReal : ‖(x : ℂ)‖ = |x|` — is that a simp lemma?? — `Complex.norm_ofReal (x : ℝ) : ‖(x : ℂ)‖ = |x|` — might be simp-tagged!! So after `simp [vonMangoldt_apply_one]`, the norm became `|Λ 2|` (real abs of the real Λ 2). Then the correct hΛ2 form: `|ArithmeticFunction.vonMangoldt 2| = Real.log 2` — via abs_of_nonneg: `abs_of_nonneg (h : 0 ≤ a) : |a| = a` ✓ — with Λ 2 = log 2 ≥ 0 ✓:\n```\n have hΛ2 : |ArithmeticFunction.vonMangoldt 2| = Real.log 2 := by\n rw [ArithmeticFunction.vonMangoldt_apply_prime Nat.prime_two]\n exact abs_of_nonneg (by linarith [Real.log_two_gt_d9] : (0 : ℝ) ≤ Real.log 2)\n rw [hΛ2]\n```\nabs_of_nonneg (hx : 0 ≤ x) : |x| = x ✓.\n\nHmm — but the goal might not have gone through norm_ofReal — the display `|...|` might just be how Lean prints ‖·‖ for these. The safest: match the goal's EXACT form — since the goal displays `|ArithmeticFunction.vonMangoldt 2|`, and if it's ‖(Λ 2 : ℂ)‖ the hΛ2 with `‖(Λ 2 : ℂ)‖` should match... it didn't. So it's the Real abs. Use the abs form.\n\nActually — hmm, `LSeries.norm_term_eq` produces `‖f n‖ / n ^ s.re` with f n : ℂ and the norm being the ℂ norm — the display as `|...|` is probably just the pretty-printer for ‖·‖ on complex with real content?? I'm not sure. Try both: if `‖(Λ 2 : ℂ)‖` fails and `|Λ 2|` (Real abs) works, use the abs. The previous hΛ2 edit used `(fun n => (↑(Λ n)):ℂ) 2` — redex — fails. The goal's form is beta-reduced. Use:\n```\n have hΛ2 : (‖(ArithmeticFunction.vonMangoldt 2 : ℂ)‖ : ℝ) = Real.log 2 := by\n rw [ArithmeticFunction.vonMangoldt_apply_prime Nat.prime_two,\n Complex.norm_of_nonneg (by linarith [Real.log_two_gt_d9] : (0 : ℝ) ≤ Real.log 2)]\n```\nif the goal's |·| is the ℂ norm — if it's Real.abs, use abs_of_nonneg. Ugh — let me determine which by probing: the display in the error: `|ArithmeticFunction.vonMangoldt 2| / 2 ^ (2 * √↑n)` — in Lean 4, the pretty printer renders `‖x‖` as `‖x‖` and `|x|` for Real.abs — a complex norm of a REAL-number-typed expression: Λ 2 : ℝ cast to ℂ, its norm is ℂ-norm, rendered `‖↑(Λ 2)‖` usually. The error displays `|ArithmeticFunction.vonMangoldt 2|` — single bars with the REAL Λ 2 inside (not `↑(Λ 2)` cast!) — so it IS Real.abs (the argument is the REAL vonMangoldt 2, not the complex cast). So simp rewrote ‖↑(Λ 2)‖ → |Λ 2| (via Complex.norm_ofReal as a simp lemma — wait — `Complex.norm_ofReal : ‖(x : ℂ)‖ = |x|`?? — hmm, actually it's `Complex.norm_ofReal (x : ℝ) : ‖(x : ℂ)‖ = ‖x‖`?? — there's `Complex.norm_ofReal` and also the simp might use `Complex.abs_ofReal`... whatever — the goal has the REAL abs form.\n\nFix hΛ2 as `|ArithmeticFunction.vonMangoldt 2| = Real.log 2` with abs_of_nonneg ✓.\n\n3. **Line 1235 (log_nine_quarters_ge's rwa)**: \"Tactic `assumption` failed\" — the rwa [Real.log_exp] at h2 — h2 : log(9/4) ≤ 0.811 — the GOAL of log_nine_quarters_ge is `(0.811 : ℝ) ≤ Real.log (9 / 4)` — h2 gives the WRONG DIRECTION (log(9/4) ≤ 0.811 vs goal 0.811 ≤ log(9/4))!! — I proved log(9/4) ≤ 0.811 but the lemma wants 0.811 ≤ log(9/4). And Real.log_le_log (0 < 9/4) (hprod : 9/4 ≤ exp 0.811) : log(9/4) ≤ log(exp 0.811) = 0.811 — that's log(9/4) ≤ 0.811 — WRONG direction again! I need 9/4 ≤ exp 0.811 ⟹ log(9/4) ≤ 0.811 — hmm — but I want log(9/4) ≥ 0.811 — which needs exp 0.811 ≤ 9/4?? NO: log(9/4) ≥ 0.811 ⟺ 9/4 ≥ e^{0.811} ⟺ e^{0.811} ≤ 2.25!! — I had it BACKWARD: log(9/4) ≥ 0.811 ⟺ e^{0.811} ≤ 9/4 — the hprod should be `Real.exp 0.811 ≤ 9/4`?? — wait: log x ≥ 0.811 ⟺ x ≥ e^{0.811} — so 9/4 ≥ e^{0.811} ⟹ log(9/4) ≥ 0.811 ✓. And e^{0.811} ≤ 2.2254·1.01106·... — wait, e^{0.811} = e^{0.8}·e^{0.011} ≤ ??? — for an UPPER bound on e^{0.811}: e^{0.8} ≤ 2.2256?? — hmm — my h08 is `(2.2254 : ℝ) ≤ Real.exp 0.8` (LOWER bound on exp!). For e^{0.811} ≤ 9/4 I need e^{0.811} ≤ 2.25 ⟸ e^{0.8}·e^{0.011} ≤ 2.25 — upper bounds: e^{0.8} ≤ 2.2256 (upper) and e^{0.011} ≤ 1.01107: product ≤ 2.2501 — too fat?? — 2.2256·1.01107 = 2.25023 > 2.25 ✗. Hmm — but the TRUE e^{0.811} = 2.24995 < 2.25 ✓ — slack 0.00005. The certification needs e^{0.811} ≤ 2.25 with slack 5e-5: e^{0.8} ≤ 2.22554 (true 2.2255409) and e^{0.011} ≤ 1.0110607 (true 1.0110607): product 2.25014 > 2.25 ✗ — the upper bounds are too fat individually. Split differently: e^{0.811} ≤ 2.25 ⟺ 0.811 ≤ log 2.25 ⟺ ... — or bound e^{0.811} directly via the partial-sum LOWER bound?? — for UPPER bounds on e^x (x > 0): the (1−x/16)⁻¹⁶ trick: e^{0.811} ≤ (1−0.811/16)⁻¹⁶ = (0.9493125)⁻¹⁶ = (1.05339...)^16: ln: −16·ln(0.9493125) = 16·0.052011 = 0.832176: e^{0.832176} = 2.29843 — way too fat (true 2.24995). e^{0.811} = e^{0.8}·e^{0.011}: e^{0.8} ≤ (1−0.8/16)⁻¹⁶ = (0.95)⁻¹⁶ = (1.052632)¹⁶ = e^{16·0.0512933} = e^{0.820693} = 2.27206 — fat. e^{0.8} ≤ 2.2256 via partial sums?? — partial sums give LOWER bounds (Σ ≤ e^x). For UPPER bounds at x > 0 the only tool is the (1−x/16)⁻¹⁶ (fat at x ~ 0.8).\n\nAlternative: e^{0.811} ≤ 2.25 ⟺ 0.811 ≤ log 2.25: certify log(9/4) ≥ 0.811 directly via log's Taylor/integral?? — or via e^{0.811} ≤ 2.25 with a better decomposition: e^{0.811} = e^{0.75}·e^{0.061}: e^{0.75} ≤ 2.1170 (upper via trick: (1−0.75/16)⁻¹⁶ = (0.953125)⁻¹⁶ = (1.049180)¹⁶ = e^{16·0.048008} = e^{0.768131} = 2.15579 — fat). e^{0.75} ≥ 2.1169 (the h075 from LiBasePoints ✓). Ugh — upper bounds on exp are systematically fat with this machinery.\n\nDIFFERENT approach for log(9/4) ≥ 0.811: use log(9/4) = log 9 − log 4 = 2(log 3 − log 2) — log 3 ≥ 1.0987 (needs e^{1.0987} ≤ 3: e^{1.0987} = e·e^{0.0987} ≤ 2.7182818·1.10373 = 2.99997 ≤ 3 ✓ — e^{0.0987} ≤ 1.10373 via partial... — e^{0.0987}: partial sums give LOWER bound 1+0.0987+0.004871+0.000160 = 1.103731 — that's LOWER; UPPER via trick (1−0.0987/16)⁻¹⁶ = (0.993831)⁻¹⁶ = e^{16·0.006188} = e^{0.099014} = 1.104083 — then e^{1.0987} ≤ 2.7182818·1.104083 = 3.001342 ≥ 3 ✗ fat again!!) — hmm — the e^small upper bounds keep overshooting the tight thresholds.\n\nHmm hmm. Let me think about what log-bound directions the machinery CAN do tightly:\n- log x ≥ B ⟺ x ≥ e^B ⟸ e^B ≤ x — needs e^B ≤ x certified: partial-sum LOWER bounds on e^B (tight!): e^B ≥ Σ₀ᴷ B^i/i! — with enough terms this is TIGHT (error ~B^{K+1}/(K+1)! tiny). For B = 0.811: Σ₀⁹(0.811^i/i!) = ? — the tail beyond 9: 0.811^10/10! ~ 0.811^10/3628800 ~ 0.125/3628800 ~ 3.4e-8 — plus the geometric continuation — the partial sum Σ₀⁹ ≈ e^{0.811} − ~5e-8 ≈ 2.24990. So e^{0.811} ≥ 2.2499 — that's a LOWER bound (e^B ≥ partial). For e^B ≤ x (x = 2.25): need e^{0.811} ≤ 2.25 — the lower bound 2.2499 ≤ 2.25 doesn't give it.\n\nFor log x ≥ B, the cleanest tight route: x·e^{−B} ≥ 1 ⟺ ... no. OR use log(1+y) ≥ y − y²/2 (the standard log bound): log(9/4) = log(1+5/4) with y = 5/4 > 1 — the y−y²/2 bound fails for y > 1. log(9/4) = log 9 − log 4: log 9 = 2 log 3, log 4 = 2 log 2: = 2(log 3 − log 2). log 3 ≥ 1.098612 (certifiable tightly how?): log 3 ≥ B ⟺ 3 ≥ e^B: e^{1.0986} ≥ Σ₀⁹(1.0986^i/i!) — tight partial ≈ e^{1.0986} − small ≈ 2.9996 ≤ 3 ✓!! — e^{1.0986} ≤ 3 certified by the partial sum giving e^{1.0986} ≥ ... — NO — the partial sum is a LOWER bound on e^B: e^{1.0986} ≥ 2.9996 — that says e^{1.0986} is AT LEAST 2.9996 — for e^{1.0986} ≤ 3 I need an UPPER bound. DAMN.\n\nFor log x ≥ B (lower bound on log): x ≥ e^B — I need e^B ≤ x — UPPER bound on e^B. The partial sums give lower bounds only. The (1−x/16)⁻¹⁶ trick gives upper bounds but FAT (error ~(x/16)·16·(x/2)·... = x²/32·... ≈ x²/32·1 = for x = 1.0986: 1.0986²/32 = 0.0377 (3.7% fat) — e^{1.0986} ≤ 2.9996·1.0377 = 3.1127 ≥ 3 ✗ USELESS.\n\nHmm — so how did LiBasePoints certify log 80000 ≥ 11.263?! Line 83: `log80000_ge : (11.263 : ℝ) ≤ Real.log 80000 := by have h1 : Real.exp 11 ≤ 59874.31; have h2 : Real.exp 0.263 ≤ 1.3037; ...` — e^{11.263} = e^{11}·e^{0.263} ≤ 59874.31·1.3037 = 78057 ≤ 80000 ✓ — e^{11} ≤ 59874.31 (upper via exp_one_pow_le 11 : e^11 = (e^1)^11 ≤ 2.7182818286^11 = 59874.30...) ✓ and e^{0.263} ≤ 1.3037 via the (1−x/16)⁻¹⁶ trick (small x = 0.263: trick error ~(0.263²/32)·... = 0.0022 (0.22%) ✓ acceptable there). So the trick works for SMALL x (≤ 0.3). For x = 0.811 the trick's error is ~2-4% — too fat for my 5e-5 slack.\n\nFor log(9/4) ≥ 0.811: write it as log(9/4) = log 9 − log 4 with log 9 ≥ 2.1972 and log 4 ≤ 1.3863: log(9/4) ≥ 2.1972 − 1.3863 = 0.8109 ≥ 0.811?? — 0.8109 < 0.811 ✗!!! — log(9/4) = 0.8109302 < 0.811 — WAIT — is 0.8109302 < 0.811? YES! So log(9/4) ≥ 0.811 is FALSE!!! Let me recompute: log(9/4) = log 2.25 = 0.810930216... — indeed < 0.811!! So my target bound is WRONG. Use 0.8109 instead: log(9/4) ≥ 0.8109 ⟺ 9/4 ≥ e^{0.8109}: e^{0.8109} = e^{0.8}·e^{0.0109}: e^{0.8} ≥ 2.2254 (h08 ✓), e^{0.0109} ≥ 1.01096 (partial): product ≥ 2.2254·1.01096 = 2.249795?? — that's e^{0.8109} ≥ 2.249795 — and I need e^{0.8109} ≤ 2.25 for log(9/4) ≥ 0.8109?? — NO WAIT: log(9/4) ≥ 0.8109 ⟺ 9/4 = 2.25 ≥ e^{0.8109} — the partial gives e^{0.8109} ≥ 2.249795 ≤ 2.25 ✓?? — the LOWER bound on exp is ≤ the true exp ≤ 2.25 ✓ but that's the LOWER bound, not the value — I need the VALUE ≤ 2.25 — the lower bound 2.249795 < 2.25 doesn't certify the value ≤ 2.25!! ARGH — same issue: certifying e^B ≤ x needs UPPER bounds on e^B.\n\nHmm OK wait — let me reconsider. log(9/4) ≥ 0.8109 ⟺ e^{0.8109} ≤ 2.25. To certify e^{0.8109} ≤ 2.25: e^{0.8109} = e^{0.8}·e^{0.0109}: e^{0.8} ≤ UPPER(0.8), e^{0.0109} ≤ UPPER(0.0109): need UPPER(0.8)·UPPER(0.0109) ≤ 2.25. e^{0.8} upper via trick: 2.27206 (fat) ✗. e^{0.8} upper another way: e^{0.8} = e/e^{0.2}: e ≤ 2.7182818286 (d9 ✓); e^{0.2} ≥ Σ₀⁷(0.2^i/i!) = 1+0.2+0.02+0.0013333+0.0000667+0.00000267+0.0000000893+0.00000000255 = 1.2214027 (LOWER ✓): e^{0.8} ≤ 2.7182818286/1.2214027 = 2.22554 ✓✓ TIGHT!! (the e/e^{small} trick — divide by a tight LOWER bound!). Then e^{0.8109} ≤ 2.22554·UPPER(0.0109): e^{0.0109} ≤ (1−0.0109/16)⁻¹⁶ = (0.999319)⁻¹⁶ = e^{16·0.000681} = e^{0.010899} = 1.01096 — tight (small x)! Product: 2.22554·1.01096 = 2.24992 ≤ 2.25 ✓✓✓ (slack 0.00008 — tight but works!).\n\nActually even simpler: e^{0.8109} = e/e^{0.1891}: e^{0.1891} ≥ Σ₀⁶(0.1891^i/i!) = 1+0.1891+0.01788+0.001127+0.0000533+0.00000202 = 1.20816: e^{0.8109} ≤ 2.7182818286/1.20816 = 2.25000 ≤ 2.25 ✓ (slack ~0.000005 — VERY tight — check: 2.7182818286/1.20816 = 2.249994 ≤ 2.25 ✓ norm_num can verify 2.249994·1.20816 ≤ 2.25·... hmm — the division bound: e/e^{0.1891} ≤ 2.7182818286/1.20816 ⟸ e^{0.1891} ≥ 1.20816 ✓ (partial ✓): then 2.7182818286/1.20816 ≤ 2.25 ⟺ 2.7182818286 ≤ 2.25·1.20816 = 2.71836 ✓ (2.7182818 ≤ 2.71836 ✓ norm_num ✓).\n\nSo the cleanest: log(9/4) ≥ 0.8109 via e^{0.8109} = e/e^{0.1891} ≤ 2.7182818286/1.20816 ≤ 2.25 ✓. And log(4/9) = −log(9/4) ≤ −0.8109. Then (4/9)^{√n} ≤ e^{−0.8109·2.236} = e^{−1.8131}·... — the final assembly needs log2 + 9·(4/9)^{√n} ≤ 2.28: (4/9)^{√n} ≤ e^{−0.8109·2.236} = e^{−1.81317}: 1/e^{1.81317} ≤ 1/5.6721-ish — e^{1.81317} ≥ Σ₀⁷(1.81317^i/i!) = 1+1.81317+1.64379+0.99354+0.45042+0.16334+0.04937+0.01279 = 6.12642 ≥ 5.6721 ✓: (4/9)^{√n} ≤ 1/6.12642·... hmm wait — (4/9)^{√n} = e^{√n·log(4/9)} ≤ e^{2.236·log(4/9)} (base < 1, exponent ≥ 2.236 ✓) ≤ e^{2.236·(−0.8109)} = e^{−1.81317} ≤ 1/6.12642 = 0.16323?? — 1/6.12642 = 0.163227 — vs my target 0.17631: 0.16323 ≤ 0.17631 ✓ fine (tighter). Then 9·(4/9)^{√n} ≤ 9·0.16323 = 1.46907: log2 + 9·(4/9)^{√n} ≤ 0.6932+1.46907 = 2.16227 ≤ 2.28 ✓✓ LOTS of slack.\n\nHmm wait — but I need (4/9)^{√n} ≤ 0.17631-ish for the assembly log2 + 9·(4/9)^{√n} ≤ 2.28: with the tighter 0.16323: 0.6932+1.46907 = 2.16227 ≤ 2.28 ✓ big slack. But the (4/9)^{√n} bound's OWN statement: (4/9)^{√n} ≤ 0.16323 — hmm — let me re-derive: (4/9)^{√n} ≤ (4/9)^{2.236} = e^{2.236·log(4/9)} ≤ e^{2.236·(−0.8109)} = e^{−1.81316}: certify e^{−1.81316} ≤ 0.16323 ⟺ e^{1.81316} ≥ 1/0.16323 = 6.1264: e^{1.81316} ≥ Σ₀⁷(1.81316^i/i!) ≈ 6.1264-ish: partial: 1+1.81316+1.64378+0.99353+0.45042+0.16334+0.04937+0.01279 = 6.12639 ≥ 6.1264?? — 6.12639 < 6.1264 ✗ TIGHT-FAIL. Use more terms or relax to 0.1635: 1/6.12639 = 0.163230 ≤ 0.1635 ✓: then (4/9)^{√n} ≤ 0.1635, 9·0.1635 = 1.4715, log2+1.4715 = 2.1647 ≤ 2.28 ✓✓.\n\nHmm — this is getting fiddly. Let me just relax the (4/9) bound to something comfortable: (4/9)^{√n} ≤ 0.164 (from e^{1.81316} ≥ 6.12639 ⟹ e^{−1.81316} ≤ 1/6.12639 = 0.163230 ≤ 0.164 ✓ big slack): 9·0.164 = 1.476, +0.6932 = 2.1692 ≤ 2.28 ✓✓.\n\nAnd log(9/4) ≥ 0.8109 via the e/e^{0.1891} route. Let me rewrite log_nine_quarters_ge cleanly:\n\n```\nlemma log_nine_quarters_ge : (0.8109 : ℝ) ≤ Real.log (9 / 4) := by\n -- e^{0.8109} = e/e^{0.1891} ≤ 2.7182818286/1.20816 ≤ 2.25\n have h01891 : (1.20816 : ℝ) ≤ Real.exp 0.1891 :=\n le_trans (by norm_num [Finset.sum_range_succ])\n (Real.sum_le_exp_of_nonneg (by norm_num : (0 : ℝ) ≤ 0.1891) 6)\n have h1 : Real.exp 0.8109 = Real.exp 1 / Real.exp 0.1891 := by\n rw [show (0.8109 : ℝ) = 1 - 0.1891 by norm_num, Real.exp_sub, Real.exp_one]\n have h2 : Real.exp 0.8109 ≤ 9 / 4 := by\n rw [h1]\n calc Real.exp 1 / Real.exp 0.1891\n ≤ 2.7182818286 / 1.20816 :=\n div_le_div₀ Real.exp_one_lt_d9.le h01891 (by norm_num) (by norm_num)\n _ ≤ 9 / 4 := by norm_num\n have h3 := Real.log_le_log (Real.exp_pos _) h2\n rwa [Real.log_exp] at h3\n```\ndiv_le_div₀ (hc : 0 ≤ c) (hac : a ≤ c) (hd : 0 < d) (hdb : d ≤ b) : a/b ≤ c/d ✓ — with a := exp 1, b := exp 0.1891, c := 2.7182818286, d := 1.20816: div_le_div₀ (by norm_num : 0 ≤ 2.7182818286) Real.exp_one_lt_d9.le (by norm_num : (0:ℝ) < 1.20816) h01891?? — div_le_div₀'s signature: div_le_div₀ (hc : 0 ≤ c) (hac : a ≤ c) (hd : 0 < d) (hdb : d ≤ b) : a / b ≤ c / d — the args: hc : 0 ≤ c = 2.7182818286 ✓ norm_num; hac : a ≤ c := exp 1 ≤ 2.7182818286 = Real.exp_one_lt_d9.le ✓; hd : 0 < d = 1.20816 ✓ norm_num; hdb : d ≤ b := 1.20816 ≤ exp 0.1891 = h01891 ✓. Then 2.7182818286/1.20816 ≤ 9/4 ⟺ 2.7182818286·4 ≤ 9·1.20816 ⟺ 10.8731273 ≤ 10.87344 ✓ norm_num ✓.\n\nWait — div_le_div₀ signature order: (hc : 0 ≤ c) (hac : a ≤ c) (hd : 0 < d) (hdb : d ≤ b) — hmm from the earlier grep: `lemma div_le_div₀ (hc : 0 ≤ c) (hac : a ≤ c) (hd : 0 < d) (hdb : d ≤ b) : a / b ≤ c / d` ✓ — so args are (hc, hac, hd, hdb) ✓.\n\nAnd h3 := Real.log_le_log (Real.exp_pos _) h2 — log_le_log (hx : 0 < x) (hxy : x ≤ y)?? — for log(exp 0.8109) ≤ log(9/4): need `Real.log_le_log (h1 : 0 < exp 0.8109) (h2 : exp 0.8109 ≤ 9/4)` : log(exp 0.8109) ≤ log(9/4) ✓ then rw [Real.log_exp] at h3 : 0.8109 ≤ log(9/4) ✓✓ — the goal of log_nine_quarters_ge : (0.8109 : ℝ) ≤ Real.log (9 / 4) ✓ rwa closes ✓.\n\nThen log_four_ninths_le : log(4/9) = −log(9/4) ≤ −0.8109.\n\nAnd four_ninths_rpow_sqrt_le with target 0.164:\n```\nlemma four_ninths_rpow_sqrt_le {x : ℝ} (hx : (2.236 : ℝ) ≤ x) :\n (4 / 9 : ℝ) ^ x ≤ (0.164 : ℝ) := by\n ... h2 : Real.log (4 / 9) * x ≤ (-1.81316 : ℝ) := ...\n have h3 : Real.exp (-1.81316) ≤ (0.164 : ℝ) := by\n have hsum : (6.12639 : ℝ) ≤ Real.exp 1.81316 := by\n calc (6.12639 : ℝ) ≤ ∑ i ∈ Finset.range 7, (1.81316 : ℝ) ^ i / (Nat.factorial i : ℝ) := by\n norm_num [Finset.sum_range_succ]\n _ ≤ Real.exp 1.81316 := Real.sum_le_exp_of_nonneg (by norm_num) 7\n rw [show Real.exp (-1.81316) = 1 / Real.exp 1.81316 by rw [Real.exp_neg, one_div]]\n calc 1 / Real.exp 1.81316 ≤ 1 / 6.12639 := one_div_le_one_div_of_le (by norm_num) hsum\n _ ≤ 0.164 := by norm_num\n ...\n```\n1/6.12639 = 0.1632302 ≤ 0.164 ✓ norm_num ✓.\n\nAnd the h2's constant: 2.236·(−0.8109) = −1.81316 — h2b : Real.log(4/9)·2.236 ≤ (−0.8109)·2.236 = −1.81316 ✓.\n\nLet me now rewrite these three lemmas cleanly (replace the broken versions). Also fix the remaining errors:\n\n4. **Line 1297 (three_pow_neg identity's rpow_def_of_pos)**: type mismatch with the norm_num-generated positivity proof — `Real.rpow_def_of_pos (by norm_num : (0 : ℝ) < 4 / 9) x` — the elaborated term's type mismatch — hmm — the error shows a giant norm_num proof term — maybe rpow_def_of_pos's signature differs: `Real.rpow_def_of_pos (hx : 0 < x) (y : ℝ) : x ^ y = Real.exp (Real.log x * y)` ✓ — hmm, maybe the issue is rpow_def_of_pos has implicit y and the application order... — the error at 1297:4 \"Type mismatch\" with the huge term — probably the (by norm_num : (0:ℝ) < 4/9) elaborated to a proof of something else (0 < 4/9 as NNRat division — the norm_num proves it ✓ should be fine). The mismatch is downstream (cascade). Let me look after fixing the others.\n\n5. **Line 1346 (h5's hlog2)**: `Real.log_two_lt_d9.le` has type `log 2 ≤ 0.6931471808` but expected `log 2 ≤ 0.6932` — log_two_lt_d9 gives the d9 bound 0.6931471808 — my 0.6932 ≠ 0.6931471808! Fix: use the d9 constant 0.6931471808 in the h5's assembly (0.6931471808 + 9·0.164 = 0.6931471808+1.476 = 2.1691471808 ≤ 2.28 ✓).\n\n6. **Line 1334 (norm_logDeriv_zeta_le_iimZeta's h3 add_le_add_left)**: \"unsolved goals\" — add_le_add_left (mul_le_mul_of_nonneg_left hC2 ...) _ — the h3's form: dirichletCX ≤ log2·2^{−2√n} + 3^{−(2√n−2)}·dirichletC2 — h2 gives that; h3 wants dirichletCX ≤ log2·2^{−2√n} + 3^{−(2√n−2)}·... — wait, h3's stated form: `dirichletCX n ≤ Real.log 2 * 2^{−(2√n)} + (3:ℝ)^{−(2√n−2)}` — but h2 gives `... + 3^{−(2√n−2)} * dirichletC2` — the refine h2.trans ?_ expects `log2·2^{−2√n} + 3^{−(2√n−2)}·dirichletC2 ≤ log2·2^{−2√n} + 3^{−(2√n−2)}` — via add_le_add_left (mul_le_mul_of_nonneg_left hC2 (rpow_nonneg) : 3^{−(2√n−2)}·dirichletC2 ≤ 3^{−(2√n−2)}·1) _ — the `_` at the end — add_le_add_left (h : b ≤ c) (a : α) : a + b ≤ a + c ✓ — the trailing `_` should be the `a` = `Real.log 2 * 2^{−(2√n)}` ✓ — hmm, mul_le_mul_of_nonneg_left : a ≤ b → 0 ≤ c → c·a ≤ c·b — with c := 3^{−(2√n−2)}, a := dirichletC2, b := 1: gives 3^{−(2√n−2)}·dirichletC2 ≤ 3^{−(2√n−2)}·1 ✓ — and add_le_add_left that _ ✓. The \"unsolved goals\" might be a cascade. Let me look after the other fixes.\n\nLet me now rewrite the three problem lemmas (log_nine_quarters_ge, log_four_ninths_le, four_ninths_rpow_sqrt_le) cleanly and fix the remaining spots.","signature":""},{"type":"text","text":"Key realization: `log(9/4) = 0.81093 < 0.811` — my constant was wrong. Rewriting the three certification lemmas with the e/e^{0.1891} tight route and bound 0.8109, plus the remaining fixes."},{"type":"tool_use","id":"Edit_443","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDogLeg.lean","old_string":"/-- log(9/4) ≥ 0.811 (via e^{0.811} ≥ 9/4 with e^{0.8} ≥ 2.2254). -/\nlemma log_nine_quarters_ge : (0.811 : ℝ) ≤ Real.log (9 / 4) := by\n have h08 : (2.2254 : ℝ) ≤ Real.exp 0.8 :=\n le_trans (by norm_num [Finset.sum_range_succ])\n (Real.sum_le_exp_of_nonneg (by norm_num : (0 : ℝ) ≤ 0.8) 7)\n have h011 : (1.01106 : ℝ) ≤ Real.exp 0.011 :=\n le_trans (by norm_num [Finset.sum_range_succ])\n (Real.sum_le_exp_of_nonneg (by norm_num : (0 : ℝ) ≤ 0.011) 4)\n have hprod : (9 / 4 : ℝ) ≤ Real.exp 0.8 * Real.exp 0.011 := by\n calc (9 / 4 : ℝ) = 2.25 := by norm_num\n _ ≤ 2.2254 * 1.01106 := by norm_num\n _ ≤ Real.exp 0.8 * Real.exp 0.011 :=\n mul_le_mul h08 h011 (by norm_num : (0 : ℝ) ≤ 1.01106) (Real.exp_pos _).le\n have h1 : Real.exp 0.811 = Real.exp 0.8 * Real.exp 0.011 := by\n rw [show (0.811 : ℝ) = 0.8 + 0.011 by norm_num, Real.exp_add]\n rw [← h1] at hprod\n have h2 := Real.log_le_log (by norm_num : (0 : ℝ) < 9 / 4) hprod\n rwa [Real.log_exp] at h2\n\n/-- log(4/9) ≤ −0.811 (the negation). -/\nlemma log_four_ninths_le : Real.log (4 / 9) ≤ (-0.811 : ℝ) := by\n have h1 := log_nine_quarters_ge\n have h2 : Real.log (4 / 9) = -Real.log (9 / 4) := by\n rw [show ((4 : ℝ) / 9) = (9 / 4)⁻¹ by norm_num, Real.log_inv]\n rw [h2]\n linarith [h1]","new_string":"/-- log(9/4) ≥ 0.8109 (via e^{0.8109} = e/e^{0.1891} ≤ 2.25, the tight\ne/e^{small} division-by-partial-sum route). -/\nlemma log_nine_quarters_ge : (0.8109 : ℝ) ≤ Real.log (9 / 4) := by\n have h01891 : (1.20816 : ℝ) ≤ Real.exp 0.1891 :=\n le_trans (by norm_num [Finset.sum_range_succ])\n (Real.sum_le_exp_of_nonneg (by norm_num : (0 : ℝ) ≤ 0.1891) 6)\n have h1 : Real.exp 0.8109 = Real.exp 1 / Real.exp 0.1891 := by\n rw [show (0.8109 : ℝ) = 1 - 0.1891 by norm_num, Real.exp_sub, Real.exp_one]\n have h2 : Real.exp 0.8109 ≤ 9 / 4 := by\n rw [h1]\n calc Real.exp 1 / Real.exp 0.1891\n ≤ 2.7182818286 / 1.20816 :=\n div_le_div₀ (by norm_num) Real.exp_one_lt_d9.le (by norm_num) h01891\n _ ≤ 9 / 4 := by norm_num\n have h3 := Real.log_le_log (Real.exp_pos _) h2\n rwa [Real.log_exp] at h3\n\n/-- log(4/9) ≤ −0.8109 (the negation). -/\nlemma log_four_ninths_le : Real.log (4 / 9) ≤ (-0.8109 : ℝ) := by\n have h1 := log_nine_quarters_ge\n have h2 : Real.log (4 / 9) = -Real.log (9 / 4) := by\n rw [show ((4 : ℝ) / 9) = (9 / 4)⁻¹ by norm_num, Real.log_inv]\n rw [h2]\n linarith [h1]"},"extra_content":null},{"type":"tool_use","id":"Edit_444","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDogLeg.lean","old_string":"/-- The certified (4/9)^{√n} ≤ 0.17631 for √n ≥ 2.236. -/\nlemma four_ninths_rpow_sqrt_le {x : ℝ} (hx : (2.236 : ℝ) ≤ x) :\n (4 / 9 : ℝ) ^ x ≤ (0.17631 : ℝ) := by\n have hlog49 := log_four_ninths_le\n have hlogneg : Real.log (4 / 9) < 0 :=\n Real.log_neg (by norm_num : (0 : ℝ) < 4 / 9) (by norm_num : (4 / 9 : ℝ) < 1)\n have h1 : (4 / 9 : ℝ) ^ x = Real.exp (Real.log (4 / 9) * x) :=\n Real.rpow_def_of_pos (by norm_num : (0 : ℝ) < 4 / 9) x\n rw [h1]\n have h2 : Real.log (4 / 9) * x ≤ (-1.8135 : ℝ) := by\n have h2a : Real.log (4 / 9) * x ≤ Real.log (4 / 9) * 2.236 :=\n mul_le_mul_of_nonpos_left hx hlogneg.le\n have h2b : Real.log (4 / 9) * 2.236 ≤ (-0.811) * 2.236 :=\n mul_le_mul_of_nonneg_right hlog49 (by norm_num)\n calc Real.log (4 / 9) * x ≤ Real.log (4 / 9) * 2.236 := h2a\n _ ≤ (-0.811) * 2.236 := h2b\n _ ≤ -1.8135 := by norm_num\n have h3 : Real.exp (-1.8135) ≤ (0.17631 : ℝ) := by\n have hsum : (5.6721 : ℝ) ≤ Real.exp 1.8135 := by\n calc (5.6721 : ℝ) ≤ ∑ i ∈ Finset.range 7, (1.8135 : ℝ) ^ i / (Nat.factorial i : ℝ) := by\n norm_num [Finset.sum_range_succ]\n _ ≤ Real.exp 1.8135 :=\n Real.sum_le_exp_of_nonneg (by norm_num : (0 : ℝ) ≤ 1.8135) 7\n rw [show Real.exp (-1.8135) = 1 / Real.exp 1.8135 by\n rw [Real.exp_neg, one_div]]\n calc 1 / Real.exp 1.8135 ≤ 1 / 5.6721 :=\n one_div_le_one_div_of_le (by positivity : (0 : ℝ) < 5.6721) hsum\n _ ≤ 0.17631 := by norm_num\n calc Real.exp (Real.log (4 / 9) * x) ≤ Real.exp (-1.8135) :=\n Real.exp_le_exp.mpr h2\n _ ≤ 0.17631 := h3","new_string":"/-- The certified (4/9)^{√n} ≤ 0.164 for √n ≥ 2.236. -/\nlemma four_ninths_rpow_sqrt_le {x : ℝ} (hx : (2.236 : ℝ) ≤ x) :\n (4 / 9 : ℝ) ^ x ≤ (0.164 : ℝ) := by\n have hlog49 := log_four_ninths_le\n have hlogneg : Real.log (4 / 9) < 0 :=\n Real.log_neg (by norm_num : (0 : ℝ) < 4 / 9) (by norm_num : (4 / 9 : ℝ) < 1)\n have h1 : (4 / 9 : ℝ) ^ x = Real.exp (Real.log (4 / 9) * x) :=\n Real.rpow_def_of_pos (by norm_num : (0 : ℝ) < 4 / 9) x\n rw [h1]\n have h2 : Real.log (4 / 9) * x ≤ (-1.81316 : ℝ) := by\n have h2a : Real.log (4 / 9) * x ≤ Real.log (4 / 9) * 2.236 :=\n mul_le_mul_of_nonpos_left hx hlogneg.le\n have h2b : Real.log (4 / 9) * 2.236 ≤ (-0.8109) * 2.236 :=\n mul_le_mul_of_nonneg_right hlog49 (by norm_num)\n calc Real.log (4 / 9) * x ≤ Real.log (4 / 9) * 2.236 := h2a\n _ ≤ (-0.8109) * 2.236 := h2b\n _ ≤ -1.81316 := by norm_num\n have h3 : Real.exp (-1.81316) ≤ (0.164 : ℝ) := by\n have hsum : (6.12639 : ℝ) ≤ Real.exp 1.81316 := by\n calc (6.12639 : ℝ) ≤ ∑ i ∈ Finset.range 7, (1.81316 : ℝ) ^ i / (Nat.factorial i : ℝ) := by\n norm_num [Finset.sum_range_succ]\n _ ≤ Real.exp 1.81316 :=\n Real.sum_le_exp_of_nonneg (by norm_num : (0 : ℝ) ≤ 1.81316) 7\n rw [show Real.exp (-1.81316) = 1 / Real.exp 1.81316 by\n rw [Real.exp_neg, one_div]]\n calc 1 / Real.exp 1.81316 ≤ 1 / 6.12639 :=\n one_div_le_one_div_of_le (by norm_num : (0 : ℝ) < 6.12639) hsum\n _ ≤ 0.164 := by norm_num\n calc Real.exp (Real.log (4 / 9) * x) ≤ Real.exp (-1.81316) :=\n Real.exp_le_exp.mpr h2\n _ ≤ 0.164 := h3"},"extra_content":null},{"type":"tool_use","id":"Edit_445","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDogLeg.lean","old_string":" have h49 := four_ninths_rpow_sqrt_le hsqrt5\n have h3 : dirichletCX n ≤ Real.log 2 * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ))) +\n (3 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) := by\n refine h2.trans ?_\n exact add_le_add_left (mul_le_mul_of_nonneg_left hC2\n (Real.rpow_nonneg (by norm_num) _)) _","new_string":" have h49 := four_ninths_rpow_sqrt_le hsqrt5\n have h3 : dirichletCX n ≤ Real.log 2 * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ))) +\n (3 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) := by\n refine h2.trans ?_\n exact add_le_add_left (mul_le_mul_of_nonneg_left hC2\n (Real.rpow_nonneg (by norm_num) _)) (Real.log 2 * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ))))"},"extra_content":null}]