[{"type":"thinking","thinking":"Confirmed: `zeroSum_nontriv_norm_le` needs `(hTle : T ≤ 3 * 10 ^ 12)` — and the bridge proves it via `by linarith [hTle]` from the over-strong `T ≤ 3·10¹²−1`. So the bridge's PUBLIC hypothesis hTle : T ≤ 3·10¹²−1 is tighter than the internal need (T ≤ 3·10¹²).\n\nFor MY fold: T ≤ √n+1 ≤ (3·10¹²−1)+1 = 3·10¹². So T ≤ 3·10¹² EXACTLY holds — the internal zeroSum_nontriv_norm_le is satisfied. But the bridge's hTle : T ≤ 3·10¹²−1 might fail when T ∈ (3·10¹²−1, 3·10¹²].\n\nHmm — wait — can T be in (3·10¹²−1, 3·10¹²]? T ∈ [√n, √n+1], √n ≤ 3·10¹²−1: T ≤ 3·10¹² ✓ and T ≥ √n could be up to 3·10¹²−1. So T ∈ [√n, √n+1] ⊆ [?, 3·10¹²] — T might land in (3·10¹²−1, 3·10¹²] (only if √n > 3·10¹²−2, i.e., n > (3·10¹²−2)², AND the pigeonhole picks T > 3·10¹²−1). So hTle is NOT guaranteed.\n\nRESOLUTION options:\n(a) Prove a variant bridge with hTle : T ≤ 3·10¹² (clone the ~30-line proof with the linarith adjusted — trivially, since the internal call already only needs T ≤ 3·10¹²). This is clean and honest: the bridge's content only ever used T ≤ 3·10¹².\n\n(b) Strengthen nothing — just inline the bridge's last mile in 6-d.\n\n(a) is best: prove `zeroSum_norm_le_four_FAlt_add_one_of_le` with (hTle : T ≤ 3 * 10 ^ 12) in LiAssembly — actually simpler: in LiSideBounds §6, prove the bridge variant by CALLING the same internal lemmas (zeroSum_nontriv_norm_le + zeroBothWindow_sum_eq_two_mul + trivTerm_norm_le_one + hZCG) — the bridge body is 30 lines, clone with hTle : T ≤ 3·10¹².\n\nHmm wait — actually — even better: can I just get hTle : T ≤ 3·10¹²−1 directly?? T ≤ √n+1 — and I need T ≤ 3·10¹²−1. Hmm — what if n is EXACTLY N₁ = (3·10¹²−1)²? — SfBoundProp includes the endpoint. √n = 3·10¹²−1 (if n = N₁ exactly — but n : ℕ and (3·10¹²−1)² might not be a perfect square — (3·10¹²−1)² = 9·10²⁴ − 6·10¹² + 1 — is that a square? — 3·10¹²−1 = 2999999999999 — its square is (3·10¹²−1)² — n can equal that value (as a real bound (n:ℝ) ≤ (3·10¹²−1)² — the largest such n is ⌊(3·10¹²−1)²⌋ = (3·10¹²−1)² exactly since it's an integer ✓ (3·10¹²−1 is a natural number? — 3·10¹² = 3000000000000 ✓ integer, so 3·10¹²−1 = 2999999999999 ∈ ℕ ✓ and its square ∈ ℕ ✓). So n = (3·10¹²−1)² IS in range, with √n = 3·10¹²−1 EXACTLY (Real.sqrt of a perfect square — (√n)² = n = (3·10¹²−1)² ⟹ √n = 3·10¹²−1 ✓). Then T ∈ [3·10¹²−1, 3·10¹²] — the pigeonhole could pick T > 3·10¹²−1 ⟹ hTle FAILS.\n\nSo I MUST have the T ≤ 3·10¹² variant of the bridge. Clone it in LiSideBounds §6 (or add to LiAssembly — but the freeze protocol... — the freeze is on PAPER files and existing proofs; adding NEW decls to LiAssembly is fine, but §6 of LiSideBounds is the natural home). I'll clone the bridge proof in LiSideBounds §6 with hTle : T ≤ 3 * 10 ^ 12 — calling zeroSum_nontriv_norm_le (T ≤ 3·10¹² ✓), zeroBothWindow_sum_eq_two_mul, trivTerm_norm_le_one, hZCG. Wait — the internal helpers h2not/hdisj2 etc. — all public? zeroSum_nontriv_norm_le is a `lemma` (public ✓), zeroBothWindow_sum_eq_two_mul ✓, trivTerm_norm_le_one ✓ — all accessible.\n\nSo the 6-d theorem `sfBoundProp`:\n\n```lean\ntheorem sfBoundProp (hRH : RHUpTo (3 * 10 ^ 12)) (hZC : ZeroCountProp)\n    (hZC2 : ZeroCountProp2) (hZCG : ZeroCountGlobalProp) (hNLZ : NoLowZeros)\n    (hMZ : MZeroProp) : SfBoundProp := by\n  intro n hn hN1\n  classical\n  have hnR : (100000 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn\n  have hn1 : 1 ≤ n := by omega\n  have ha : (3 : ℝ) ≤ Real.sqrt (n : ℝ) := by\n    have h1 : (10 : ℝ) ≤ Real.sqrt (n : ℝ) := by\n      rw [Real.le_sqrt (by norm_num) (by positivity)]\n      nlinarith [hnR]\n    linarith\n  obtain ⟨T, hTn, hTn1, hTwide⟩ := exists_zero_avoiding_T_wide hZC ha\n  have hT1 : (1 : ℝ) ≤ T := by linarith [ha, hTn]\n  have hT2 : (2 : ℝ) ≤ T := by linarith\n  have h10T : (10 : ℝ) ≤ T := by linarith [show (10:ℝ) ≤ √(n:ℝ) from ...]\n  -- T ≤ 3·10¹² (from n ≤ N₁)\n  have hTle : T ≤ 3 * 10 ^ 12 := by\n    have h1 : Real.sqrt (n : ℝ) ≤ 3 * 10 ^ 12 - 1 := by\n      have h2 : (Real.sqrt (n : ℝ)) ^ 2 ≤ (3 * 10 ^ 12 - 1 : ℝ) ^ 2 := by\n        rw [Real.sq_sqrt (by positivity : (0:ℝ) ≤ (n:ℝ))]\n        -- (n:ℝ) ≤ (3·10¹²−1)² ✓ hN1\n        -- need ^2 form: (√n)² = n ≤ (3·10¹²−1)² — and RHS is already squared\n        -- hmm — (3*10^12−1:ℝ)^2 vs hN1's (3 * 10 ^ 12 - 1 : ℝ) ^ 2 ✓ same\n        exact hN1\n      -- √n ≤ 3·10¹²−1 from squares + nonneg\n      exact (sq_le_sq₀ (Real.sqrt_nonneg _) (by norm_num : (0:ℝ) ≤ 3*10^12-1)).mp h2\n    linarith [hTn1]\n```\n\nHmm — sq_le_sq₀ : 0 ≤ a → 0 ≤ b → (a^2 ≤ b^2 ↔ a ≤ b)?? or (a ≤ b ↔ a² ≤ b²)? — the name suggests sq_le_sq₀ (ha : 0 ≤ a) (hb : 0 ≤ b) : a ^ 2 ≤ b ^ 2 ↔ a ≤ b — the .mp direction: a² ≤ b² ⟹ a ≤ b ✓. Let me double check its exact form later (banked gotcha mentions sq_eq_sq₀ and pow_le_one₀ — and I used pow_le_pow_left₀ before). Alternative: use Real.sqrt_le_sqrt on hN1: √(n) ≤ √((3·10¹²−1)²) = |3·10¹²−1| = 3·10¹²−1:\n```lean\n  have hTle : T ≤ 3 * 10 ^ 12 := by\n    have h1 : Real.sqrt (n : ℝ) ≤ 3 * 10 ^ 12 - 1 := by\n      have h2 := Real.sqrt_le_sqrt hN1\n      rwa [Real.sqrt_sq (by norm_num : (0:ℝ) ≤ 3 * 10 ^ 12 - 1)] at h2\n    linarith [hTn1]\n```\n`Real.sqrt_le_sqrt (h : a ≤ b) : √a ≤ √b` ✓ (used in DL-5: Real.sqrt_le_sqrt (by exact_mod_cast hn) ✓ — takes the inequality directly). `Real.sqrt_sq (ha : 0 ≤ a) : √(a^2) = a` ✓ (Real.sqrt_sq, standard). hN1 : (n:ℝ) ≤ (3*10^12−1)^2 — Real.sqrt_le_sqrt hN1 : √(↑n) ≤ √((3·10¹²−1)²) — rwa [Real.sqrt_sq ...] at h2 : √((3·10¹²−1)²) → 3·10¹²−1 ✓ (norm_num proves 0 ≤ 3·10¹²−1 ✓).\n\nThen T ≤ √n+1 ≤ (3·10¹²−1)+1 = 3·10¹² ✓ linarith [hTn1].\n\n  -- the sides identity + bridge(variant)\n  have hsf := sf_abs_le_rectInt_add_zeroSum hZC hn1 hT1 hTn hTn1 hTwide\n  -- the bridge variant (T ≤ 3·10¹²)\n  have hbridge : ‖∑ ρ ∈ ((zeroBothWindow_finite T).toFinset ∪ {(-2 : ℂ)}),\n      (zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)‖ ≤ 4 * FAlt T + 1 := by\n    -- clone of zeroSum_norm_le_four_FAlt_add_one with hTle : T ≤ 3·10¹²\n    have h2not : (-2 : ℂ) ∉ (zeroBothWindow_finite T).toFinset := by\n      intro h\n      have hnt := (zeroBothWindow_finite T).mem_toFinset.mp h |>.1\n      have h21 : (0 : ℝ) < (-2 : ℂ).re := hnt.2.1\n      norm_num at h21\n    have hdisj2 : Disjoint (zeroBothWindow_finite T).toFinset {(-2 : ℂ)} := by\n      rw [Finset.disjoint_left]\n      intro ρ hρ hρ2\n      rw [Finset.mem_singleton] at hρ2\n      exact h2not (hρ2 ▸ hρ)\n    rw [Finset.sum_union hdisj2, Finset.sum_singleton]\n    have htriv := trivTerm_norm_le_one n\n    have hbr := zeroSum_nontriv_norm_le hRH (n := n) (T := T) hTle\n    have hcount := zeroBothWindow_sum_eq_two_mul hNLZ T\n    have hZ := hZCG T hT2\n    calc ...\n```\n\n(clone the calc verbatim.)\n\n  -- the side bounds\n  have hVl := vIntegral_Jlag_left_norm_le hZC hZC2 hNLZ hMZ hn hTn hTn1\n  have hVr := vIntegral_Jlag_right_le_exp_third_IIMaj hn hTn hTn1\n  have hH := hIntegral_Jlag_full_two_sides hZC hZC2 hNLZ hn hTwide hTn hTn1\n  -- ‖RectInt'‖ = (1/2π)·‖RectInt‖\n  have hnorm : ‖RectangleIntegral' (Jlag n) (rectZ T) (rectW n T)‖ =\n      (1 / (2 * Real.pi)) * ‖RectangleIntegral (Jlag n) (rectZ T) (rectW n T)‖ := by\n    unfold RectangleIntegral'\n    rw [norm_smul]\n    congr 1\n    -- ‖1/(2πi)‖ = 1/(2π)\n    rw [norm_div, norm_one]\n    have h1 : ‖(2 : ℂ) * Real.pi * Complex.I‖ = 2 * Real.pi := by\n      rw [norm_mul, Complex.norm_I, mul_one]\n      -- ‖(2:ℂ) * π‖ = 2π: norm_mul, ‖(2:ℂ)‖ = 2, ‖(π:ℂ)‖ = π\n      rw [norm_mul]\n      have h2 : ‖((2 : ℕ) : ℂ)‖ = 2 := by norm_num?... \n```\n\nHmm — ‖(2 * π * I : ℂ)‖ — the elaborated form: (2 : ℂ) * (π : ℂ) * I — ‖·‖ = 2 * π * 1 = 2π. Note: `2 * π * I` in the RectangleIntegral' def — the 2 is a ℂ numeral, π : ℝ coerced to ℂ, I : ℂ. ‖2 * π * I‖ = ‖2‖·‖π‖·‖I‖ = 2·π·1 = 2π. In Lean: rw [norm_mul, norm_mul] : ‖(2:ℂ)‖·‖(π:ℂ)‖·‖I‖ — ‖(2:ℂ)‖ = 2 (norm_num or RCLike.norm_natCast... — hmm — `‖((2 : ℂ))‖` — via `norm_num`? or the natCast route (2:ℂ) = ((2:ℕ):ℂ): `show ((2:ℕ):ℂ) ...` — ugh. There's `Complex.norm_two`? — hmm. And ‖(π:ℂ)‖ = π : `Complex.norm_real`? — π is Real.pi coerced: ‖(↑π : ℂ)‖ = |π| = π (Complex.norm_real + abs_of_nonneg pi_nonneg). Let me look for existing norms: `Complex.norm_ofReal (r : ℝ) : ‖(↑r : ℂ)‖ = |r|` ✓ exists (norm_ofReal). And ‖(2:ℂ)‖ = 2 : via `show ((2:ℕ):ℂ)`... — simplest: `by norm_num [norm_mul, Complex.norm_I, Complex.norm_ofReal, abs_of_nonneg Real.pi_nonneg]`?? — hmm — norm_num with those simp lemmas might do it. Let me instead do it manually:\n\n```lean\n    have h1 : ‖(2 : ℂ) * (Real.pi : ℂ) * Complex.I‖ = 2 * Real.pi := by\n      rw [norm_mul, norm_mul, Complex.norm_I, mul_one]\n      have h2 : ‖((2 : ℂ) * (Real.pi : ℂ))‖ = 2 * Real.pi := by\n        rw [norm_mul]\n        have h3 : ‖(2 : ℂ)‖ = (2 : ℝ) := by\n          rw [show (2 : ℂ) = ((2 : ℝ) : ℂ) by push_cast; ring, Complex.norm_real]\n          exact abs_of_nonneg (by norm_num)\n        have h4 : ‖(Real.pi : ℂ)‖ = Real.pi := by\n          rw [Complex.norm_real]\n          exact abs_of_nonneg Real.pi_nonneg\n        rw [h3, h4]\n      rw [h2]\n```\nHmm — wait: ‖2 * π * I‖ — parse: ((2 * π) * I) — norm_mul → ‖2*π‖·‖I‖ — Complex.norm_I : ‖I‖ = 1 ✓ → ‖2*π‖ — norm_mul → ‖2‖·‖π‖ → 2·π via h3/h4. But — Complex.norm_real : ‖((r : ℝ) : ℂ)‖ = |r| ✓ (used in 6-c-ii ✓). (Real.pi : ℂ) — π is Real.pi : ℝ coerced — `(Real.pi : ℂ)` — hmm — how is π written in the def? `2 * π * I` — π here — in Zeta23's ResidueCalcOnRectangles, `π` is presumably `Real.pi` coerced to ℂ (they `open Complex` — π : ℂ via coercion or a local notation?). In the def `(1 / (2 * π * I))` — with Complex namespace open — `π` might be `Real.pi` with a coercion inserted automatically (since the context is ℂ). So the term is `(1 : ℂ) / ((2:ℂ) * (↑Real.pi) * I)` — the norm computation as above ✓. Complex.norm_real : ‖(↑r)‖ = |r| — with r := Real.pi ✓.\n\nHmm — `Real.pi_nonneg : 0 ≤ π` ✓.\n\nThen ‖1/(2πI)‖ = 1/‖2πI‖ = 1/(2π) via norm_div + norm_one + h1: \n```lean\n    rw [norm_div, norm_one, h1]\n```\n‖1/(2πI)‖ = ‖1‖/‖2πI‖ = 1/(2π) ✓.\n\nWait — norm_smul : ‖c • x‖ = ‖c‖ * ‖x‖ — RectangleIntegral' = (1/(2πI)) • RectInt — the smul is ℂ-scalar on ℂ-vector ✓ norm_smul ✓ gives ‖1/(2πI)‖·‖RectInt‖ ✓.\n\nHmm — the RectangleIntegral' is an `abbrev` — `unfold RectangleIntegral'` ✓ (or it's reducible — norm_smul might match directly without unfold — use unfold to be safe).\n\n  -- the rectangle side decomposition + norm triangle\n  have hrect := rectangleIntegral_Jlag_eq n T\n  -- RectInt = H(−T) − H(T) + V(right) − V(left)\n  have htri : ‖RectangleIntegral (Jlag n) (rectZ T) (rectW n T)‖ ≤\n      (‖HIntegral (Jlag n) (-5/2) (2 * Real.sqrt n) T‖ +\n        ‖HIntegral (Jlag n) (-5/2) (2 * Real.sqrt n) (-T)‖) +\n      (‖VIntegral (Jlag n) (2 * Real.sqrt n) (-T) T‖ +\n        ‖VIntegral (Jlag n) (-5/2) (-T) T‖) := by\n    rw [hrect]\n    -- ‖(A − B) + (C − D)‖ ≤ ‖A‖ + ‖B‖ + ‖C‖ + ‖D‖\n    calc ‖(HIntegral (Jlag n) (-5/2) (2√n) (-T) − HIntegral (Jlag n) (-5/2) (2√n) T) +\n        (VIntegral (Jlag n) (2√n) (-T) T − VIntegral (Jlag n) (-5/2) (-T) T)‖\n        ≤ ‖HIntegral (Jlag n) (-5/2) (2√n) (-T) − HIntegral (Jlag n) (-5/2) (2√n) T‖ +\n          ‖VIntegral (Jlag n) (2√n) (-T) T − VIntegral (Jlag n) (-5/2) (-T) T‖ :=\n          norm_add_le _ _\n      _ ≤ (‖HIntegral (Jlag n) (-5/2) (2√n) (-T)‖ + ‖HIntegral (Jlag n) (-5/2) (2√n) T‖) +\n          (‖VIntegral (Jlag n) (2√n) (-T) T‖ + ‖VIntegral (Jlag n) (-5/2) (-T) T‖) :=\n          add_le_add (norm_sub_le _ _) (norm_sub_le _ _)\n```\n\nCheck rectangleIntegral_Jlag_eq's exact form (§1, lines 161-168):\n```\nRectangleIntegral (Jlag n) (rectZ T) (rectW n T) =\n  HIntegral (Jlag n) (-5/2) (2*√n) (-T) − HIntegral (Jlag n) (-5/2) (2*√n) T +\n  VIntegral (Jlag n) (2*√n) (-T) T − VIntegral (Jlag n) (-5/2) (-T) T\n```\n✓ — the association: `H(−T) − H(T) + V(right) − V(left)` = `((H(−T) − H(T)) + V(right)) − V(left)`?? — the written form: `H - H + V - V` — infixl: `((H − H) + V) − V` — hmm — my calc assumed `(H−H) + (V−V)`. The def's association: `HIntegral ... - HIntegral ... + VIntegral ... - VIntegral ...` parses as `((H − H) + V) − V`. My norm split needs to match: ‖((H−H)+V)−V‖ ≤ ‖(H−H)+V‖ + ‖V‖ ≤ (‖H−H‖ + ‖V‖) + ‖V‖... Let me redo with the correct association:\n\n‖((A − B) + C) − D‖ ≤ ‖(A−B)+C‖ + ‖D‖ ≤ ‖A−B‖ + ‖C‖ + ‖D‖ ≤ (‖A‖+‖B‖) + ‖C‖ + ‖D‖.\n\n```lean\n    calc ‖((H A − H B) + V C) − V D‖\n        ≤ ‖(H A − H B) + V C‖ + ‖V D‖ := norm_sub_le _ _\n      _ ≤ (‖H A − H B‖ + ‖V C‖) + ‖V D‖ := by linarith [norm_add_le _ _]\n      _ ≤ (‖H A‖ + ‖H B‖) + ‖V C‖ + ‖V D‖ := by linarith [norm_sub_le _ _]\n```\n\nHmm — the middle: ‖(A−B)+C‖ ≤ ‖A−B‖ + ‖C‖ := norm_add_le — then the linariths. Fine — but the exact association must match hrect's RHS. Let me write htri to match hrect exactly:\n\nhrect : RectInt = H(−T) − H(+T) + Vr − Vl — I'll structure:\n```lean\n  have htri : ‖RectangleIntegral (Jlag n) (rectZ T) (rectW n T)‖ ≤\n      ‖HIntegral (Jlag n) (-5/2) (2 * Real.sqrt (n:ℝ)) (-T)‖ +\n      ‖HIntegral (Jlag n) (-5/2) (2 * Real.sqrt (n:ℝ)) T‖ +\n      ‖VIntegral (Jlag n) (2 * Real.sqrt (n:ℝ)) (-T) T‖ +\n      ‖VIntegral (Jlag n) (-5/2) (-T) T‖ := by\n    rw [hrect]\n    have h1 := norm_sub_le (HIntegral (Jlag n) (-5/2) (2*√n) (-T) − HIntegral (Jlag n) (-5/2) (2*√n) T +\n      VIntegral (Jlag n) (2*√n) (-T) T) (VIntegral (Jlag n) (-5/2) (-T) T)\n    have h2 := norm_add_le (HIntegral (Jlag n) (-5/2) (2*√n) (-T) − HIntegral (Jlag n) (-5/2) (2*√n) T)\n      (VIntegral (Jlag n) (2*√n) (-T) T)\n    have h3 := norm_sub_le (HIntegral (Jlag n) (-5/2) (2*√n) (-T)) (HIntegral (Jlag n) (-5/2) (2*√n) T)\n    linarith [h1, h2, h3, norm_nonneg (VIntegral (Jlag n) (2*√n) (-T) T),\n      norm_nonneg (VIntegral (Jlag n) (-5/2) (-T) T),\n      norm_nonneg (HIntegral (Jlag n) (-5/2) (2*√n) (-T)),\n      norm_nonneg (HIntegral (Jlag n) (-5/2) (2*√n) T)]\n```\n\nh1 : ‖(H1−H2+Vr) − Vl‖ ≤ ‖H1−H2+Vr‖ + ‖Vl‖; h2 : ‖H1−H2+Vr‖ ≤ ‖H1−H2‖ + ‖Vr‖; h3 : ‖H1−H2‖ ≤ ‖H1‖ + ‖H2‖. Sum: ‖RectInt‖ ≤ ‖H1‖+‖H2‖+‖Vr‖+‖Vl‖ ✓ linarith with atoms ✓ (no norm_nonneg needed — the inequalities suffice: h1+h2+h3 chain directly: ‖X‖ ≤ ‖H1−H2+Vr‖ + ‖Vl‖ ≤ (‖H1−H2‖+‖Vr‖)+‖Vl‖ ≤ ((‖H1‖+‖H2‖)+‖Vr‖)+‖Vl‖ ✓ pure linarith).\n\n  -- the pinch (horizontal) — separate lemma\n  have hpinch : 2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n:ℝ) + 2)) +\n      (3 - -5/2) * (10.5 * Real.log (T + 2) + 48) ≤ 7 * Hhat T := pinch_horizontal hTn hTn1 (the n/T facts)\n\n  -- assemble\n  -- ‖RectInt'‖ = (1/2π)·‖RectInt‖ ≤ (1/2π)·(‖H−‖+‖H+‖+‖Vr‖+‖Vl‖)\n  -- ≤ (1/2π)·(2(mid+DLR) + e^{1/3}·IIMaj + I_III-charge)\n  -- ≤ (1/2π)·(2·(e⁴+1)·(7·Hhat) + 2·DLR + 2π·IIMaj + I_III-charge)  [pinch + e^{1/3} ≤ 2π]\n  -- = (1/2π)·(2·(e⁴+1)·7·Hhat + 2·DLR) + IIMaj + (1/2π)·I_III-charge\n  -- ≤ (1/2π)·(2·(e⁴+1)·7·Hhat + 2·DLR) + IIMaj + I_III-charge\n  -- and Bn = 4F + I_III-charge + 40·1.3352 + 2(e⁴+1)·7Hhat + 2·DLR + IIMaj + 1 — so:\n  -- |Sf| ≤ (1/2π)(...) + (4F+1) ≤ 4F + I_III-charge + 2(e⁴+1)·7Hhat + 2DLR + IIMaj + 1 = Bn − 40·1.3352?? \n```\n\nHmm wait — careful with the Bn comparison. Bn FAlt n = 4·FAlt T' + 4·T'·((2/3)·Z2hat T' + 10.5·log(T'+2) + 48) + 40·1.3352 + 2·(e⁴+1)·(7·Hhat T') + 2·DogLegRight n + IIMaj n + 1 with T' := √n+1 (the LET in Bn's def).\n\nNOTE: Bn uses T' = √n + 1 (a DEFINITIONAL T), while my side bounds are at the PIGEONHOLE T ∈ [√n, √n+1] — DIFFERENT! The I_III charge is 4·T·((2/3)Z2hat T + 10.5 log(T+2) + 48) + 40·1.3352 at MY T — and Bn's I_III share is 4·T'·(...) + 40·1.3352 at T' = √n+1. Since T ≤ T' = √n+1: 4·T·X(T) ≤ 4·T'·X(T')?? — X(t) = (2/3)Z2hat(t) + 10.5 log(t+2) + 48 — increasing in t (Z2hat_mono + log mono) and T ≤ T' ⟹ 4·T·X(T) ≤ 4·T'·X(T') ✓ (need T·X(T) ≤ T'·X(T'): mul_le_mul (T ≤ T') (X(T) ≤ X(T')) (X(T) ≥ 0) (T' ≥ 0) ✓ — X(T) ≥ 0: Z2hat ≥ 0 (Z2hat_nonneg) + 10.5 log(T+2) ≥ 0 + 48 ✓).\n\nSimilarly Hhat T ≤ Hhat T' (Hhat increasing — Hhat t = 3·C0hat(t)² + 10.5 log(t+2) + 48 — C0hat_mono + log mono + C0hat ≥ 0) ⟹ 7·Hhat T ≤ 7·Hhat T' ✓.\n\nAnd the horizontal pinch at MY T: NI(T) + 5.5·R(T) ≤ 7·Hhat T ≤ 7·Hhat T' ✓.\n\nAnd FAlt T ≤ FAlt T'?? — FAlt increasing (it's the Trudgian majorant — the perimeter ZeroCountGlobalProp is at the SAME T though — hZCG T hT2 : count(T) ≤ FAlt T — the bridge gives 4·FAlt T + 1. Bn has 4·FAlt T' + ... — need FAlt T ≤ FAlt T': FAlt t = (1/2π)·(t·log t) + 0.137·log t + 0.443·loglog t + (7/8+1.588) — increasing for t ≥ 316 ✓ (each term increasing: t·log t — its derivative log t + 1 > 0 ✓ — but for a Lean proof of FAlt T ≤ FAlt T' I'd need monotonicity — the ψ-block machinery in LiSkeleton PROVES FAlt-related monotonicity for the margin convexity — is there a ready `FAlt_mono`? — marginTilde_convex's support — hmm — there might not be a standalone FAlt_mono lemma. For the fold: 4·FAlt T + 1 ≤ 4·FAlt T' + 1 ⟸ FAlt T ≤ FAlt T' ⟸ (T·log T ≤ T'·log T' (mul_le_mul T≤T' logT≤logT' ...) + log T ≤ log T' + loglog T ≤ loglog T') — each term monotone — elementary via Real.log_le_log (T ≥ 316 > 0) + mul_le_mul. Let me just prove FAlt_le_FAlt inline:\n\nFAlt T ≤ FAlt T':\n- (1/2π)·(T·log T) ≤ (1/2π)·(T'·log T'): mul_le_mul (h : T ≤ T') (Real.log_le_log (T > 0) (T ≤ T')) (log T ≥ 0 — T ≥ 316 ⟹ log T ≥ 5 ✓) (T' ≥ 0) then mul by 1/2π ≥ 0.\n- 0.137·log T ≤ 0.137·log T' ✓ log mono.\n- 0.443·log(log T) ≤ 0.443·log(log T') ✓ log mono twice (log T ≥ 1 since T ≥ 316 > e ✓ — wait — Real.log_le_log needs 0 < log T — log T ≥ log 316 ≈ 5.76 > 0 ✓).\n- constants equal.\nSo FAlt T ≤ FAlt T' — elementary linarith-assemblable.\n\nHmm — but hold on — is it cleaner to just prove the comparison |Sf n| ≤ Bn FAlt n via Bn's UNFOLDED form and handle all the T vs T' comparisons in one giant linarith? The final comparison:\n\n|Sf n| ≤ ‖RectInt'‖ + ‖Σ‖\n  ≤ (1/2π)·‖RectInt‖ + (4·FAlt T + 1)\n  ≤ (1/2π)·(‖H−‖+‖H+‖+‖Vr‖+‖Vl‖) + (4·FAlt T + 1)\n  ≤ (1/2π)·([2(mid(T)+DLR)] + [e^{1/3}·IIMaj] + [4T·X(T) + 40·1.3352]) + (4·FAlt T + 1)\n\nwhere mid(T) = (e⁴+1)·(NI(T) + 5.5R(T)), and the horizontal two-sides bound is 2·(mid(T) + DLR) [6-c-v two-sides].\n\n  = (1/2π)·(2(e⁴+1)(NI+5.5R) + 2·DLR + e^{1/3}·IIMaj + 4T·X + 40·1.3352) + 4F + 1\n\nNow: (1/2π)·(e^{1/3}·IIMaj) ≤ IIMaj ⟸ e^{1/3} ≤ 2π ✓ (e^{1/3} ≤ 1.4 ≤ 2π).\n(1/2π)·(2(e⁴+1)(NI+5.5R)) ≤ (1/2π)·(2(e⁴+1)·7·Hhat T) [pinch NI+5.5R ≤ 7·Hhat T; 2(e⁴+1) ≥ 0]\n(1/2π)·(2·DLR) ≤ 2·DLR ⟸ 1/2π ≤ 1 (π ≥ 1/2 — π > 3 ✓) and DLR ≥ 0.\n(1/2π)·(4T·X + 40·1.3352) ≤ 4T·X + 40·1.3352 ⟸ 1/2π ≤ 1 and the bracket ≥ 0.\n\nSo: |Sf n| ≤ (1/2π)·(2(e⁴+1)·7·Hhat T) + 2·DLR + IIMaj + (4T·X(T) + 40·1.3352) + (4·FAlt T + 1)\n  ≤ 2(e⁴+1)·7·Hhat T + 2·DLR + IIMaj + 4T·X(T) + 40·1.3352 + 4·FAlt T + 1 [(1/2π) ≤ 1 again on the Hhat term — Hhat ≥ 0]\n  \n  hmm wait — (1/2π)·(2(e⁴+1)·7·Hhat T) ≤ 2(e⁴+1)·7·Hhat T ⟸ 1/2π ≤ 1 ✓ (bracket ≥ 0).\n\n  ≤ 2(e⁴+1)·7·Hhat T' + 2·DLR + IIMaj + 4T'·X(T') + 40·1.3352 + 4·FAlt T' + 1 [T ≤ T' monotonicity]\n  = Bn FAlt n [Bn's def at T' = √n+1 — UNFOLD]\n\nThe Bn-def match: Bn FAlt n = let T := √n+1; 4·FAlt T + 4·T·X(T) + 40·1.3352 + 2(e⁴+1)·(7·Hhat T) + 2·DLR n + IIMaj n + 1 — with X(T) = ((2/3)·Z2hat T + 10.5·log(T+2)+48) — Bn's exact def (line 2463-2467): `let T := Real.sqrt n + 1; 4 * F T + 4 * T * ((2/3) * Z2hat T + 10.5 * Real.log (T + 2) + 48) + 40 * 1.3352 + 2 * (Real.exp 4 + 1) * (7 * Hhat T) + 2 * DogLegRight n + IIMaj n + 1`.\n\nSo the needed final form: 4·FAlt T' + 4·T'·X(T') + 40·1.3352 + 2(e⁴+1)·7·Hhat T' + 2·DLR + IIMaj + 1 — my assembled bound has EXACTLY these terms (modulo ordering — linarith/ring handles).\n\nSo the proof structure:\n\n1. T from the pigeonhole; T' := √n+1 comparisons (FAlt/X/Hhat monotonicity at T vs T').\n2. hsf (6-b identity) + hbridge (variant T ≤ 3·10¹²).\n3. hnorm (‖RectInt'‖ = (1/2π)‖RectInt‖) + htri + hVl + hVr + hH.\n4. hpinch : NI + 5.5R ≤ 7·Hhat T (the separate pinch_horizontal lemma).\n5. he13 : e^{1/3} ≤ 1.4 ≤ 2π (certified via e ≤ 2.7183 ≤ 2.744 = 1.4³).\n6. h2π : 1/(2π) ≤ 1 (π ≥ 1/2 — from π > 3? — Real.pi_gt_three : 3 < π ✓ — so 2π > 6 > 2 ⟹ 1/(2π) < 1/2 < 1 — actually 1/(2π) ≤ 1 ⟺ 1 ≤ 2π ⟸ 2·3 ≤ 2π ⟸ 3 ≤ π ✓ Real.pi_gt_three).\n7. The giant final linarith assembling everything.\n\nNonneg facts needed for the multiplicative comparisons: IIMaj ≥ 0? — hmm — IIMaj n = 2(√n+1)(e^{√n/2}+1)·0.57·2^{−(2√n−2)} ≥ 0 ✓ positivity. DLR ≥ 0 (sum of nonneg terms — ((√n+1)/2)(e^{5/2}+1)/2 + 8.38 + IIMaj/4 ≥ 0 ✓). Hhat T ≥ 0 (C0hat ≥ 2 > 0 ⟹ 3·C0hat² > 0 + bracket) ✓. X(T) ≥ 0 ✓. FAlt T ≥ 0 ✓ (each term nonneg for T ≥ 316: log T, loglog T ≥ 0, const > 0). 2π > 0 ✓.\n\nThe mul-comparisons:\n- (1/2π)·(e^{1/3}·IIMaj) ≤ 1·IIMaj = IIMaj: (1/2π)·(e^{1/3}·IIMaj) ≤ IIMaj ⟸ (1/2π)·e^{1/3} ≤ 1 ⟸ e^{1/3} ≤ 2π ✓ IIMaj ≥ 0: mul_le_mul_of_nonneg_left-ish or: (1/2π)·(e^{1/3}·IIMaj) = ((1/2π)·e^{1/3})·IIMaj ≤ 1·IIMaj — mul_le_mul_of_nonneg_right ((1/2π)·e^{1/3} ≤ 1) (IIMaj ≥ 0) ✓.\n- (1/2π)·(2(e⁴+1)(NI+5.5R)) ≤ (1/2π)·(2(e⁴+1)·7·Hhat T): mul_le_mul_of_nonneg_left (NI+5.5R ≤ 7·Hhat T) ((1/2π)·2(e⁴+1) ≥ 0)... — break: 2(e⁴+1)·(NI+5.5R) ≤ 2(e⁴+1)·7·Hhat T := mul_le_mul_of_nonneg_left hpinch' (by positivity) where hpinch' : NI + 5.5R ≤ 7·Hhat T — wait — hpinch is stated as 2·Z2hat·log + 5.5R ≤ 7·Hhat — and NI + 5.5R = 2·Z2hat·log(148.5·C0hat) + 5.5·R — hmm — NI := 2·Z2hat(T)·log(148.5·C0hat(√n+2)) ✓ — and the mid bound's inner is NI + 5.5R with 5.5 written as (3 − −5/2) — (3 − −5/2) = 5.5 ✓ norm_num/ring for the coefficient match.\n- Then (1/2π)·(2(e⁴+1)·7·Hhat T) ≤ 2(e⁴+1)·7·Hhat T := mul_le_mul_of_nonneg_left?? — no — (1/2π)·Y ≤ Y ⟸ 1/2π ≤ 1, Y ≥ 0: `mul_le_mul_of_nonneg_right (h1/2π≤1) (Y ≥ 0)` : (1/2π)·Y ≤ 1·Y = Y ✓ — hmm — mul_le_mul_of_nonneg_right (hbc : b ≤ c) (ha : 0 ≤ a) : b * a ≤ c * a — with b := 1/2π, c := 1, a := Y ✓ (1/2π)·Y ≤ 1·Y ✓ then ring for 1·Y = Y.\n\nLet me now also nail the pinch lemma's exact statement:\n\n```lean\ntheorem pinch_horizontal {n : ℕ} (hn : 100000 ≤ n) {T : ℝ}\n    (hTn : Real.sqrt (n : ℝ) ≤ T) (hTn1 : T ≤ Real.sqrt (n : ℝ) + 1) :\n    2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) +\n      (3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48) ≤ 7 * Hhat T\n```\n\nProof components:\n(a) hL : Real.log (148.5 * C0hat (√n+2)) ≤ 2 * Real.log (T + 2):\n    - hC0le : C0hat (√n+2) ≤ √n+2 — via C0hat_le_self (u ≥ 318 — actually make C0hat_le_self for t ≥ 100 to be safe: at t = 100: 0.27922·102 + 2.9 = 31.4 ≤ 100 ✓ — wait my coefficient chain gave C0hat(u) ≤ 0.28(u+2)+2.9 ≤ u ⟺ 3.46 ≤ 0.72u ⟺ u ≥ 4.8 ✓ — let me set C0hat_le_self for 5 ≤ t — then applies at √n+2 ≥ 318 ✓).\n    - h148 : (148.5 : ℝ) ≤ √n + 2: √n ≥ 316 ⟹ √n+2 ≥ 318 ≥ 148.5 ✓.\n    - hC0pos : 0 < C0hat (√n+2) (two_le_C0hat).\n    - h1 : 148.5 * C0hat (√n+2) ≤ (√n+2)^2 := by\n        have := mul_le_mul hC0le h148 (by norm_num : (0:ℝ) ≤ 148.5) (by positivity : (0:ℝ) ≤ √n+2)\n        -- (148.5)·C0hat ≤ (√n+2)·(√n+2) = (√n+2)²\n        nlinarith [this]\n      hmm — mul_le_mul (h₁ : C0hat ≤ √n+2) (h₂ : 148.5 ≤ √n+2) (c0 : 0 ≤ 148.5) (b0 : 0 ≤ √n+2) : C0hat·148.5 ≤ (√n+2)·(√n+2) — ordering: mul_le_mul a≤b c≤d 0≤c 0≤b : a·c ≤ b·d — a := C0hat, b := √n+2, c := 148.5, d := √n+2 : C0hat·148.5 ≤ (√n+2)² — my target: 148.5·C0hat ≤ (√n+2)² — mul_comm ✓ nlinarith or rewrite.\n    - h2 : Real.log (148.5 * C0hat (√n+2)) ≤ Real.log ((√n+2)^2) := Real.log_le_log (by positivity) h1\n    - h3 : Real.log ((√n+2)^2) = 2 * Real.log (√n+2) := by rw [Real.log_pow]; ring\n    - h4 : Real.log (√n+2) ≤ Real.log (T+2) := Real.log_le_log (by positivity) (by linarith [hTn])\n    linarith [h2, h3, h4]\n(b) hZ2le : Z2hat T ≤ 2 * C0hat T: unfold both defs; L := log(T+2) ≥ 1, LL := log L ≥ 0 (T ≥ 316): \n    Z2hat T = 0.6L + 0.886LL + 2.7; 2·C0hat T = 0.866L + 1.772LL + 5.8: diff = 0.266L + 0.886LL + 3.1 ≥ 0 ✓ — unfold Z2hat C0hat; have hL1 : 1 ≤ L (as in Z2hat_mono's hlog1); have hLL0 : 0 ≤ LL (Real.log_nonneg hL1); nlinarith.\n(c) hC0L : 0.433 * Real.log (T + 2) ≤ C0hat T: unfold C0hat; LL ≥ 0, 2.9 ≥ 0: 0.433L ≤ 0.433L + 0.886LL + 2.9 ✓ linarith.\n(d) the main: 2·Z2hat·log(148.5·C0hat) ≤ 2·Z2hat·2·log(T+2) [hL, Z2hat ≥ 0] = 4·Z2hat·log(T+2) ≤ 8·C0hat·log(T+2) [hZ2le, log(T+2) ≥ 0] ≤ 21·C0hat·C0hat [8·log(T+2) ≤ 21·C0hat from hC0L: 8·log(T+2) ≤ (8/0.433)·C0hat ≤ 21·C0hat ⟺ 8/0.433 ≤ 21 ⟺ 8 ≤ 9.093 ✓; then mul_le_mul (8·log(T+2) ≤ 21·C0hat) (le_refl C0hat) (C0hat ≥ 0) (by positivity : 0 ≤ 21·C0hat) : (8·log(T+2))·C0hat ≤ (21·C0hat)·C0hat ✓ rearrange ring].\n(e) 5.5·R ≤ 7·R (R := 10.5·log(T+2)+48 ≥ 0): (3 − −5/2) = 5.5 ✓ norm_num; 5.5·R ≤ 7·R ⟸ R ≥ 0.\n(f) Hhat T = 3·C0hat T² + R: unfold Hhat ✓. 21·C0hat² + 7·R = 7·(3·C0hat² + R) = 7·Hhat ✓ ring.\n\nAssembly: 2·Z2hat·log148.5 + 5.5·R ≤ 21·C0hat² + 7·R = 7·Hhat ✓ linarith.\n\nNow — the C0hat_le_self lemma:\n```lean\ntheorem C0hat_le_self {t : ℝ} (ht : 5 ≤ t) : C0hat t ≤ t := by\n  have ht2 : (0 : ℝ) < t + 2 := by linarith\n  have ht1 : (1 : ℝ) < t + 2 := by linarith\n  have he : (2.7182 : ℝ) ≤ Real.exp 1 := by\n    have h := Real.exp_one_gt_d9.le  -- 2.7182818283 < e\n    norm_num at h ⊢  -- 2.7182818283 ≥ 2.7182 ✓\n    linarith [h]  -- hmm — just linarith [Real.exp_one_gt_d9.le]\n  -- log x ≤ x/e: log(x/e) ≤ x/e − 1\n  have hloge : ∀ x : ℝ, 0 < x → Real.log x ≤ x / Real.exp 1 := by\n    intro x hx\n    have h1 := Real.log_le_sub_one_of_pos (show (0:ℝ) < x / Real.exp 1 from div_pos hx (Real.exp_pos 1))\n    -- h1 : log(x/e) ≤ x/e − 1; log(x/e) = log x − log e = log x − 1\n    have h2 : Real.log (x / Real.exp 1) = Real.log x - 1 := by\n      rw [Real.log_div (ne_of_gt hx) (Real.exp_pos 1).ne', Real.log_exp]\n      ring?? -- log x − log(e^1) = log x − 1... wait Real.log_exp : log(exp x) = x — log(e^1) = 1 ✓\n    rw [h2] at h1\n    -- log x − 1 ≤ x/e − 1 ⟹ log x ≤ x/e\n    linarith [h1]\n  have hL : Real.log (t + 2) ≤ (t + 2) / Real.exp 1 := hloge (t + 2) ht2\n  have hLL : Real.log (Real.log (t + 2)) ≤ Real.log (t + 2) / Real.exp 1 :=\n    hloge (Real.log (t + 2)) (Real.log_pos ht1)\n  -- 1/e ≤ 1/2.7182\n  have hinv : (1 : ℝ) / Real.exp 1 ≤ 1 / 2.7182 :=\n    one_div_le_one_div_of_le (by norm_num : (0:ℝ) < 2.7182) he\n  -- assemble: C0hat t = 0.433L + 0.886LL + 2.9 ≤ (0.433·L + 0.886·L)/e?? \n```\n\nHmm — assembling: C0hat t = 0.433·L + 0.886·LL + 2.9. With L ≤ (t+2)/e and LL ≤ L/e: \n0.433L + 0.886LL ≤ 0.433(t+2)/e + 0.886·L/e = (0.433(t+2) + 0.886L)/e ≤ (0.433(t+2) + 0.886(t+2)/e)/e?? — ugh — nested. Cleaner bound: LL ≤ L (log x ≤ x − 1 ≤ x — actually LL = log L ≤ L/e ≤ L·0.368 hmm) — simplest: LL ≤ L/e (hLL) and L/e ≤ (t+2)/e² — I want a NUMERIC coefficient: C0hat t ≤ 0.433L + 0.886·(L/e) + 2.9. With L ≤ (t+2)/e ≤ (t+2)·0.36789 (1/e ≤ 1/2.7182 = 0.367889 — hmm — 1/2.7182 = ? — compute: 1/2.7182 = 0.3678894 — so L ≤ (t+2)/e ≤ (t+2)·0.36789?? — 1/e ≤ 0.36789 ⟺ e ≥ 1/0.36789 = 2.71821 — e > 2.7182818283 ≥ 2.71821 ✓. Let me use 0.36789 as the certified upper for 1/e: 1/e ≤ 0.36789 ⟺ 1 ≤ 0.36789·e ⟺ 1/0.36789 ≤ e ⟺ 2.71821 ≤ e ✓ from exp_one_gt_d9 (2.7182818283 ≤ e... wait — exp_one_gt_d9 : 2.7182818283 < exp 1 — so e > 2.7182818283 > 2.71821 ✓).\n\nFormally: 1/e ≤ 0.36789 ⟸ 1 ≤ 0.36789·e ⟸ 1/0.36789 ≤ e — hmm — 1/0.36789 = 2.718206... ≤ 2.7182818283 < e ✓. Prove: `have hinv : (1:ℝ)/Real.exp 1 ≤ 0.36789 := by rw [div_le_iff₀ (Real.exp_pos 1), one_mul]; norm_num1; nlinarith [Real.exp_one_gt_d9]` — goal after div_le_iff₀: 1 ≤ 0.36789·e¹ — hmm — div_le_iff₀ (hb : 0 < b) : a/b ≤ c ↔ a ≤ c·b: 1/e ≤ 0.36789 ⟺ 1 ≤ 0.36789·e ✓ — 0.36789·e ≥ 0.36789·2.7182818283 = 1.0000004... ≥ 1 ✓ — compute: 0.36789·2.7182818283 = 1.00000038... ✓ ≥ 1 — nlinarith [Real.exp_one_gt_d9]: 0.36789·e > 0.36789·2.7182818283 = 1.00000038 ≥ 1 ✓ — norm_num verifies 0.36789·2.7182818283 ≥ 1: 0.36789·2.7182818283 = 1.00000075... — let me compute precisely: 0.36789 × 2.7182818 = 0.36789×2.7 = 0.993303, 0.36789×0.0182818 = 0.006727 — total 1.000030 ≈ 1.00003 ≥ 1 ✓✓ — wait let me redo: 0.36789 × 2.7182818283: 0.36789×2 = 0.73578; ×0.7 = 0.257523; ×0.0182818283 = 0.0067272... — hmm — 0.73578 + 0.257523 = 0.993303 (that's ×2.7); + 0.36789×0.0182818283 = 0.006727... — total 1.000030 ✓ ≥ 1 ✓. So 0.36789·2.7182818283 ≈ 1.00003 — norm_num can verify 1 ≤ 0.36789 * 2.7182818283 ✓ (decimal arithmetic).\n\nThen: L ≤ (t+2)/e = (t+2)·(1/e) ≤ (t+2)·0.36789 (t+2 ≥ 0); LL ≤ L/e = L·(1/e) ≤ L·0.36789 ≤ (t+2)·0.36789² ≤ (t+2)·0.135343 (0.36789² = 0.135343...).\n\nHmm — two-step: LL ≤ L·0.36789 and L ≤ (t+2)·0.36789: LL ≤ (t+2)·0.36789·0.36789 = (t+2)·0.36789². mul_le_mul (LL ≤ L·c) (L ≤ (t+2)·c) ... — or nlinarith with the products as hints. This is getting long but it's all mechanical. Let me bound LL more simply: LL = log L ≤ L − 1 ≤ L ≤ (t+2)·0.36789 — via Real.log_le_sub_one_of_pos (L > 0): LL ≤ L − 1 ≤ L ≤ (t+2)·0.36789 ✓ — NO e² needed!! LL ≤ L directly (log x ≤ x−1). So:\n\nC0hat t = 0.433L + 0.886LL + 2.9 ≤ 0.433L + 0.886L + 2.9 = 1.319·L + 2.9 ≤ 1.319·(t+2)·0.36789 + 2.9 = 0.485257·(t+2) + 2.9.\n≤ t ⟺ 0.485257·(t+2) + 2.9 ≤ t ⟺ 0.485257t + 0.970514 + 2.9 ≤ t ⟺ 3.870514 ≤ 0.514743·t ⟺ t ≥ 7.519. So for t ≥ 8 (use ht : 8 ≤ t — or keep 14): 0.514743·t ≥ 0.514743·8 = 4.12 ≥ 3.87 ✓ — at t ≥ 8: 0.485257(t+2)+2.9 ≤ t ⟺ 3.870514 ≤ 0.514743t — at t = 8: 0.514743·8 = 4.118 ≥ 3.87 ✓✓ linarith closes.\n\nHmm wait — 1.319·0.36789 = 0.485257... — verify: 1.319 × 0.36789 = 0.48524... ✓. And the final: 0.485257·(t+2) + 2.9 ≤ t: 0.485257t + 0.970514 + 2.9 ≤ t ⟺ 0.970514 + 2.9 ≤ (1 − 0.485257)t = 0.514743t ⟺ 3.870514 ≤ 0.514743t ⟺ t ≥ 7.5194 ✓ — take ht : 8 ≤ t.\n\nWait — but I need LL ≤ L: Real.log_le_sub_one_of_pos (hL0 : 0 < L) : log L ≤ L − 1 — L = log(t+2) > 0 ⟸ t+2 > 1 ⟸ t > −1 ✓ (t ≥ 8). ✓\n\nSo C0hat_le_self (ht : 8 ≤ t): C0hat t ≤ t — clean:\n```lean\ntheorem C0hat_le_self {t : ℝ} (ht : 8 ≤ t) : C0hat t ≤ t := by\n  have ht2 : (0 : ℝ) < t + 2 := by linarith\n  have ht1 : (1 : ℝ) < t + 2 := by linarith\n  have hinv : (1 : ℝ) / Real.exp 1 ≤ 0.36789 := by\n    rw [div_le_iff₀ (Real.exp_pos 1), one_mul]\n    nlinarith [Real.exp_one_gt_d9]\n  have hL1 : Real.log (t + 2) ≤ (t + 2) / Real.exp 1 := by\n    have h1 := Real.log_le_sub_one_of_pos (div_pos ht2 (Real.exp_pos 1))\n    have h2 : Real.log ((t + 2) / Real.exp 1) = Real.log (t + 2) - 1 := by\n      rw [Real.log_div (ne_of_gt ht2) (Real.exp_pos 1).ne', Real.log_exp]\n    rw [h2] at h1\n    linarith [h1]\n  have hL2 : (t + 2) / Real.exp 1 ≤ (t + 2) * 0.36789 := by\n    rw [div_eq_mul_one_div]\n    exact mul_le_mul_of_nonneg_left hinv ht2.le\n  have hL : Real.log (t + 2) ≤ (t + 2) * 0.36789 := hL1.trans hL2\n  have hLL : Real.log (Real.log (t + 2)) ≤ (t + 2) * 0.36789 := by\n    have h1 := Real.log_le_sub_one_of_pos (Real.log_pos ht1)\n    -- log(log(t+2)) ≤ log(t+2) − 1 ≤ log(t+2) ≤ (t+2)·0.36789\n    nlinarith [h1, hL, ht2]\n  unfold C0hat\n  nlinarith [hL, hLL, ht, Real.log_pos ht1]\n```\n\nThe final nlinarith: goal: 0.433·L + 0.886·LL + 2.9 ≤ t (after unfold C0hat — wait — C0hat's def: `C0hat t = 0.433 * Real.log (t + 2) + 0.886 * Real.log (Real.log (t + 2)) + 2.9` — let me verify the def — from LiContour/audit-037: \"C0hat t = 0.433·log(t+2) + 0.886·log log(t+2) + 2.9\" ✓). With hL : L ≤ (t+2)·0.36789, hLL : LL ≤ (t+2)·0.36789, ht : 8 ≤ t: 0.433L + 0.886LL + 2.9 ≤ (0.433+0.886)·0.36789·(t+2) + 2.9 = 1.319·0.36789·(t+2) + 2.9 = 0.48525·(t+2) + 2.9 — nlinarith computes 1.319·0.36789 = 0.485247... hmm — 1.319 × 0.36789: 1.319×0.36789 = 0.485247 — and I claimed 0.485257 — whatever — nlinarith does the exact decimal arithmetic: 0.485247·(t+2) + 2.9 ≤ t ⟺ 0.485247t + 0.970494 + 2.9 ≤ t ⟺ 3.870494 ≤ 0.514753t ⟺ t ≥ 7.5194 — at t ≥ 8 ✓ — nlinarith [hL, hLL, ht] with products (hL, hLL as linear bounds on atoms L, LL): 0.433L ≤ 0.433·0.36789·(t+2), 0.886LL ≤ 0.886·0.36789·(t+2) — these are LINEAR in L, LL, t ✓ linarith suffices (the coefficient multiplication 0.433·0.36789 is scalar arithmetic ✓ linarith evaluates). ✓\n\nHmm — wait — Real.log_le_sub_one_of_pos : 0 < x → log x ≤ x − 1 — signature: `Real.log_le_sub_one_of_pos (hx : 0 < x) : Real.log x ≤ x - 1` ✓ (the recipe names it ✓). And `Real.log_exp (x) : Real.log (Real.exp x) = x` ✓. And `Real.log_pos (hx : 1 < x) : 0 < Real.log x` ✓.\n\ndiv_le_iff₀ (hb : 0 < b) : a / b ≤ c ↔ a ≤ c * b ✓ (used in 6-c-ii ✓). div_eq_mul_one_div ✓.\n\nNow — the LAST piece: he13 : Real.exp (1/3) ≤ 2·π:\n```lean\n  have he13 : Real.exp (1 / 3 : ℝ) ≤ 2 * Real.pi := by\n    have h1 : Real.exp (1 / 3 : ℝ) ≤ 1.4 := by\n      have h2 : (Real.exp (1 / 3 : ℝ)) ^ 3 ≤ (1.4 : ℝ) ^ 3 := by\n        have h3 : (Real.exp (1 / 3 : ℝ)) ^ 3 = Real.exp 1 := by\n          rw [← Real.exp_nat_mul (1/3 : ℝ) 3]\n          norm_num\n        rw [h3]\n        -- e ≤ 1.4³ = 2.744\n        have h4 : Real.exp 1 ≤ 2.7183 := Real.exp_one_lt_d9.le\n        norm_num at h4 ⊢  -- 1.4^3 = 2.744\n        linarith [h4]\n      exact le_of_pow_le_pow_left₀ (by norm_num : (3 : ℕ) ≠ 0) (Real.exp_nonneg _) h2\n    have h5 : (3 : ℝ) ≤ Real.pi := Real.pi_gt_three.le\n    nlinarith [h1, h5]\n```\n\nle_of_pow_le_pow_left₀ (hn : n ≠ 0) (ha : 0 ≤ a) (h : a^n ≤ b^n) : a ≤ b — signature check: `le_of_pow_le_pow_left₀ (hn : n ≠ 0) (ha : 0 ≤ a) (h : a ^ n ≤ b ^ n) : a ≤ b` — hmm — I think it's `le_of_pow_le_pow_left₀ (hn : n ≠ 0) (ha : 0 ≤ a) : a ^ n ≤ b ^ n → a ≤ b`? — hmm — actually the name pattern: le_of_pow_le_pow_left₀ (hn : n ≠ 0) (ha : 0 ≤ a) (h : a ^ n ≤ b ^ n) : a ≤ b ✓ plausible. Let me verify via grep later.\n\n(Real.exp (1/3))^3 = exp(3·(1/3)) = exp 1: `← Real.exp_nat_mul (1/3) 3` — Real.exp_nat_mul (x) (n) : exp(↑n·x) = (exp x)^n — ← direction: (exp(1/3))^3 → exp(3·(1/3)) — then 3·(1/3) = 1 — `norm_num` — hmm — the goal after rw [← Real.exp_nat_mul]: `Real.exp (↑3 * (1/3)) = Real.exp 1` — ↑3·(1/3) = 1 — `norm_num` proves exp(1) = exp(1)?? — need to simplify ↑3·(1/3) → 1: `norm_num` might close by reducing to exp 1 = exp 1 ✓ or `congr 1; norm_num`. Write `rw [← Real.exp_nat_mul (1/3 : ℝ) 3]; norm_num` — if norm_num leaves `exp 1 = exp 1` it closes ✓; if it reduces the exponent — the goal becomes Real.exp 1 = Real.exp 1 after norm_num simplifies ↑3*(1/3) — ✓ closed by rfl (norm_num closes rfl-goals ✓). Hmm — safer: `rw [← Real.exp_nat_mul (1/3 : ℝ) 3]; congr 1; norm_num` — hmm — wait — the rewrite direction: I want (exp(1/3))^3 = exp 1. h3's proof: `rw [← Real.exp_nat_mul (1/3 : ℝ) 3]` — the goal is `(exp (1/3))^3 = exp 1` — ← exp_nat_mul : pattern (exp ?x)^?n → exp(↑?n·?x) — matches with x := 1/3, n := 3 — goal becomes `exp (↑3·(1/3)) = exp 1` — `congr 1` → `↑3·(1/3) = 1` — norm_num ✓. Let me use that.\n\nHmm — wait — Real.exp_nat_mul (x : ℝ) (n : ℕ) : Real.exp (↑n * x) = (Real.exp x) ^ n — the exponent is `↑n * x` with the NAT CAST — `(3 : ℝ) * (1/3)` where 3 = ↑3 — norm_num handles ↑3·(1/3) = 1 ✓.\n\nFor the hnorm piece — the RectangleIntegral' norm — one more consideration: `unfold RectangleIntegral'` — it's an abbrev — unfold should work; alternatively `rw [RectangleIntegral']`?? — for abbrevs, `show` or `unfold` ✓. Actually — RectangleIntegral' f z w is DEFINED as `(1/(2πI)) • RectangleIntegral f z w` — the norm: ‖(1/(2πI)) • RectInt‖ = ‖1/(2πI)‖·‖RectInt‖ (norm_smul) — but wait — norm_smul for ℂ·ℂ: `norm_smul (a : α) (x : β) : ‖a • x‖ = ‖a‖ * ‖x‖` — needs [NormedSpace α β]-ish — for ℂ on ℂ ✓. ✓\n\nNow — the perimeter hypotheses for sfBoundProp: (hRH : RHUpTo (3·10¹²)) (hZC : ZeroCountProp) (hZC2 : ZeroCountProp2) (hZCG : ZeroCountGlobalProp) (hNLZ : NoLowZeros) (hMZ : MZeroProp) — 6 hypotheses — matching the declared perimeter + RHUpTo. \n\nOne more design point: the final Bn-unfold. After assembling |Sf n| ≤ [the T-form], unfold Bn FAlt n and close by linarith with the T ≤ T' monotonicity haves. The Bn def has `let T := Real.sqrt n + 1` — unfold Bn; simp only [Bn]? — `unfold Bn` produces the let — then `simp only []` or `show` to eliminate the let. Actually — the `let` in Bn's def: `let T := Real.sqrt n + 1; 4 * F T + ...` — after `unfold Bn`, the goal has the let-expression — `simp only [Bn]`? — hmm — Bn is a def with a let — `unfold Bn` might produce `let T := ...; ...` in the goal — Lean's `let` in the goal: `show` the beta-reduced form? — the let-expression `(let T := √n+1; body)` is defeq to body[√n+1/T] — a `show` with the substituted form should work:\n```lean\n  have hBn : Bn FAlt (n : ℝ) = 4 * FAlt (√n+1) + 4 * (√n+1) * ((2/3) * Z2hat (√n+1) + 10.5 * Real.log (√n+1 + 2) + 48) + 40 * 1.3352 + 2 * (Real.exp 4 + 1) * (7 * Hhat (√n+1)) + 2 * DogLegRight (n:ℝ) + IIMaj (n:ℝ) + 1 := by\n    unfold Bn\n    rfl?? or ring\n```\nHmm — unfold Bn gives `let T := √↑n+1; ...` — is `let T := a; f T` rfl-equal to `f a`? YES (zeta reduction — defeq) — so `rfl` after unfold... — or even WITHOUT unfold: Bn FAlt ↑n is DEFEQ to the substituted body ✓ `rfl` directly might work. Use `by rfl`?? — if not, `by unfold Bn`. Let me write `by unfold Bn` and if the goal shows the let, hmm — actually in practice `unfold Bn` normalizes the let away (delta + beta/zeta reduce in the goal display) — then `rfl` might be needed — or the hBn's statement matches the unfolded form exactly and `unfold Bn` closes by rfl automatically? unfold closes goals that become rfl ✓ if the RHS matches. Write:\n```lean\n  have hBn : Bn FAlt (n : ℝ) = ... := by unfold Bn\n```\n— unfold Bn at goal `Bn FAlt ↑n = RHS` → goal becomes `(let T := √↑n+1; ...) = RHS` — hmm — unfold leaves the let — then need to zeta-reduce: `rfl`? or `show RHS = RHS`?? — the let-form is defeq to RHS — `unfold` tactic might fully whnf including zeta — uncertain. Robust: `by have : Bn FAlt (n:ℝ) = ... := rfl; exact this`?? — or just `by rfl`. Try `by rfl` first (Bn's body with let zeta-reduces to RHS by defeq ✓ rfl should work directly). If rfl fails: `by unfold Bn; rfl`? — hmm — `unfold Bn` then the goal still has let — `rfl` uses defeq incl zeta ✓. Actually simplest: `by simp only [Bn]` — simp only with the def-lemma unfolds and beta/zeta reduces ✓ then closes by rfl if RHS matches. Hmm — simp only [Bn] needs Bn to be unfoldable by simp (it's a def — simp only [Bn] uses the equation lemma Bn.eq_def or the definitional unfolding ✓ common pattern). I'll write `by unfold Bn` and add nothing; test.\n\nHmm — actually — WAIT. Maybe cleaner: don't relate to Bn via an hBn equation at all — just `unfold Bn at *`?? no — unfold at goal. Final step: the goal is `|Sf ↑n| ≤ Bn FAlt ↑n` — `unfold Bn` at goal → `|Sf ↑n| ≤ (let ...)...` → hmm. Let me just plan: `rw [hBn]; exact the-assembled-linarith`? no — the assembled bound IS ≤ RHS-of-hBn. So:\n\n```lean\n  rw [hBn]  -- goal: |Sf ↑n| ≤ (the T' = √n+1 form)\n  -- then the giant linarith with all the pieces\n```\n\nHmm — rw [hBn] rewrites Bn FAlt ↑n → the T'-form ✓ then linarith [everything].\n\nThe final linarith's logical content:\n- hsf : |Sf n| ≤ ‖RectInt'‖ + ‖Σ‖\n- hnorm : ‖RectInt'‖ = (1/2π)·‖RectInt‖\n- htri : ‖RectInt‖ ≤ ‖H−‖+‖H+‖+‖Vr‖+‖Vl‖\n- hH : ‖H+‖+‖H−‖ ≤ 2·((e⁴+1)·(NI + 5.5R) + DLR) — wait — hIntegral_Jlag_full_two_sides gives ‖H(+)‖ + ‖H(−)‖ ≤ 2·(midBound + DLR) where midBound = (e⁴+1)·(2·Z2hat·log148.5 + (3−−5/2)·R) ✓ = (e⁴+1)·(NI + 5.5R) ✓.\n- hVr : ‖Vr‖ ≤ e^{1/3}·IIMaj\n- hVl : ‖Vl‖ ≤ 4T·X(T) + 40·1.3352 (I_III charge — where X(T) = (2/3)Z2hat T + 10.5 log(T+2) + 48 ✓ matches Bn's 4T·X(T) term ✓).\n- hbridge : ‖Σ‖ ≤ 4·FAlt T + 1\n- hpinch : NI + 5.5R ≤ 7·Hhat T (with the (3−−5/2) = 5.5 coefficient matching — hpinch stated with (3 − −5/2)·R — and hH's midBound has (3−−5/2)·R too ✓ same atom).\n- he13 : e^{1/3} ≤ 2π\n- h2π1 : 1/(2π) ≤ 1\n- T ≤ T' comparisons: hFAlt : FAlt T ≤ FAlt T'; hX : T·X(T) ≤ T'·X(T'); hHhat : Hhat T ≤ Hhat T'.\n- nonneg: IIMaj ≥ 0, DLR ≥ 0, Hhat T' ≥ 0?? — the linarith needs the multiplicative relations:\n  (1/2π)·‖RectInt‖ ≤ (1/2π)·(‖H−‖+‖H+‖+‖Vr‖+‖Vl‖) — linear (1/2π ≥ 0 ✓ mul by scalar).\n  Then (1/2π)·(2(mid+DLR) + e^{1/3}·IIMaj + (4TX + 40M0)):\n  Expand: (1/2π)·2·mid + (1/2π)·2·DLR + (1/2π)·e^{1/3}·IIMaj + (1/2π)·(4TX + 40M0).\n  Need: (1/2π)·e^{1/3}·IIMaj ≤ IIMaj ⟸ e^{1/3} ≤ 2π, IIMaj ≥ 0 — NONLINEAR (product (1/2π)·e13 — but both are CONSTANTS — linarith treats (1/2π)·e13·IIMaj as IIMaj·c with c a numeric-ish atom?? — the product (1/(2π))·(e^{1/3}) is a CONSTANT (no variables) — linarith can evaluate it?? — he13 : e^{1/3} ≤ 2π — so (1/2π)·e^{1/3} ≤ (1/2π)·2π = 1 — linarith with the atom IIMaj and the constant (1/(2π))·(e^{1/3}): from he13 (e13 ≤ 2π) and 2π > 0: (1/2π)·e13 ≤ 1 — is that LINEAR derivable? (1/2π)·e13 = e13/(2π) — with the DIVISION — linarith doesn't do division!! — need to precompute: have he13' : (1/(2·π))·(e^{1/3}) ≤ 1 — by: rw [div_le_iff₀ (2π > 0)]; ... e13 ≤ 1·(2π) = 2π ✓ he13. Provide as a have:\n  ```lean\n    have h2πpos : (0 : ℝ) < 2 * Real.pi := by positivity?? — pi_pos ✓ positivity with Real.pi_pos in context? — 2·π > 0 — by positivity — π > 0 is an atom-fact positivity knows (Real.pi_pos is a positivity extension? — `Real.pi_pos` — positivity proves 0 < π ✓ I believe).\n    have he13' : (1 / (2 * Real.pi)) * Real.exp (1/3 : ℝ) ≤ 1 := by\n      rw [div_le_iff₀ h2πpos, one_mul]\n      exact he13\n  ```\n  Then (1/2π)·e13·IIMaj ≤ 1·IIMaj = IIMaj via mul_le_mul_of_nonneg_right he13' hIIMaj0 — provide hIIMaj0 : 0 ≤ IIMaj ↑n := by unfold IIMaj; positivity. Hmm — ((1/2π)·e13)·IIMaj ≤ 1·IIMaj — mul_le_mul_of_nonneg_right (he13' : (1/2π)e13 ≤ 1) (0 ≤ IIMaj) ✓ — the association ((1/2π)·e13)·IIMaj vs (1/2π)·(e13·IIMaj) — ring_nf in linarith ✓ fine if I provide the multiplied-out form. To be safe, provide:\n  ```lean\n    have hIIMajAbs : (1 / (2 * Real.pi)) * (Real.exp (1/3 : ℝ) * IIMaj (n:ℝ)) ≤ IIMaj (n:ℝ) := by\n      have h1 := mul_le_mul_of_nonneg_right he13' hIIMaj0\n      -- h1 : ((1/2π)·e13) · IIMaj ≤ 1 · IIMaj\n      calc (1/(2π))·(e13·IIMaj) = ((1/2π)·e13)·IIMaj := by ring\n        _ ≤ 1·IIMaj := h1\n        _ = IIMaj := by ring\n  ```\n  \n  Similarly for the Hhat term: (1/2π)·(2(e⁴+1)·7·Hhat T) ≤ 2(e⁴+1)·7·Hhat T ⟸ 1/2π ≤ 1:\n  ```lean\n    have h2πle : (1 / (2 * Real.pi)) ≤ 1 := by\n      rw [div_le_iff₀ h2πpos, one_mul]\n      have h := Real.pi_gt_three.le\n      linarith\n    have hHhatAbs : (1/(2π))·(2·(e⁴+1)·(7·Hhat T)) ≤ 2·(e⁴+1)·(7·Hhat T) := by\n      have hY : (0:ℝ) ≤ 2·(Real.exp 4+1)·(7·Hhat T) := by positivity?? — Hhat T ≥ 0 needed\n      have h1 := mul_le_mul_of_nonneg_right h2πle hY\n      calc (1/2π)·Y' = (1/2π)·Y' := rfl... — just: have := mul_le_mul_of_nonneg_right h2πle hY; rwa [one_mul] at this\n  ```\n  Hhat T ≥ 0: Hhat T = 3·C0hat T² + 10.5 log(T+2)+48: 3·C0hat² ≥ 0 ✓, log(T+2) ≥ 1 > 0 ✓ ⟹ positivity-ish with two_le_C0hat... — `have hHhat0 : 0 ≤ Hhat T := by unfold Hhat; nlinarith [hC0two, hL1]` — hC0two : 2 ≤ C0hat T (two_le_C0hat hT1'), hL1 : 1 ≤ log(T+2) ✓ then 3·(≥0) + 10.5·(≥1) + 48 ≥ 0 ✓ nlinarith/linarith.\n\n  And the remaining (1/2π)·(2·DLR) ≤ 2·DLR and (1/2π)·(4TX+40M0) ≤ 4TX+40M0 — same h2πle pattern with nonneg of each.\n\nThis is a lot of small nonneg haves — let me just collect them: hDLR0 : 0 ≤ DogLegRight ↑n (unfold DogLegRight; positivity — needs IIMaj ≥ 0 for the /4 part ✓ unfold IIMaj; positivity — nested unfolds — `unfold DogLegRight IIMaj; positivity` — hmm — positivity can't always see through defs — DogLegRight's body: ((√n+1)/2)·(e^{5/2}+1)/2 + 8.38 + IIMaj n/4 — with IIMaj unfolded: 2(√n+1)(e^{√n/2}+1)·0.57·2^{...} — positivity: √n ≥ 0 ✓ (Real.sqrt_nonneg is a positivity extension ✓), exp > 0 ✓, 2^rpow ≥ 0 ✓ — should work).\n  hX0 : 0 ≤ 4·T·X(T) + 40·1.3352 — X(T) ≥ 0: (2/3)·Z2hat T (Z2hat_nonneg hT1) + 10.5·log(T+2) (≥ 0) + 48 — positivity with Z2hat_nonneg and log_nonneg... — 4·T·X(T): T ≥ 0 ✓ — nlinarith [Z2hat_nonneg, log(T+2) ≥ 1] or positivity with the haves. Use: have hX0 : (0:ℝ) ≤ 4*T*((2/3)*Z2hat T + 10.5*Real.log (T+2)+48) + 40*1.3352 := by have h1 := Z2hat_nonneg hT1; have h2 := Real.log_nonneg (by linarith : (1:ℝ) ≤ T+2); nlinarith [hTn, Real.sqrt_nonneg (n:ℝ)].\n\n  The T ≤ T' comparisons:\n  hFAlt : FAlt T ≤ FAlt (√n+1): unfold FAlt; T·log T ≤ (√n+1)·log(√n+1) [mul_le_mul hTn1 (Real.log_le_log hTpos (by linarith [hTn1])) (Real.log_nonneg (1 ≤ T)) (by positivity...)]; 0.137·log T ≤ 0.137·log(√n+1) [log_le_log]; 0.443·log(log T) ≤ 0.443·log(log(√n+1)) [log_le_log (log T > 0)...]; linarith.\n  hX : 4·T·X(T) ≤ 4·(√n+1)·X(√n+1): X increasing: (2/3)·Z2hat T ≤ (2/3)·Z2hat(√n+1) [Z2hat_mono hT1 hTn1] + 10.5·log(T+2) ≤ 10.5·log(√n+1+2) [log_le_log] ⟹ X(T) ≤ X(√n+1); and 0 ≤ X(T); mul_le_mul hTn1 (that) (X(T) ≥ 0) ((√n+1) ≥ 0) then ×4.\n  hHhat : Hhat T ≤ Hhat (√n+1): Hhat t = 3·C0hat t² + 10.5·log(t+2)+48: C0hat T ≤ C0hat(√n+1) [C0hat_mono hT1' hTn1'] ⟹ C0hat T² ≤ C0hat(√n+1)² [pow_le_pow_left₀ (C0hat ≥ 0) that 2] + log mono ⟹ linarith.\n\n  C0hat_mono — signature: from LiGapCircles (cloned as Z2hat_mono in my §1): `C0hat_mono {a b : ℝ} (ha : 1 ≤ a) (hab : a ≤ b) : C0hat a ≤ C0hat b` ✓ (comment in my Z2hat_mono says \"clone of C0hat_mono, LiGapCircles\" ✓ exists).\n\nOK — this is a LOT of small pieces but all elementary. Total 6-d estimate: ~350-450 lines (the pinch ~120, the bridge clone ~35, hnorm ~25, htri ~25, monotonicity ~100, assembly ~60, small haves ~60).\n\nLet me also double check: `exists_zero_avoiding_T_wide hZC ha` gives ⟨T, hT1 : a ≤ T, hT2 : T ≤ a+1, hT3 : the clearance⟩ — obtain ⟨T, hTn, hTn1, hTwide⟩ with hTn : √n ≤ T, hTn1 : T ≤ √n+1 ✓.\n\nAlso sf_abs_le_rectInt_add_zeroSum hZC hn1 hT1 hTn hTn1 hTwide — hT1 : 1 ≤ T ✓ (from ha : 3 ≤ √n ≤ T).\n\nhTwide's form for the 6-c theorems: `∀ ρ, IsNontrivialZero ρ → a − 1 < ρ.im → ρ.im < a + 2 → 1/(9·C0hat(a+2)) ≤ |ρ.im − T|` with a := √n ✓ matches hIntegral_Jlag_full_two_sides' hTwide parameter ✓.\n\nAnd the 6-c-ii's vIntegral_Jlag_left_norm_le hZC hZC2 hNLZ hMZ hn hTn hTn1 ✓; 6-c-iii's vIntegral_Jlag_right_le_exp_third_IIMaj hn hTn hTn1 ✓.\n\nNow — one subtle issue: the hH (two-sides) is stated as ‖H(+)‖ + ‖H(−)‖ ≤ 2·(mid + DLR) — and htri gives ‖RectInt‖ ≤ ‖H−‖+‖H+‖+‖Vr‖+‖Vl‖ — the sum ‖H−‖+‖H+‖ appears in a different ORDER (‖H(−T)‖ + ‖H(T)‖) vs hH's (‖H(T)‖ + ‖H(−T)‖) — linarith handles (atoms) ✓.\n\nAlright — also `Real.pi_gt_three : 3 < Real.pi` ✓ standard.\n\n`Real.exp_one_lt_d9 : exp 1 < 2.7182818286` ✓ used in Z2hat_mono.\n\n`le_of_pow_le_pow_left₀` — verify signature via grep.\n\nLet me write the whole §6 now. Statement name: `sfBoundProp` — hmm — a theorem named sfBoundProp proving the Prop `SfBoundProp` ✓ (per ii′-7's plan: \"theorem sfBoundProp : SfBoundProp\").\n\nOne more check — `Z2hat_nonneg (ht : 1 ≤ t)` ✓ (my §2 lemma). `two_le_C0hat (ht : 1 ≤ t)` ✓ (LiContour:169).\n\n`C0hat_mono` — verify its exact signature via grep (need (ha : 1 ≤ a) (hab : a ≤ b)).","signature":""},{"type":"text","text":"All pieces mapped. The bridge's public `hTle : T ≤ 3·10¹²−1` is over-strong — internally only `T ≤ 3·10¹²` is used, which my T satisfies exactly. I'll clone the bridge's last mile with the right hypothesis. Verifying `C0hat_mono` and `le_of_pow_le_pow_left₀` signatures."},{"type":"tool_use","id":"Bash_167","name":"Bash","input":{"command":"grep -rn -A2 \"theorem C0hat_mono\" \"D:/Python/Quantum/research/lean/NguyenRH1/NguyenRH1/\" | head -6; grep -rn -A2 \"theorem le_of_pow_le_pow_left₀\" \"D:/Python/Quantum/zeta-23-lean/.lake/packages/mathlib/Mathlib/\" | head -6","description":"Verify C0hat_mono and le_of_pow_le_pow_left₀ signatures"},"extra_content":null}]