[{"type":"thinking","thinking":"Timeouts around lines 1204-1222 — inside `hu2anti` / the hCD and derivative section. Line 1204:6 (hCD's `simp only [hu2def]` or the contDiff exact), 1209, 1213, 1218, 1222 — the whole hu2anti region times out. The problem might be the `set u2 ... with hu2def` interacting badly with whnf (u2 is a let-variable; unfold attempts at whnf explode?) or the ContDiff term with nested implicit metavariables causing search blowup, or `Set.Ici (Real.sqrt 20)` with the let-variables a, b (also set vars) — linarith/simplex timeouts.\n\nDiagnosis: `set` variables a, b, eA, eB, u2 — when linarith/whnf tries to normalize, it may unfold the lets and blow up. The `(deterministic) timeout at whnf` at 1204 — hCD's `simp only [hu2def]` — unfolds u2 → but then the `exact` needs to match the contDiff term — with a, b as LET variables inside — the unification might unfold a, b (via hadef/hbdef?) no — set vars are fvars with local defs; whnf unfolding them gives 2*L−1/2 etc — L itself a let for Real.log 2 — chains fine...\n\nActually — likely culprit: `antitoneOn_of_deriv_nonpos (convex_Ici _)` — the `_` for the set: convex_Ici (r : ℝ) — the set is Ici (Real.sqrt 20) ✓ should infer. The continuousOn/differentiableOn goals: hCD.continuous.continuousOn — fine. The last bullet: intro x hx; rw [interior_Ici] at hx — interior_Ici : interior (Ici a) = Ioi a ✓. The derivative ≤ 0: rw [(hu2der x).deriv] — hu2der x : HasDerivAt u2 (...) x → .deriv : deriv u2 x = ... — the rw in goal `deriv u2 x ≤ 0` ✓...\n\nWhich line is 1213:12 (SimplexAlgorithm Gauss)? That's linarith's simplex — a linarith call timing out — 1213 is `have := Set.mem_Ioi.mp hx; linarith`?? or hx4's linarith. Simplex timeout suggests linarith got a huge/normalized context — the set-variables with let-values might get unfolded by linarith's preprocessing?? linarith doesn't unfold lets... but `set` creates the vars as fvars WITH definitions; ring_nf/linarith might zeta-expand them, producing giant polynomial terms (2*L−1/2 etc with L = log 2 — fine, small)... Simplex timeout at getTableauImp — the tableau construction with MANY hypotheses (context has ~25 haves) — linarith uses all hypotheses; with big context + decimal rationals it can choke.\n\nMitigation: restructure to shrink context for the linarith calls inside hu2anti — extract needed facts into a `clear` or use targeted linarith [..] with explicit hypothesis list (linarith [h1, h2] uses ONLY those + local hyps? No — linarith [h1] uses h1 PLUS all hypotheses... actually `linarith [h]` adds h to the full context). Better: `linarith only [...]` — uses ONLY the listed ones! Use linarith only for the risky spots.\n\nActually — alternative: move the hu2anti/hu2fac content OUT of the big proof into a separate lemma with a small context. The let-variable soup inside iimaj_bracket_bound is the issue. Split: \n\nlemma iim_u2_antitone : AntitoneOn (fun t => (iimB^2*t + iimB)*Real.exp (−iimA*t)) (Set.Ici (Real.sqrt 20))\nlemma iim_bracket (the bound with the three factors + assembly)\n\nThe u2 derivative fact: hu2der standalone (hasDerivAt of that function) — standalone lemma.\n\nLet me restructure: pull out as standalone theorems with explicit constants — smaller contexts, no set-variables across the boundary:\n\ntheorem iim_u2_hasDerivAt (x : ℝ) : HasDerivAt (fun t => (iimB^2*t + iimB)*Real.exp (−iimA*t)) (Real.exp (−iimA*x)*(iimB^2 − iimA*(iimB^2*x + iimB))) x\n\ntheorem iim_u2_antitone : AntitoneOn (fun t => (iimB^2*t + iimB) * Real.exp (−iimA*t)) (Set.Ici (Real.sqrt 20))\n\nthen in the big proof use them. The numeric facts inside antitone proof: needs iimA/iimB bounds — unfold locally there.\n\nThis decomposition also helps build times (smaller goals). Let me rewrite the whole iimaj_bracket_bound + add these two standalone lemmas. Actually the main proof already has hstep1/hstep2/hstep3 proved OK (errors were all later). The failing region is hu2fac (the antitone argument). Extract:\n\n```lean\n/-- [PROVED session 011] u₂(t) = (b²t+b)e^{−at} is antitone on [√20, ∞):\nderivative e^{−at}(b² − a(b²t+b)) < 0 (a(b²t+b) ≥ 8.846 > b² there). -/\ntheorem iim_u2_antitone : AntitoneOn (fun t => (iimB ^ 2 * t + iimB) * Real.exp (-iimA * t))\n    (Set.Ici (Real.sqrt 20)) := by\n  have hCD : ContDiff ℝ 2 (fun t => (iimB ^ 2 * t + iimB) * Real.exp (-iimA * t)) := by\n    unfold iimA iimB\n    exact ((contDiff_const.mul contDiff_id).add contDiff_const).mul\n      ((contDiff_const.mul contDiff_id).exp)\n  have hder : ∀ x : ℝ, HasDerivAt (fun t => (iimB ^ 2 * t + iimB) * Real.exp (-iimA * t))\n      (Real.exp (-iimA * x) * (iimB ^ 2 - iimA * (iimB ^ 2 * x + iimB))) x := by\n    intro x\n    have hp : HasDerivAt (fun t => iimB ^ 2 * t + iimB) (iimB ^ 2 * 1) x :=\n      ((hasDerivAt_id' x).const_mul (iimB ^ 2)).add_const iimB\n    have he : HasDerivAt (fun t => Real.exp (-iimA * t))\n        (Real.exp (-iimA * x) * (-iimA * 1)) x :=\n      ((hasDerivAt_id' x).const_mul (-iimA)).exp\n    have h := hp.mul he\n    have e : iimB ^ 2 * 1 * Real.exp (-iimA * x) + (iimB ^ 2 * x + iimB) *\n        (Real.exp (-iimA * x) * (-iimA * 1)) =\n        Real.exp (-iimA * x) * (iimB ^ 2 - iimA * (iimB ^ 2 * x + iimB)) := by ring\n    rw [e] at h\n    simp only [Pi.mul_apply] at h\n    exact h\n  apply antitoneOn_of_deriv_nonpos (convex_Ici _)\n  · exact hCD.continuous.continuousOn\n  · exact (hCD.differentiable (by norm_num)).differentiableOn.mono interior_subset\n  · intro x hx\n    rw [interior_Ici] at hx\n    have hxs : Real.sqrt 20 < x := Set.mem_Ioi.mp hx\n    have hlog2lo := Real.log_two_gt_d9\n    have hlog2hi := Real.log_two_lt_d9\n    have ha : (0.8862943606 : ℝ) ≤ iimA := by unfold iimA; linarith\n    have hblo : (1.3862943606 : ℝ) ≤ iimB := by unfold iimB; linarith\n    have hb : iimB ≤ (1.3862943616 : ℝ) := by unfold iimB; linarith\n    have hbpos : (0 : ℝ) < iimB := by linarith\n    have hapos : (0 : ℝ) < iimA := by linarith\n    have hb2lo : (1.9218 : ℝ) ≤ iimB ^ 2 := by nlinarith [hblo]\n    have hb2up : iimB ^ 2 ≤ (1.92182 : ℝ) := by nlinarith [hb, hbpos]\n    have hx4 : (4.4721 : ℝ) ≤ x := by\n      have h : (4.4721 : ℝ) ≤ Real.sqrt 20 := by\n        rw [Real.le_sqrt (by norm_num) (by norm_num)]; norm_num\n      linarith\n    have hbig : (8.8461 : ℝ) ≤ iimA * (iimB ^ 2 * x + iimB) := by\n      have hb2x : (9.9809 : ℝ) ≤ iimB ^ 2 * x + iimB := by\n        have h1 : (1.9218 : ℝ) * 4.4721 ≤ iimB ^ 2 * x :=\n          mul_le_mul hb2lo hx4 (by norm_num) (sq_nonneg iimB)\n        nlinarith [hblo]\n      calc (8.8461 : ℝ) ≤ 0.8862943606 * 9.9809 := by norm_num\n        _ ≤ iimA * (iimB ^ 2 * x + iimB) := mul_le_mul ha hb2x (by norm_num) hapos.le\n    rw [(hder x).deriv]\n    have h : iimB ^ 2 - iimA * (iimB ^ 2 * x + iimB) ≤ 0 := by linarith\n    exact mul_nonpos_of_nonneg_of_nonpos (Real.exp_pos _).le h\n```\n\nWait — the simp only [Pi.mul_apply] at h — earlier it said \"made no progress\". If it makes no progress → error. The .mul output function: let me NOT simp and just try exact h; if mismatch, convert h using 1 (function eq). Risk-managed: use `convert h using 1` — leftover function goal closed by rfl-ish? convert auto-closes rfl goals... The function: goal's lambda fun t => (iimB²*t+iimB)*exp(−iimA*t) vs h's (f*g) Pi form — NOT syntactically equal → convert leaves function-eq goal → then `simp only [Pi.mul_apply]`?? or ext t; rfl?? — the functions ARE pointwise-equal definitionally: `funext t; rfl`? (f*g) t ≡ f t * g t by Pi.mul_apply — rfl should hold at reducible+instances transparency... `funext t` then goal (f*g) t = ... — might close by rfl. Safest: after rw [e] at h: `simp only [Pi.mul_apply] at h; exact h` — but simp made no progress errored earlier... earlier failure was with convert h using 1 bullets — the bullets' goals might have differed. Just try `exact h` FIRST (the defeq might go through at default transparency since Pi.mul_apply is definitional).\n\nHmm — earlier (psiOf_log_sq_shift batch) the analogous `rwa [e] at h` failed with the Pi.mul form visible — assumption failed — meaning exact could NOT see through. But in iim_u2 (hp.mul he) the outer constructor is .mul whose conclusion in THIS Mathlib... in the psiTilde case (hu.mul (hva.add hvb)) the error print showed `fun y => 4.56 * ((f + g) y)` — Pi form. For safety: simp only [Pi.mul_apply] at h; exact h — if simp reports no progress, then exact h directly (already fine). I'll write `simp only [Pi.mul_apply] at h` and handle error if no-progress (remove it).\n\nThen the main iimaj_bracket_bound uses iim_u2_antitone directly:\n  have hu2le : (iimB^2*s + iimB)*eA ≤ (iimB^2*√20 + iimB)*Real.exp (−iimA*√20) := iim_u2_antitone (mem_Ici.mpr hsqrthi.le) (mem_Ici.mpr hs)\n— with hsqrthi.le : Real.sqrt 20 ≤ 4.4722?? — antitone needs the base point IN Ici √20: (√20 ∈ Ici √20) ✓ le_refl. I had that as Set.mem_Ici.mpr hsqrthi.le — hsqrthi : √20 ≤ 4.4722 — that's NOT √20 ≤ √20!! BUG in my earlier code: `hu2anti (Set.mem_Ici.mpr hsqrthi.le) (Set.mem_Ici.mpr hs)` — first arg should prove √20 ∈ Ici √20 = √20 ≤ √20 — I passed hsqrthi.le : 4.4722 ≤ √20?? hsqrthi : √20 ≤ 4.4722 → .le : 4.4722 ≤ √20 — WRONG VALUE (False-ish, unprovable... actually .le flips: hsqrthi.le : 4.4722 ≤ √20 — that's FALSE in general — wait no: hsqrthi : Real.sqrt 20 ≤ 4.4722 — .le is just le of that: 4.4722 ≤ ... no — LE.le.ge : a ≥ b — hsqrthi.le : 4.4722 ≤ Real.sqrt 20?? LE.le.ge reverses the relation: hsqrthi : √20 ≤ 4.4722, hsqrthi.ge : 4.4722 ≥ √20 i.e. 4.4722 ≥ √20 — FALSE (unprovable but it's a term of that type IF hsqrthi exists — no: .ge : b ≥ a FROM a ≤ b — hsqrthi.ge : 4.4722 ≥ √20 — this is a TRUE statement? √20 ≈ 4.4721 ≤ 4.4722 ✓ 4.4722 ≥ √20 ✓ TRUE ✓ fine — but for set membership I need √20 ≤ √20: use le_refl). So: Set.mem_Ici.mpr (le_refl (Real.sqrt 20)).\n\nAlso — the hu2fac's u2-value at √20: the calc with u2 — drop the `set u2` and use the explicit function with iimA/iimB (main proof has a, b as set vars bound to the same expressions — MISMATCH: main proof's a = 2L−1/2 (unfolded) vs iim_u2_antitone's iimA (folded)!! Since the main proof unfolds iimA iimB at the start, its expressions use 2*L−1/2, while iim_u2_antitone uses iimA — DEFEQ but not syntactic — the application `iim_u2_antitone ... : ... ≤ ...` would be in iimA/iimB form, and the main goal (unfolded) needs (2L−1/2) form — mismatch at `exact`/calc. UGH.\n\nResolution: DON'T unfold iimA/iimB in iimaj_bracket_bound; instead keep them folded and rewrite the standalone facts via `show`/conversions. The numeric facts (ha, hb etc) are proved by `unfold iimA iimB at *`?? — but then goal's iimA unfolds too... \n\nCleanest: DON'T unfold in the main proof. Prove numeric facts with local unfolds:\n  have ha : (0.8862943606 : ℝ) ≤ iimA := by unfold iimA; linarith [Real.log_two_gt_d9]\n(unfold iimA in the GOAL of that have only ✓ goal becomes 0.8862943606 ≤ 2*log2−1/2 ✓ linarith with the bounds — pass them: linarith [Real.log_two_gt_d9, Real.log_two_lt_d9].)\nSimilarly hab : iimA ≤ iimB := by unfold iimA iimB; linarith [Real.log_two_gt_d9].\nheB' : eB-equation: exp(−iimB*s) = exp(−iimA*s)*exp(−s/2): exponent: −iimB*s = −iimA*s − s/2 ⟺ iimB − iimA = 1/2: have hab2 : iimB = iimA + 1/2 := by unfold iimA iimB; ring. Then: rw [← Real.exp_add]; congr 1; rw [hab2]; ring.\n\nSo revise iimaj_bracket_bound: remove the top `unfold iimA iimB` + set L/a/b — instead work with iimA/iimB/iimA directly, setting only eA, eB... but wait — I already rewrote everything with a, b, L... The previous version's errors were ONLY in the hu2fac region (antitone) — hstep1/2/3 PASSED (their errors got fixed). So minimal change: replace the hu2fac subproof (antitone part) with the standalone iim_u2_antitone + bridge the folded/unfolded mismatch.\n\nSince the main proof has a := 2L−1/2 set-var and iim_u2_antitone talks about iimA: bridge: have hAid : iimA = a := by rw [hadef, ← hLdef]?? hadef : a = 2*L−1/2; iimA = 2*log2−1/2: hAid : iimA = a: unfold iimA; rw [← hLdef, ← hadef]. Hmm hLdef : L = Real.log 2: iimA unfolds to 2*Real.log 2 − 1/2; rw [← hLdef] → 2*L − 1/2; rw [← hadef] → a ✓. So:\n  have hAid : iimA = a := by unfold iimA; rw [← hLdef, ← hadef]\n  have hBid : iimB = b := by unfold iimB; rw [← hLdef, ← hadef]?? iimB = 2*log2 → rw [← hLdef] → 2*L; hbdef : b = 2*L → rw [← hbdef] ✓.\nThen iim_u2_antitone's statement in a,b terms: rw [hAid, hBid] at iim_u2_antitone?? — rewriting a CONSTANT's occurrences in a theorem instance: obtain hanti := iim_u2_antitone; rw [hAid, hBid] at hanti ✓ (hAid : iimA = a rewrites iimA → a everywhere in hanti ✓).\n\nAnd u2value: (b²√20+b)*exp(−a√20) — from hanti : AntitoneOn (fun t => (b²*t+b)*exp(−a*t)) (Ici √20): hanti (mem_Ici.mpr (le_refl _)) (mem_Ici.mpr hs) : (fun ...) s ≤ (fun ...) √20 — beta: (b²*s+b)*exp(−a*s) ≤ (b²*√20+b)*exp(−a*√20) — beta-reducible ✓ maybe need `simp only []` or `show` — the application hanti h1 h2 has type with the lambda applied — use `have := hanti (Set.mem_Ici.mpr (le_refl _)) (Set.mem_Ici.mpr hs)` — its type is (fun t => ...) s ≤ (fun t => ...) (√20) — defeq to the applied form ✓ usable in the calc via exact/defeq.\n\nOK — implement: add standalone iim_u2_antitone (before iimaj_bracket_bound), and in the main proof replace the hu2fac subproof's antitone internals with the bridge. The rest of hu2fac (hb2lo/hb2up reused for hu2val's hpoly — those are inside hu2fac: hb2lo, hb2up were defined at hu2fac level... they were inside hu2fac in my code? Looking at my code: hb2lo/hb2up were inside hu2anti's... I had them at hu2fac level (before hu2anti)? In the last edit they're inside hu2anti (the `have hCD` version moved them). The hu2val's hpoly needs hb2up — re-derive locally.\n\nSimplest: rewrite the hu2fac block completely:\n\n```lean\n  have hu2fac : (b ^ 2 * s + b) * eA ≤ (0.2124 : ℝ) := by\n    have hAid : iimA = a := by unfold iimA; rw [← hLdef, ← hadef]\n    have hBid : iimB = b := by unfold iimB; rw [← hLdef, ← hbdef]\n    have hanti := iim_u2_antitone\n    rw [hAid, hBid] at hanti\n    have hu2le : (b ^ 2 * s + b) * Real.exp (-a * s) ≤\n        (b ^ 2 * Real.sqrt 20 + b) * Real.exp (-a * Real.sqrt 20) :=\n      hanti (Set.mem_Ici.mpr (le_refl _)) (Set.mem_Ici.mpr hs)\n    have hu2val : (b ^ 2 * Real.sqrt 20 + b) * Real.exp (-a * Real.sqrt 20) ≤\n        (0.2124 : ℝ) := by\n      have hb2up : b ^ 2 ≤ (1.92182 : ℝ) := by nlinarith [hb, hbpos]\n      have hexp : Real.exp (-a * Real.sqrt 20) ≤ (0.0212721 : ℝ) := by\n        ... (as before)\n      have hpoly : b ^ 2 * Real.sqrt 20 + b ≤ (9.9811 : ℝ) := by\n        have h1 : b ^ 2 * Real.sqrt 20 ≤ 1.92182 * 4.4722 :=\n          mul_le_mul hb2up hsqrthi (by norm_num) (sq_nonneg b)\n        nlinarith [hb]\n      exact le_trans (mul_le_mul hpoly hexp (Real.exp_pos _).le (by norm_num)) (by norm_num)\n    calc (b ^ 2 * s + b) * eA = (b ^ 2 * s + b) * Real.exp (-a * s) := rfl\n      _ ≤ (b ^ 2 * Real.sqrt 20 + b) * Real.exp (-a * Real.sqrt 20) := hu2le\n      _ ≤ 0.2124 := hu2val\n```\nNote: `(b²*s+b)*eA = (b²*s+b)*exp(−a*s)` — rfl? eA is a set-var := Real.exp (−a*s): heAdef : eA = Real.exp (−a*s) — rw [heAdef] or rfl via defeq of let-vars — `rfl` works (set vars are let-bound, defeq ✓)... rfl might fail at syntactic — use `by rw [heAdef]`. calc step with `= ... := by rw [heAdef]`? heAdef rewrites eA → exp ✓.\n\nhanti's application type: (fun t => (b²*t+b)*exp(−a*t)) s ≤ (fun t => ...) (√20) — hu2le's stated type is the beta-reduced form — defeq: `exact` should accept?? The hanti h1 h2 term has the UNREDUCED type; hu2le declares reduced — the `:= hanti ...` requires defeq check between declared and actual ✓ beta-reduction is default defeq ✓ OK.\n\nAlso hbpos needed in hu2val's hb2up — hbpos defined at main level ✓ (already have hbpos : 0 < b).\n\nDelete the old hu2fac entirely (the set u2/hCD/hu2anti block) and the stray hb2lo/hb2up definitions that were inside it — check current text: after hu1, the hu2fac block contains: set u2, hu2der, hb2lo, hb2up, hCD, hu2anti, hu2le, hu2val, calc. Replace ALL of it with the new version (keeping the hexp subproof with the sum bound).\n\nThe standalone iim_u2_antitone goes BEFORE iimaj_bracket_bound.","signature":""},{"type":"text","text":"The antitone argument needs to be its own lemma (smaller context), with a folded/unfolded bridge. Restructuring."},{"type":"tool_use","id":"Edit_212","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean","old_string":"/-- [PROVED session 011] The B̃₄ bracket bound (D-057 §3): for s ≥ √20,","new_string":"/-- [PROVED session 011] u₂(t) = (b²t+b)·e^{−at} is antitone on [√20, ∞):\nits derivative is e^{−at}·(b² − a(b²t+b)) and a(b²t+b) ≥ 8.846 > b² there. -/\ntheorem iim_u2_antitone :\n    AntitoneOn (fun t => (iimB ^ 2 * t + iimB) * Real.exp (-iimA * t))\n      (Set.Ici (Real.sqrt 20)) := by\n  have hCD : ContDiff ℝ 2 (fun t => (iimB ^ 2 * t + iimB) * Real.exp (-iimA * t)) := by\n    unfold iimA iimB\n    exact ((contDiff_const.mul contDiff_id).add contDiff_const).mul\n      ((contDiff_const.mul contDiff_id).exp)\n  have hder : ∀ x : ℝ,\n      HasDerivAt (fun t => (iimB ^ 2 * t + iimB) * Real.exp (-iimA * t))\n        (Real.exp (-iimA * x) * (iimB ^ 2 - iimA * (iimB ^ 2 * x + iimB))) x := by\n    intro x\n    have hp : HasDerivAt (fun t => iimB ^ 2 * t + iimB) (iimB ^ 2 * 1) x :=\n      ((hasDerivAt_id' x).const_mul (iimB ^ 2)).add_const iimB\n    have he : HasDerivAt (fun t => Real.exp (-iimA * t))\n        (Real.exp (-iimA * x) * (-iimA * 1)) x :=\n      ((hasDerivAt_id' x).const_mul (-iimA)).exp\n    have h := hp.mul he\n    have e : iimB ^ 2 * 1 * Real.exp (-iimA * x) + (iimB ^ 2 * x + iimB) *\n        (Real.exp (-iimA * x) * (-iimA * 1)) =\n        Real.exp (-iimA * x) * (iimB ^ 2 - iimA * (iimB ^ 2 * x + iimB)) := by ring\n    rw [e] at h\n    simp only [Pi.mul_apply] at h\n    exact h\n  apply antitoneOn_of_deriv_nonpos (convex_Ici _)\n  · exact hCD.continuous.continuousOn\n  · exact (hCD.differentiable (by norm_num)).differentiableOn.mono interior_subset\n  · intro x hx\n    rw [interior_Ici] at hx\n    have hxs : Real.sqrt 20 < x := Set.mem_Ioi.mp hx\n    have hlog2lo := Real.log_two_gt_d9\n    have hlog2hi := Real.log_two_lt_d9\n    have ha : (0.8862943606 : ℝ) ≤ iimA := by unfold iimA; linarith\n    have hblo : (1.3862943606 : ℝ) ≤ iimB := by unfold iimB; linarith\n    have hb : iimB ≤ (1.3862943616 : ℝ) := by unfold iimB; linarith\n    have hbpos : (0 : ℝ) < iimB := by linarith\n    have hapos : (0 : ℝ) < iimA := by linarith\n    have hb2lo : (1.9218 : ℝ) ≤ iimB ^ 2 := by nlinarith [hblo]\n    have hb2up : iimB ^ 2 ≤ (1.92182 : ℝ) := by nlinarith [hb, hbpos]\n    have hx4 : (4.4721 : ℝ) ≤ x := by\n      have h : (4.4721 : ℝ) ≤ Real.sqrt 20 := by\n        rw [Real.le_sqrt (by norm_num) (by norm_num)]; norm_num\n      linarith\n    have hbig : (8.8461 : ℝ) ≤ iimA * (iimB ^ 2 * x + iimB) := by\n      have hb2x : (9.9809 : ℝ) ≤ iimB ^ 2 * x + iimB := by\n        have h1 : (1.9218 : ℝ) * 4.4721 ≤ iimB ^ 2 * x :=\n          mul_le_mul hb2lo hx4 (by norm_num) (sq_nonneg iimB)\n        nlinarith [hblo]\n      calc (8.8461 : ℝ) ≤ 0.8862943606 * 9.9809 := by norm_num\n        _ ≤ iimA * (iimB ^ 2 * x + iimB) := mul_le_mul ha hb2x (by norm_num) hapos.le\n    rw [(hder x).deriv]\n    have h : iimB ^ 2 - iimA * (iimB ^ 2 * x + iimB) ≤ 0 := by linarith\n    exact mul_nonpos_of_nonneg_of_nonpos (Real.exp_pos _).le h\n\n/-- [PROVED session 011] The B̃₄ bracket bound (D-057 §3): for s ≥ √20,"},"extra_content":null}]