← Session 35 — ii′-6-R: Lagarias 6.1 right-tail re-proof (E-032/D-073)
thinking (4495 chars)
norm_num proves both comparisons instantly. So the bracket bound's final constant is fine. The whnf/isDefEq timeouts must be elsewhere. Let me test the lt_three's exact structure in a scratch — the exact `div_lt_div_of_pos_right hb h4n` with a huge hypothesis. Hmm — hard to isolate. Let me instead look at whether marginTilde_convex's final linarith is the actual loop (commenting the hbridge to see if it passes without it) — no wait, can't comment easily.
Actually — let me reconsider the errors' ORDER: 2166:0 whnf timeout (lt_three), then 2191:2 «tactic execution» (marginTilde_convex's intro), then 2399:6 isDefEq (hbridge's linarith), then 2777 marginTilde_convex unknown (cascade). The lt_three's timeout is FIRST — if lt_three genuinely loops, the elaborator state corrupts downstream. Let me isolate lt_three's exact: replace `rw [e]; exact div_lt_div_of_pos_right hb h4n` with a calc that avoids the exact-unification:
```
have hb := iimaj_bracket_bound (Real.sqrt_le_sqrt hn)
have h4n : (0 : ℝ) < 4 * n := by linarith
have hb3 : (4.56 * (2 * (-iimA * Real.exp (-iimA * Real.sqrt n) -
iimB * Real.exp (-iimB * Real.sqrt n)) +
(Real.sqrt n + 1) * (iimA ^ 2 * Real.exp (-iimA * Real.sqrt n) +
iimB ^ 2 * Real.exp (-iimB * Real.sqrt n))) -
(4.56 * ((Real.exp (-iimA * Real.sqrt n) + Real.exp (-iimB * Real.sqrt n)) +
(Real.sqrt n + 1) * (-iimA * Real.exp (-iimA * Real.sqrt n) -
iimB * Real.exp (-iimB * Real.sqrt n)))) / Real.sqrt n) / (4 * n) <
(4 / 3) / (4 * n) :=
div_lt_div_of_pos_right hb h4n
rw [hId, chain_rule_sqrt psiTilde psiTilde_contDiff n hn0, deriv_psiTilde,
deriv2_psiTilde]
calc (4.56 * (2 * (-iimA * Real.exp (-iimA * Real.sqrt n) -
iimB * Real.exp (-iimB * Real.sqrt n)) +
(Real.sqrt n + 1) * (iimA ^ 2 * Real.exp (-iimA * Real.sqrt n) +
iimB ^ 2 * Real.exp (-iimB * Real.sqrt n))) -
(4.56 * ((Real.exp (-iimA * Real.sqrt n) + Real.exp (-iimB * Real.sqrt n)) +
(Real.sqrt n + 1) * (-iimA * Real.exp (-iimA * Real.sqrt n) -
iimB * Real.exp (-iimB * Real.sqrt n)))) / Real.sqrt n) / (4 * n)
< (4 / 3) / (4 * n) := hb3
_ = 1 / (3 * n) := by
have h1 : (0 : ℝ) < 3 * n := by linarith [hn0]
have h2 : (0 : ℝ) < 4 * n := by linarith [hn0]
rw [div_eq_div_iff h1.ne' h2.ne']
ring
```
Hmm — this restates hb3 with the EXPLICIT huge form so the calc-step unification is syntactic (no hidden isDefEq). But writing that huge form inline is error-prone. Alternative: use `show` for the goal's form after the rewrites:
```
rw [hId, chain_rule_sqrt psiTilde psiTilde_contDiff n hn0, deriv_psiTilde,
deriv2_psiTilde]
show (4.56 * (2 * (-iimA * Real.exp (-iimA * Real.sqrt n) -
iimB * Real.exp (-iimB * Real.sqrt n)) +
(Real.sqrt n + 1) * (iimA ^ 2 * Real.exp (-iimA * Real.sqrt n) +
iimB ^ 2 * Real.exp (-iimB * Real.sqrt n))) -
(4.56 * ((Real.exp (-iimA * Real.sqrt n) + Real.exp (-iimB * Real.sqrt n)) +
(Real.sqrt n + 1) * (-iimA * Real.exp (-iimA * Real.sqrt n) -
iimB * Real.exp (-iimB * Real.sqrt n)))) / Real.sqrt n) / (4 * n) <
1 / (3 * n)
rw [show (1 : ℝ) / (3 * n) = (4 / 3) / (4 * n) by
rw [div_eq_div_iff (by linarith [hn0] : (0 : ℝ) < 3 * n).ne'
(by linarith [hn0] : (0 : ℝ) < 4 * n).ne']
ring]
exact div_lt_div_of_pos_right hb h4n
```
The `show` pins the goal's form explicitly so the exact's unification is trivial. If the loop was in the goal-form unification, this fixes it. The huge form is verbose but mechanical — let me get the EXACT closed forms from deriv_psiTilde/deriv2_psiTilde (lines 1401-1411 earlier): deriv_psiTilde x = `4.56 * ((Real.exp (-iimA * x) + Real.exp (-iimB * x)) + (x + 1) * (-iimA * Real.exp (-iimA * x) - iimB * Real.exp (-iimB * x)))` and deriv2_psiTilde x = `4.56 * (2 * (-iimA * Real.exp (-iimA * x) - iimB * Real.exp (-iimB * x)) + (x + 1) * (iimA ^ 2 * Real.exp (-iimA * x) + iimB ^ 2 * Real.exp (-iimB * x)))`. And chain_rule_sqrt gives `deriv (deriv ψ(√n)) n = (ψ″(√n) − ψ′(√n)/√n)/(4n)`. So the goal after the rws: `(deriv2-form(√n) − (deriv-form(√n))/√n)/(4n) < 1/(3n)` — the show writes that out.
Hmm — but actually, maybe simpler: the ORIGINAL IIMaj_deriv2_lt worked with EXACTLY this structure — let me diff the original from git to see if something ELSE changed. `git diff` on LiSkeleton.lean will show my changes — the whnf timeout might be caused by an accidental corruption elsewhere in my edits. Let me check git diff.
norm_num is fine on the constants. Checking the full diff of my LiSkeleton changes to find what actually broke.
tool: Bash ok
input
{
"command": "cd D:/Python/Quantum && git diff --stat research/lean/NguyenRH1/NguyenRH1/LiSkeleton.lean && git diff research/lean/NguyenRH1/NguyenRH1/LiSkeleton.lean | head -120",
"description": "Diff LiSkeleton changes so far"
}
result 2026-08-26 11:32:38Z → 2026-08-26 11:32:38Z
research/lean/NguyenRH1/NguyenRH1/LiSkeleton.lean | 37 +++++++++++++++--------
1 file changed, 24 insertions(+), 13 deletions(-)
diff --git a/research/lean/NguyenRH1/NguyenRH1/LiSkeleton.lean b/research/lean/NguyenRH1/NguyenRH1/LiSkeleton.lean
index 0fd1feb..e439152 100644
--- a/research/lean/NguyenRH1/NguyenRH1/LiSkeleton.lean
+++ b/research/lean/NguyenRH1/NguyenRH1/LiSkeleton.lean
@@ -1495,17 +1495,19 @@ theorem iim_u2_antitone :
exact mul_nonpos_of_nonneg_of_nonpos (Real.exp_pos _).le h
set_option maxHeartbeats 800000 in
-/-- [PROVED session 011] The B̃₄ bracket bound (D-057 §3): for s ≥ √20,
-ψ̃″(s) − ψ̃′(s)/s < 2. Factor-monotone argument: the bound splits as
+/-- [PROVED session 011; strengthened to 4/3 session 040 for the
+D-074 dog-leg's 1.5·IIMaj charge] The B̃₄ bracket bound (D-057 §3):
+for s ≥ √20,
+ψ̃″(s) − ψ̃′(s)/s < 4/3. Factor-monotone argument: the bound splits as
4.56·[(s+1)/s]·[(b²s+b)e^{−as}]·[1+e^{−s/2}], three positive decreasing
-factors; at s = √20 the product is ≤ 1.316 < 2. -/
+factors; at s = √20 the product is ≤ 1.3155 < 4/3. -/
theorem iimaj_bracket_bound {s : ℝ} (hs : Real.sqrt 20 ≤ s) :
4.56 * (2 * (-iimA * Real.exp (-iimA * s) - iimB * Real.exp (-iimB * s)) +
(s + 1) * (iimA ^ 2 * Real.exp (-iimA * s) +
iimB ^ 2 * Real.exp (-iimB * s))) -
(4.56 * ((Real.exp (-iimA * s) + Real.exp (-iimB * s)) +
(s + 1) * (-iimA * Real.exp (-iimA * s) -
- iimB * Real.exp (-iimB * s)))) / s < 2 := by
+ iimB * Real.exp (-iimB * s)))) / s < 4 / 3 := by
unfold iimA iimB
set L := Real.log 2 with hLdef
set a : ℝ := 2 * L - 1 / 2 with hadef
@@ -1675,7 +1677,7 @@ theorem iimaj_bracket_bound {s : ℝ} (hs : Real.sqrt 20 ≤ s) :
≤ 4.56 * (s + 1) * (b ^ 2 + b / s) * (eA + eB) := le_trans hstep1 hstep2
_ = 4.56 * ((s + 1) / s) * ((b ^ 2 * s + b) * eA) * (1 + Real.exp (-s / 2)) := hstep3
_ ≤ 4.56 * 1.2237 * 0.2124 * 1.1099 := hchain
- _ < 2 := by norm_num
+ _ < 4 / 3 := by norm_num
/-! ### Assembly: regularity bundles -/
@@ -2139,10 +2141,13 @@ theorem chain_rule_sqrt_shift (φ : ℝ → ℝ) (hφ : ContDiff ℝ 2 φ)
field_simp [hs0]
ring
-/-- [PROVED session 011] IIMaj″(n) < 1/(2n) for n ≥ 20 (the analytic
-version of D-057 §3's "max 2n·|B̃₄″| = 0.189 < 1"). -/
-theorem IIMaj_deriv2_lt {n : ℝ} (hn : 20 ≤ n) :
- deriv (deriv IIMaj) n < 1 / (2 * n) := by
+set_option maxHeartbeats 800000 in
+/-- [PROVED session 011; strengthened session 040 to 1/(3n) via the
+4/3 bracket — the D-074 dog-leg charges 1.5·IIMaj, and 1.5/(3n) =
+1/(2n) preserves the convexity slack] IIMaj″(n) < 1/(3n) for n ≥ 20
+(the analytic version of D-057 §3's "max 2n·|B̃₄″| = 0.189 < 1"). -/
+theorem IIMaj_deriv2_lt_three {n : ℝ} (hn : 20 ≤ n) :
+ deriv (deriv IIMaj) n < 1 / (3 * n) := by
have hn0 : (0 : ℝ) < n := by linarith
have hId : IIMaj = fun m => psiTilde (Real.sqrt m) :=
funext fun m => IIMaj_eq_psiTilde_sqrt m
@@ -2150,8 +2155,10 @@ theorem IIMaj_deriv2_lt {n : ℝ} (hn : 20 ≤ n) :
deriv2_psiTilde]
have hb := iimaj_bracket_bound (Real.sqrt_le_sqrt hn)
have h4n : (0 : ℝ) < 4 * n := by linarith
- have e : (1 : ℝ) / (2 * n) = 2 / (4 * n) := by
- field_simp [hn0.ne']
+ have e : (1 : ℝ) / (3 * n) = (4 / 3) / (4 * n) := by
+ have h1 : (0 : ℝ) < 3 * n := by linarith [hn0]
+ have h2 : (0 : ℝ) < 4 * n := by linarith [hn0]
+ rw [div_eq_div_iff h1.ne' h2.ne']
ring
rw [e]
exact div_lt_div_of_pos_right hb h4n
@@ -2385,8 +2392,12 @@ theorem marginTilde_convex (F : ℝ → ℝ) (hF : ContDiffOn ℝ 2 F (Set.Ioi 1
(div_neg_of_neg_of_pos (psiOf_log_log_shift_neg (by
have h := Real.sqrt_pos.mpr hn0
linarith)) hn4).le
- have hIIM := IIMaj_deriv2_lt (show 20 ≤ n by linarith)
- linarith [hIIM, hnn1, hnn2, hnn3, hnn4, hnn5, hnn6, hnn7, hnn8, hnn9]
+ have hIIM := IIMaj_deriv2_lt_three (show 20 ≤ n by linarith)
+ have hbridge : (1 : ℝ) / (3 * n) < 1 / (2 * n) := by
+ rw [div_lt_div_iff₀ (by linarith [hn0] : (0 : ℝ) < 3 * n)
+ (by linarith [hn0] : (0 : ℝ) < 2 * n), one_mul, one_mul]
+ linarith [hn0]
+ linarith [hIIM, hbridge, hnn1, hnn2, hnn3, hnn4, hnn5, hnn6, hnn7, hnn8, hnn9]
/-! ## 4. Tier (ii) step 1 (session 012): the finite-height Li theorem,
assembled modulo the single named analytic hypothesis `SfBoundProp`.
raw content_json (database row)
[{"type":"thinking","thinking":"norm_num proves both comparisons instantly. So the bracket bound's final constant is fine. The whnf/isDefEq timeouts must be elsewhere. Let me test the lt_three's exact structure in a scratch — the exact `div_lt_div_of_pos_right hb h4n` with a huge hypothesis. Hmm — hard to isolate. Let me instead look at whether marginTilde_convex's final linarith is the actual loop (commenting the hbridge to see if it passes without it) — no wait, can't comment easily.\n\nActually — let me reconsider the errors' ORDER: 2166:0 whnf timeout (lt_three), then 2191:2 «tactic execution» (marginTilde_convex's intro), then 2399:6 isDefEq (hbridge's linarith), then 2777 marginTilde_convex unknown (cascade). The lt_three's timeout is FIRST — if lt_three genuinely loops, the elaborator state corrupts downstream. Let me isolate lt_three's exact: replace `rw [e]; exact div_lt_div_of_pos_right hb h4n` with a calc that avoids the exact-unification:\n\n```\n have hb := iimaj_bracket_bound (Real.sqrt_le_sqrt hn)\n have h4n : (0 : ℝ) < 4 * n := by linarith\n have hb3 : (4.56 * (2 * (-iimA * Real.exp (-iimA * Real.sqrt n) -\n iimB * Real.exp (-iimB * Real.sqrt n)) +\n (Real.sqrt n + 1) * (iimA ^ 2 * Real.exp (-iimA * Real.sqrt n) +\n iimB ^ 2 * Real.exp (-iimB * Real.sqrt n))) -\n (4.56 * ((Real.exp (-iimA * Real.sqrt n) + Real.exp (-iimB * Real.sqrt n)) +\n (Real.sqrt n + 1) * (-iimA * Real.exp (-iimA * Real.sqrt n) -\n iimB * Real.exp (-iimB * Real.sqrt n)))) / Real.sqrt n) / (4 * n) <\n (4 / 3) / (4 * n) :=\n div_lt_div_of_pos_right hb h4n\n rw [hId, chain_rule_sqrt psiTilde psiTilde_contDiff n hn0, deriv_psiTilde,\n deriv2_psiTilde]\n calc (4.56 * (2 * (-iimA * Real.exp (-iimA * Real.sqrt n) -\n iimB * Real.exp (-iimB * Real.sqrt n)) +\n (Real.sqrt n + 1) * (iimA ^ 2 * Real.exp (-iimA * Real.sqrt n) +\n iimB ^ 2 * Real.exp (-iimB * Real.sqrt n))) -\n (4.56 * ((Real.exp (-iimA * Real.sqrt n) + Real.exp (-iimB * Real.sqrt n)) +\n (Real.sqrt n + 1) * (-iimA * Real.exp (-iimA * Real.sqrt n) -\n iimB * Real.exp (-iimB * Real.sqrt n)))) / Real.sqrt n) / (4 * n)\n < (4 / 3) / (4 * n) := hb3\n _ = 1 / (3 * n) := by\n have h1 : (0 : ℝ) < 3 * n := by linarith [hn0]\n have h2 : (0 : ℝ) < 4 * n := by linarith [hn0]\n rw [div_eq_div_iff h1.ne' h2.ne']\n ring\n```\nHmm — this restates hb3 with the EXPLICIT huge form so the calc-step unification is syntactic (no hidden isDefEq). But writing that huge form inline is error-prone. Alternative: use `show` for the goal's form after the rewrites:\n\n```\n rw [hId, chain_rule_sqrt psiTilde psiTilde_contDiff n hn0, deriv_psiTilde,\n deriv2_psiTilde]\n show (4.56 * (2 * (-iimA * Real.exp (-iimA * Real.sqrt n) -\n iimB * Real.exp (-iimB * Real.sqrt n)) +\n (Real.sqrt n + 1) * (iimA ^ 2 * Real.exp (-iimA * Real.sqrt n) +\n iimB ^ 2 * Real.exp (-iimB * Real.sqrt n))) -\n (4.56 * ((Real.exp (-iimA * Real.sqrt n) + Real.exp (-iimB * Real.sqrt n)) +\n (Real.sqrt n + 1) * (-iimA * Real.exp (-iimA * Real.sqrt n) -\n iimB * Real.exp (-iimB * Real.sqrt n)))) / Real.sqrt n) / (4 * n) <\n 1 / (3 * n)\n rw [show (1 : ℝ) / (3 * n) = (4 / 3) / (4 * n) by\n rw [div_eq_div_iff (by linarith [hn0] : (0 : ℝ) < 3 * n).ne'\n (by linarith [hn0] : (0 : ℝ) < 4 * n).ne']\n ring]\n exact div_lt_div_of_pos_right hb h4n\n```\nThe `show` pins the goal's form explicitly so the exact's unification is trivial. If the loop was in the goal-form unification, this fixes it. The huge form is verbose but mechanical — let me get the EXACT closed forms from deriv_psiTilde/deriv2_psiTilde (lines 1401-1411 earlier): deriv_psiTilde x = `4.56 * ((Real.exp (-iimA * x) + Real.exp (-iimB * x)) + (x + 1) * (-iimA * Real.exp (-iimA * x) - iimB * Real.exp (-iimB * x)))` and deriv2_psiTilde x = `4.56 * (2 * (-iimA * Real.exp (-iimA * x) - iimB * Real.exp (-iimB * x)) + (x + 1) * (iimA ^ 2 * Real.exp (-iimA * x) + iimB ^ 2 * Real.exp (-iimB * x)))`. And chain_rule_sqrt gives `deriv (deriv ψ(√n)) n = (ψ″(√n) − ψ′(√n)/√n)/(4n)`. So the goal after the rws: `(deriv2-form(√n) − (deriv-form(√n))/√n)/(4n) < 1/(3n)` — the show writes that out.\n\nHmm — but actually, maybe simpler: the ORIGINAL IIMaj_deriv2_lt worked with EXACTLY this structure — let me diff the original from git to see if something ELSE changed. `git diff` on LiSkeleton.lean will show my changes — the whnf timeout might be caused by an accidental corruption elsewhere in my edits. Let me check git diff.","signature":""},{"type":"text","text":"norm_num is fine on the constants. Checking the full diff of my LiSkeleton changes to find what actually broke."},{"type":"tool_use","id":"Bash_578","name":"Bash","input":{"command":"cd D:/Python/Quantum && git diff --stat research/lean/NguyenRH1/NguyenRH1/LiSkeleton.lean && git diff research/lean/NguyenRH1/NguyenRH1/LiSkeleton.lean | head -120","description":"Diff LiSkeleton changes so far"},"extra_content":null}]