[{"type":"thinking","thinking":"6-c-iv committed (1fed1df). Now 6-c-v — the horizontal assembly. This is much simpler:\n\n**6-c-v RECIPE:** HIntegral_split at 3 (integrability via zeta_ne_zero_horizontal for the mid, re ≥ 3 zero-free for the tail) ⟹ ‖H(−5/2→2√n, ±T)‖ ≤ mid + DogLegRight (dogLegUpper_two_sides, hIntegral_Jlag_low(_neg)_norm_le_dogLegUpper ✓ PROVED); both sides: ≤ 2(e⁴+1)(NI + 5.5(...)) + 2·DogLegRight.\n\nSo:\n- ‖H(−5/2→2√n, T)‖ = ‖H(−5/2→3, T) + H(3→2√n, T)‖ ≤ ‖H(−5/2→3, T)‖ + ‖H(3→2√n, T)‖ ≤ mid-bound + DL-tail-bound.\n\nThe DL-5 tail bounds:\n- `hIntegral_Jlag_low_le_dogLegUpper {n} {T} (hn : 16 ≤ n) (hTn) (hTn1) : ‖HIntegral (Jlag n) 3 (2√n) T‖ ≤ ((√n+1)/2)(e^{5/2}+1)/2 + 8.38 + IIMaj/4`\n- `hIntegral_Jlag_low_neg_norm_le_dogLegUpper` — same for (−T).\n\nAnd DogLegRight (n : ℝ) — from LiSkeleton line 762: `def DogLegRight (n : ℝ) : ℝ := ...` — let me check its exact def (it should be ((√n+1)/2)(e^{5/2}+1)/2 + 8.38 + IIMaj/4 — the per-side charge).\n\nAnd `dogLegUpper_two_sides` (DL-5 capstone): ‖H(3→2√n, T)‖ + ‖H(3→2√n, −T)‖ ≤ 2·DogLegRight... wait — dogLegUpper_two_sides's statement (lines 1404-1408): ‖HIntegral (Jlag n) 3 (2√n) T‖ + ‖HIntegral (Jlag n) 3 (2√n) (−T)‖ ≤ 2·((√n+1)/2·(e^{5/2}+1)/2 + 8.38 + IIMaj/4) — hmm — the RHS is written as 2·(...) — and DogLegRight is presumably exactly that (...). Let me check DogLegRight's def.\n\nThe 6-c-v deliverable (per the 6-d recipe): the horizontal charge is `2(e⁴+1)(NI + 5.5(...)) + 2·DogLegRight` where NI = 2·Z2hat(T)·log(148.5·C0hat(√n+2)). Hmm — actually for the FOLD (6-d), what form is most useful? The fold: |Sf n| ≤ (1/2π)(I_III + Horiz + e^{1/3}IIMaj) + (4F+1) where Horiz = ‖H(−5/2→2√n, T)‖ + ‖H(−5/2→2√n, −T)‖... — wait — actually the RectangleIntegral decomposes as H(−T) − H(T) + V(right) − V(left) — so ‖RectInt‖ ≤ ‖H(−T)‖ + ‖H(T)‖ + ‖V(right)‖ + ‖V(left)‖ — the \"sides\" sum. The horizontal assembly's deliverable: ‖H(−5/2→2√n, T)‖ + ‖H(−5/2→2√n, −T)‖ ≤ 2·mid-bound + 2·DogLegRight — i.e., a two-sides lemma like dogLegUpper_two_sides.\n\nPer 6-c-v recipe: \"both sides: ≤ 2(e⁴+1)(NI + 5.5(...)) + 2·DogLegRight\". So:\n\n```lean\ntheorem hIntegral_Jlag_full_two_sides (hZC) (hZC2) (hNLZ) {n} (hn : 100000 ≤ n) {T}\n    (hTwide) (hTn) (hTn1) :\n    ‖HIntegral (Jlag n) (-5/2) (2 * Real.sqrt n) T‖ +\n      ‖HIntegral (Jlag n) (-5/2) (2 * Real.sqrt n) (-T)‖ ≤\n      2 * ((Real.exp 4 + 1) * (2 * Z2hat T * Real.log (148.5 * C0hat (√n+2)) +\n          (3 - -5/2) * (10.5 * Real.log (T + 2) + 48))) +\n        2 * DogLegRight (n : ℝ)\n```\n\nSteps:\n1. HIntegral_split at 3 for each side: H(−5/2→2√n, ±T) = H(−5/2→3, ±T) + H(3→2√n, ±T) — needs integrability on [−5/2,3] and [3,2√n] of the Jlag path at ±T.\n   - On [−5/2,3]: continuity via zeta_ne_zero_horizontal (my hcontJ from 6-c-iv — but that's inside the mid theorem's proof — I need it again here or factor it... hmm — hcontJ was a local have in hIntegral_Jlag_mid_norm_le. For 6-c-v I need the integrability again. Factor a global continuity lemma? — actually the HIntegral_split (from §1 scaffolding) takes (h1 : IntervalIntegrable ... a b) (h2 : ... b c). For [−5/2,3] — rebuild the hcontJ machine (or factor). For [3,2√n] — re ≥ 3 zero-free — the DL continuity machine: `holomorphicOn_Jlag_dogleg` or `Jlag_differentiableAt_dogleg` (DL-1) — gives holomorphicity on Re ≥ 3! So IntervalIntegrable from the DL lemmas? Let me check what DL-5 used for integrability when it split... — DL-5's hIntegral_Jlag_low_le_dogLegUpper is about H(3→2√n) — its own proof handled the integrability internally. For MY split at 3, I need IntervalIntegrable on both [−5/2,3] and [3,2√n] of (fun σ => Jlag n (↑σ + ↑T·I)).\n   - [−5/2,3]: hcontJ from 6-c-iv (rebuild — it's ~15 lines).\n   - [3,2√n]: Jlag continuous on re ≥ 3 path — from DL-1's Jlag_differentiableAt_dogleg / holomorphicOn_Jlag_dogleg — those are about the Jlag on the dog-leg region. Let me check their exact statements — if they give DifferentiableAt Jlag at each point with re ≥ 3, then continuousAt ⟹ intervalIntegrable via Continuous.intervalIntegrable with the comp pattern (fun_prop path + ContinuousAt.comp pinned) — or via holomorphicOn → continuousOn → intervalIntegrable: `ContinuousOn.intervalIntegrable (hab : a ≤ b) (h : ContinuousOn f (uIcc a b))`. The path's image {σ + iT : σ ∈ [3, 2√n]} ⊆ {re ≥ 3} ✓.\n\n2. Then ‖H(−5/2→2√n, ±T)‖ ≤ ‖H(−5/2→3, ±T)‖ + ‖H(3→2√n, ±T)‖ (norm_add_le) ≤ mid + DL-tail (the 6-c-iv mid bound + DL-5's hIntegral_Jlag_low(_neg)_norm_le_dogLegUpper).\n\n3. Sum the two sides + final arithmetic to the stated form.\n\nLet me check the exact DL lemma names/statements + DogLegRight's def + holomorphicOn_Jlag_dogleg.","signature":""},{"type":"text","text":"6-c-iv committed (`1fed1df`). Now 6-c-v (horizontal assembly) — the lightest of the four. Checking the DL-5 split-integrability machinery and `DogLegRight`'s definition."},{"type":"tool_use","id":"TodoWrite_144","name":"TodoWrite","input":{"todos":[{"content":"6-c-ii: I_III left-vertical bound vIntegral_Jlag_left_norm_le","status":"completed","activeForm":"Proving 6-c-ii I_III left-vertical bound"},{"content":"6-c-iii: I_I right-vertical bound (F-E form)","status":"completed","activeForm":"Proving 6-c-iii I_I bound"},{"content":"6-c-iv: mid-horizontal segment machine","status":"completed","activeForm":"Proving 6-c-iv mid-horizontal machine"},{"content":"6-c-v: horizontal assembly (mid + DL-5 tails)","status":"in_progress","activeForm":"Assembling 6-c-v horizontal bound"},{"content":"6-d: fold ⟹ sfBoundProp (then commit, update archive)","status":"pending","activeForm":"Proving 6-d fold to sfBoundProp"}]},"extra_content":null},{"type":"tool_use","id":"Grep_145","name":"Grep","input":{"pattern":"def DogLegRight|theorem holomorphicOn_Jlag_dogleg|theorem Jlag_differentiableAt_dogleg|theorem ContinuousOn\\.intervalIntegrable|theorem continuousOn_intervalIntegrable","path":"D:\\Python\\Quantum","output_mode":"content","-A":8,"glob":"*.lean","head_limit":60},"extra_content":null}]