[{"type":"thinking","thinking":"Conventions clear: `import Mathlib` wholesale, `open Zeta23 Complex Filter Topology`, `noncomputable section`, `namespace NguyenRH1`, full module doc with archive references. Note line 36 of the LiSides doc: \"The split Sz = {nontrivial zeros} ∪ {−2} on the D-064 rectangle (σ ∈ [−5/2, 2√n]) is ii′-4 territory.\"\n\nNow let me start with ii′-4a. First update todos, then write LiContour.lean §1–3 (L3). I'll develop iteratively: write the file with `sorry`s first? NO — honesty policy: no sorries in new proved files (sorryAx only on intended skeletons). Better: build lemma by lemma with `lake env lean` checking.\n\nStrategy: write the file incrementally, checking with `lake env lean NguyenRH1/LiContour.lean` from the package dir after each chunk.\n\nKey Lean details to nail for ii′-4a:\n\n1. `zeroWindow (a : ℝ) : Set ℂ := {ρ | IsNontrivialZero ρ ∧ a ≤ ρ.im ∧ ρ.im ≤ a + 1}`\n2. `zeroWindow_finite (a : ℝ) : (zeroWindow a).Finite`:\n   - zerosIn T₁ T₂ = {ρ | IsNontrivialZero ρ ∧ T₁ < ρ.im ∧ ρ.im ≤ T₂}\n   - zeroWindow a ⊆ zerosIn (a−1) (a+1): a ≤ im ⟹ a−1 < im ✓; im ≤ a+1 ✓.\n   - `(zerosIn_finite (a−1) (a+1)).subset hsubset`\n3. ZeroCountProp:\n```lean\ndef ZeroCountProp : Prop :=\n  ∀ t : ℝ, 2 ≤ t → (Nat.card (zeroWindow t) : ℝ) ≤ C0hat (t + 1)\n```\n   Nat.card of a set coerced to a type — `Nat.card (zeroWindow t)` — zeroWindow t is a Set ℂ; Nat.card expects a Type — `Nat.card (zeroWindow t)` where the set coerces to a subtype ✓ (Set coercion to Sort). Need Finite instance for Nat.card to be the \"right\" value: Nat.card is defined via toFinite-independent? Nat.card α = if finite then card else 0 — actually `Nat.card` is defined for any type and equals the cardinality for finite types (0 for infinite). `Nat.card_eq_of_finite`? The pigeonhole will need: from (Nat.card W : ℝ) ≤ C, conclude things about a Finset of W. With Finite W: get `W.toFinset` (needs Fintype — `Set.Finite.fintype : s.Finite → Fintype s` — `Set.Finite.fintype (h : s.Finite) : Fintype s`). \n\n   Hmm wait — Set.Finite.fintype is noncomputable ✓ fine. card: `Set.Finite.toFinset`? With `hs : s.Finite`, `hs.toFinset : Finset α` with `hs.mem_toFinset : x ∈ hs.toFinset ↔ x ∈ s`. And card relation: `Nat.card s = (hs.toFinset).card`? There's `Set.Finite.card_toFinset`? or Nat.card_coe_set_eq: `Nat.card s = s.toFinset.card` for Fintype... `Set.Nat.card_coe_set_eq : Nat.card s = ...`? There's `Set.ncard`: `s.ncard = Nat.card s` and `Set.Finite.toFinset`... `Set.ncard_eq_toFinset_card'`? For hs : s.Finite: `hs.ncard_toFinset_eq : s.ncard = hs.toFinset.card`? Something like `Set.ncard_coe_Finset`/`Set.Finite.ncard_toFinset`. I'll find it in implementation.\n\n4. C0hat lower bound: `two_le_C0hat {t : ℝ} (ht : 1 ≤ t) : 2 ≤ C0hat t`:\n   C0hat t = 0.433 log(t+2) + 0.886 log log(t+2) + 2.9. t ≥ 1: t+2 ≥ 3 > e ⟹ log(t+2) ≥ 1 ⟹ log log(t+2) ≥ 0. So C0hat t ≥ 0.433·1 + 0 + 2.9 = 3.33 ≥ 2. Wait — need log(t+2) ≥ 1 ⟸ t+2 ≥ e: t ≥ 1 ⟹ t+2 ≥ 3 ≥ e ✓ (e ≤ 3: `Real.exp_one_lt_d9`? e < 3: `Real.exp_one_lt_d9 : Real.exp 1 < 2.7182818286`? there's `Real.exp_one_lt_d9`; or Real.exp 1 < 3 via `Real.exp_one_lt_...`? nlinarith with Real.exp_one_lt_d9 hmm; or log 3 ≥ 1 ⟺ 3 ≥ e: `Real.le_log_iff_exp_le`? For implementation: Real.log 3 ≥ 1 ⟸ Real.exp 1 ≤ 3. There's `Real.exp_one_lt_d9 : exp 1 < 2.7182818286` ⟹ < 3 ✓. Or `Real.one_le_log_iff`? I'll manage.)\n   Then: 0.433·log(t+2) ≥ 0.433·1 = 0.433 (mul_le_mul_of_nonneg_left), 0.886·loglog ≥ 0 (mul_nonneg, log_nonneg of log(t+2) ≥ 1), + 2.9. Total ≥ 3.33 ≥ 2 ✓.\n   \n   Actually for the assembly I need 2(k+1) ≤ 3C from (k+1) ≤ C+1 and C ≥ 2: 2(k+1) ≤ 2(C+1) ≤ 3C ⟺ 2 ≤ C ✓.\n\n5. exists_avoiding_midpoint — the pure combinatorial heart. Let me write it carefully:\n\n```lean\ntheorem exists_avoiding_midpoint {k : ℕ} (a : ℝ) (S : Finset ℝ)\n    (hS : ∀ x ∈ S, a ≤ x ∧ x ≤ a + 1) (hcard : S.card ≤ k) :\n    ∃ T : ℝ, a ≤ T ∧ T ≤ a + 1 ∧ ∀ x ∈ S, |x - T| ≥ 1 / (2 * (k + 1)) := by\n  classical\n  set w : ℝ := 1 / (2 * (k + 1)) with hw_def\n  have hw : 0 < w := by positivity  -- k+1 ≥ 1\n  -- candidate points c j = a + (2j+1)·w, j ∈ range (k+1)\n  -- wait: T_j = a + (2j+1)/(2(k+1)) = a + (2j+1)·w ✓ since w = 1/(2(k+1)).\n  set c : ℕ → ℝ := fun j => a + (2 * j + 1) * w with hc_def\n  -- candidates in range\n  have hmem : ∀ j < k + 1, a ≤ c j ∧ c j ≤ a + 1 := ...\n  -- |c i − c j| = |i − j| · 2w for i j\n  have hdist : ∀ i j : ℕ, c i - c j = (2 * (i : ℝ) - 2 * j) * w := fun i j => by ring\n  -- bad set\n  set Bad : Finset ℕ := (Finset.range (k + 1)).filter (fun j => ∃ x ∈ S, |x - c j| < w)\n  ...\n```\n\nWait — careful with the distance scale: clearance target is w = 1/(2(k+1)); adjacent candidates are 2w apart: c(j+1) − c j = 2w. Bad j: ∃ x ∈ S, |x − c j| < w. If j₁, j₂ both bad via same x: |c j₁ − c j₂| ≤ |c j₁ − x| + |x − c j₂| < 2w ⟹ |i−j|·2w < 2w ⟹ |i−j| < 1 ⟹ i = j ✓.\n\n- injOn: φ : ∀ j ∈ Bad, {x // x ∈ S}... use Finset.card_le_card_of_injOn: needs f : ℕ → ℝ with ∀ j ∈ Bad, f j ∈ S and Set.InjOn f Bad. Then Bad.card ≤ S.card ≤ k.\n  f via choice: for j ∈ Bad, ∃ x ∈ S, |x − c j| < w — choose. `Finset.card_le_card_of_injOn : (∀ a ∈ s, f a ∈ t) → Set.InjOn f s → s.card ≤ t.card` ✓ exists.\n- Then ∃ j ∈ range(k+1), j ∉ Bad: card Bad ≤ k < k+1 = card (range (k+1)): \n  `Finset.exists_mem_not_mem_of_card_lt_card`? hmm — there's `Finset.exists_mem_not_mem_of_card_lt_card : s.card < t.card → ∃ a ∈ t, a ∉ s`? I believe something like `Finset.exists_mem_not_mem_of_card_lt`... Let me just plan: by_contra: if range(k+1) ⊆ Bad then card(range) ≤ card Bad ≤ k < k+1 contradiction. Finset.card_le_card (subset) — simple.\n- For that j: ∀ x ∈ S, |x − c j| ≥ w: from j ∉ Bad: ¬∃ x ∈ S, |x−c j| < w ⟹ ∀ x ∈ S, ¬(|x−c j| < w) ⟹ ≥ w (not_lt ⟹ ge).\n- Conclusion with T = c j.\n\nThe arithmetic |c i − c j| < 2w ⟹ i = j: c i − c j = (2i − 2j)w (integers cast); |(2i−2j)w| = |2(i−j)|·w (w > 0): = 2|i−j|w. If i ≠ j: |i−j| ≥ 1 ⟹ 2|i−j|w ≥ 2w — contradiction with < 2w. In Lean: work with ((i:ℝ) − j) via Int or directly reals: (2i+1)w − (2j+1)w = (2i − 2j)w as reals: 2*((i:ℝ)−(j:ℝ))*w. |(i:ℝ)−(j:ℝ)| ≥ 1 for i ≠ j: `Nat.one_le_iff...`: |((i : ℝ) - j)| = |(i−j : ℤ)| cast: abs_of... `Nat.cast_le`: i ≠ j ⟹ i < j ∨ j < i ⟹ (i:ℝ) + 1 ≤ j or j+1 ≤ i ⟹ |(i:ℝ)−(j:ℝ)| ≥ 1 ✓. nlinarith/linarith glue.\n\n6. exists_zero_avoiding_T:\n```lean\ntheorem exists_zero_avoiding_T (hZC : ZeroCountProp) {a : ℝ} (ha : 2 ≤ a) :\n    ∃ T : ℝ, a ≤ T ∧ T ≤ a + 1 ∧\n      ∀ ρ : ℂ, IsNontrivialZero ρ → a ≤ ρ.im → ρ.im ≤ a + 1 →\n        1 / (3 * C0hat (a + 1)) ≤ |ρ.im - T| := by\n  classical\n  haveI := Set.finite_coe_iff.mpr (zeroWindow_finite a)  -- Finite (zeroWindow a)\n  -- hmm: zeroWindow_finite gives (zeroWindow a).Finite; the subtype Finite instance\n  set W := zeroWindow a with hW\n  set S : Finset ℝ := (finite toFinset).image (fun ρ => (ρ : ℂ).im)\n  ...\n```\n\nHmm — Set.Finite.toFinset: for hfin : (zeroWindow a).Finite: `hfin.toFinset : Finset ℂ` with membership ↔ ∈ zeroWindow a. Then S := hfin.toFinset.image (Complex.im). card S ≤ hfin.toFinset.card = Nat.card (zeroWindow a) (via Set.Finite.toFinset + Nat.card: `Set.Finite.card_toFinset : s.Finite → s.toFinset.card = s.ncard`? or ncard... `Set.ncard_eq_toFinset_card'`? hmm: `Set.Finite.toFinset` is defined for a Finite set; `Set.ncard (s) = s.toFinset.card`? There's `Set.ncard_eq_toFinset_card' (s : Finset?)`... I'll figure out: the chain I need: S.card ≤ W.toFinset.card = W.ncard = Nat.card W ≤ C0hat(a+1) (hZC). \n\nFinset.image card: `Finset.card_image_le : (s.image f).card ≤ s.card` ✓.\n\nThen k := W.toFinset.card... wait exists_avoiding_midpoint wants S.card ≤ k with k : ℕ. Use k := hfin.toFinset.card: hcard: S.card ≤ k ✓ (card_image_le). Get T with clearance 1/(2(k+1)). Then need 1/(3·C0hat(a+1)) ≤ 1/(2(k+1)) ⟺ 2(k+1) ≤ 3·C0hat(a+1) (both sides positive): from (k : ℝ) ≤ C0hat(a+1) (hZC a ha — the Nat.card = k needs the card-toFinset relation... hfin.toFinset.card = Nat.card (zeroWindow a): `Set.Finite.toFinset` card: `Set.Finite.card_toFinset`? Let me search mathlib during implementation: likely `Set.Finite.toFinset` + `Set.ncard_eq_toFinset_card'`: theorem Set.ncard_eq_toFinset_card' (s : Set α) [Fintype s] : s.ncard = s.toFinset.card — different toFinset (Fintype-based vs Finite-based). Ugh, two toFinset variants. For hs : s.Finite: `hs.toFinset` and `hs.mem_toFinset`; and `hs.ncard_eq_toFinset_card`? I recall `Set.Finite.ncard_toFinset (hs : s.Finite) : s.ncard = hs.toFinset.card`?? I'll check. And Nat.card vs ncard: `Set.Nat.card_coe_set_eq : Nat.card s = s.ncard` ✓ exists (Set.Nat.card_coe_set_eq). Chain: hfin.toFinset.card = s.ncard (hfin lemma) = Nat.card s (symm). \n\nThen: 2((k:ℝ)+1) ≤ 3·C: (k:ℝ) ≤ C ⟹ k+1 ≤ C+1 ⟹ 2(k+1) ≤ 2C+2 ≤ 3C ⟺ C ≥ 2 ✓ (two_le_C0hat with a+1 ≥ 3 ≥ 1 ✓).\n\nDivision flip: 1/(3C) ≤ 1/(2(k+1)) ⟺ 2(k+1) ≤ 3C with 0 < 2(k+1), 0 < 3C: `one_div_le_one_div_of_le` : 0 < a → a ≤ b → 1/b ≤ 1/a ✓ exists (one_div_le_one_div_of_le (ha : 0 < a) (h : a ≤ b) : 1/b ≤ 1/a). ✓\n\nThen final: for ρ with the hypotheses: ρ ∈ zeroWindow a ⟹ ρ ∈ hfin.toFinset ⟹ ρ.im ∈ S (mem_image) ⟹ |ρ.im − T| ≥ 1/(2(k+1)) ≥ 1/(3C) ✓.\n\nOK — ready to implement ii′-4a. One more check — exact names: `Finset.card_le_card_of_injOn`, `one_div_le_one_div_of_le`, `Set.Nat.card_coe_set_eq`, `Set.Finite.toFinset` API, `Finset.filter` decidability of the ∃ (classical ✓), `Real.add_one_le_exp` (for later), `zerosIn_finite` namespace: it's in `namespace Zeta23` (end Zeta23 at line 55-ish) — so `Zeta23.zerosIn_finite`. And IsNontrivialZero is in Zeta23.Statement — opened Zeta23 in LiSides; I'll open Zeta23 too.\n\nAlso C0hat lives in LiSkeleton (namespace NguyenRH1) ✓ same namespace.\n\nLet me now write the file's §1–§3 and iterate with the compiler. I'll create LiContour.lean with a module doc and the L3 content first (4a), get it green, commit; then 4b (kFun bounds) appended; then 4c.\n\nActually — for efficiency, let me write the whole skeleton of §1–3 in one go and iterate on errors. Development loop: `cd research/lean/NguyenRH1 && ~/.elan/bin/lake env lean NguyenRH1/LiContour.lean`. PATH: handoff says elan at ~/.elan/bin, export per shell: `export PATH=\"$HOME/.elan/bin:$PATH\"`.\n\nLet me write §1–3 now. Careful with:\n- `open Zeta23 Complex Filter Topology` + `open scoped Nat`\n- noncomputable section + namespace NguyenRH1\n\nDraft §1–3:\n\n```lean\n/-\nNguyenRH1/LiContour.lean — tier ii′ sub-stage ii′-4 (D-064 §5 graph L3+L1,\nD-036 §2–3): the zero-avoiding ordinate T (pigeonhole on the perimeter\nunit-window count bound) and the Lagarias-kernel norm bounds.\n\nL3 (D-036 §2): in every unit ordinate window [a, a+1] (a ≥ 2) with at most\nĈ₀(a+1) zero ordinates, one of the k+1 equally-spaced midpoints\nT_j = a + (2j+1)/(2(k+1)) has distance ≥ 1/(2(k+1)) ≥ 1/(3·Ĉ₀(a+1)) from\nevery zero ordinate in the window (k+1 candidates, each zero kills at most\none: adjacent candidates are 2·(1/(2(k+1))) apart). The count input is the\nperimeter hypothesis `ZeroCountProp` (Trudgian 2014 N(T)/S(T), D-062 §4;\nĈ₀ = C0hat is D-056 §2's majorant, already in LiSkeleton).\n\nL1 (D-036 §3): the kernel kFun n s = (s/(s−1))ⁿ − 1 satisfies\n  * ‖kFun n s‖ ≤ 2                       (re s ≤ 1/2: |s/(s−1)| ≤ 1)\n  * ‖kFun n (s+1)‖ ≤ e⁴ + 1              (|re s| ≤ 3, n ≤ (im s)²: the\n    horizontals, |1+1/s| ≤ 1 + (σ+1)/(σ²+T²) ≤ 1 + 4/n)\n  * ‖kFun n (s+1)‖ ≤ e^{√n/2} + 1        (2√n ≤ re s: the right vertical,\n    |1+1/s| ≤ 1 + 1/|s| ≤ 1 + 1/(2√n))\n  * kFun n (−2) = (2/3)ⁿ − 1, hence ‖kFun n (−2)‖ ≤ 1 (trivial-zero term).\n\nAlso the deferred trivial-zero simplicity (ii′-1b(iii) note): zeroMult(−2) = 1,\nvia ζ(s) = (s+2)·G(s) near −2 with G(s) = Λ(s)/H(s),\nH(s) = 4·π^{−s/2}·Γ(s/2+2)/s = (s+2)·ΓR(s) (punctured), H(−2) = −2π ≠ 0,\nΛ(−2) = Λ(3) = ΓR(3)·ζ(3) ≠ 0.\n\nArchive references: D-036 §2–3, D-056 §2, D-064 §5 (L3/L1), D-066 §6.\n-/\nimport Mathlib\nimport Zeta23.Statement\nimport NguyenRH1.LiSides\nimport NguyenRH1.LiSkeleton\n\nopen Zeta23 Complex Filter Topology\nopen scoped Nat\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. The unit ordinate window and the perimeter count hypothesis -/\n\n/-- The nontrivial zeros with ordinate in the unit window [a, a+1]. -/\ndef zeroWindow (a : ℝ) : Set ℂ :=\n  {ρ | IsNontrivialZero ρ ∧ a ≤ ρ.im ∧ ρ.im ≤ a + 1}\n\n/-- Finiteness of the unit ordinate window (Zeta23 `zerosIn_finite`). -/\ntheorem zeroWindow_finite (a : ℝ) : (zeroWindow a).Finite := by\n  apply Set.Finite.subset (zerosIn_finite (a - 1) (a + 1))\n  intro ρ hρ\n  refine ⟨hρ.1, ?_, hρ.2.2⟩\n  linarith [hρ.2.1]\n\n/-- [PERIMETER — Trudgian 2014 N(T)/S(T), D-062 §4] The unit-window\nzero-count bound: at most Ĉ₀(t+1) nontrivial zeros have ordinates in\n[t, t+1] (t ≥ 2). This is the declared counting input for the L3\npigeonhole; Ĉ₀ = `C0hat` is D-056 §2's honest majorant. -/\ndef ZeroCountProp : Prop :=\n  ∀ t : ℝ, 2 ≤ t → (Nat.card (zeroWindow t) : ℝ) ≤ C0hat (t + 1)\n```\n\nWait — zerosIn_finite is in namespace Zeta23 (the file ended `end Zeta23`) — with `open Zeta23` it's just `zerosIn_finite` ✓. Also check: `zerosIn` def is in Zeta23 namespace in Statement.lean? The grep showed `Zeta23/Statement.lean:46:def zerosIn` — need to check namespace there; SeamClosed.lean:47 `zerosIn_finite` inside `namespace Zeta23`. With open Zeta23 both accessible ✓.\n\nC0hat lower bound:\n\n```lean\n/-- 2 ≤ Ĉ₀(t) for t ≥ 1 (indeed 3.33: log(t+2) ≥ 1 since t + 2 ≥ 3 > e). -/\ntheorem two_le_C0hat {t : ℝ} (ht : 1 ≤ t) : 2 ≤ C0hat t := by\n  have h3 : 3 ≤ t + 2 := by linarith\n  have hlog : 1 ≤ Real.log (t + 2) := by\n    -- 1 = log e ≤ log (t+2) since e ≤ 3 ≤ t+2\n    have he : Real.exp 1 ≤ t + 2 := by\n      have := Real.exp_one_lt_d9\n      linarith [this.le.trans ... ] hmm\n```\n\nReal.exp_one_lt_d9 : Real.exp 1 < 2.7182818286 — so exp 1 < 3 ≤ t+2: linarith with h3. Then 1 ≤ log(t+2): `Real.le_log_iff_exp_le (h : 0 < x) : 1 ≤ log x ↔ exp 1 ≤ x`? hmm the exact name: `Real.le_log_iff_exp_le (hx : 0 < x) : r ≤ log x ↔ exp r ≤ x` ✓ exists. So `(Real.le_log_iff_exp_le (by positivity)).mpr he`... wait need r ≤ Real.log x form ✓.\n\nThen log log(t+2) ≥ 0: `Real.log_nonneg (h : 1 ≤ x)` ✓: log(t+2) ≥ 1 ⟹ log log(t+2) ≥ 0.\n\n```lean\n  have hloglog : 0 ≤ Real.log (Real.log (t + 2)) := Real.log_nonneg hlog\n  unfold C0hat\n  have : (0:ℝ) ≤ 0.433 * Real.log (t + 2) := by positivity  -- 0.433 > 0, log ≥ 1 > 0\n  have : (0:ℝ) ≤ 0.886 * Real.log (Real.log (t + 2)) := by positivity\n  nlinarith / linarith: 0.433·(≥1) + (≥0) + 2.9 ≥ 2 — even simpler: both terms ≥ 0 and 2.9 ≥ 2 ✓ linarith.\n```\n\npositivity for the two products: 0.433 * log(t+2): needs log(t+2) ≥ 0 — positivity knows log_nonneg? positivity extension for Real.log: yes there's one (log_nonneg for 1 ≤ x... positivity has a log extension: `Real.log` positive when 1 ≤ x? I think positivity handles 0 ≤ log x given 1 ≤ x in context? Hmm — the positivity extension for log: `0 < Real.log x` if `1 < x`... To be safe, apply mul_nonneg directly with hlog.le / hloglog.)\n\nNow §2 pigeonhole:\n\n```lean\n/-! ## 2. The midpoint pigeonhole (pure combinatorics) -/\n\n/-- **Midpoint pigeonhole**: a finset S ⊂ [a, a+1] with card S ≤ k avoids\none of the k+1 midpoints a + (2j+1)/(2(k+1)) by ≥ 1/(2(k+1)). (Each point\nof S is within < 1/(2(k+1)) of at most one midpoint, since adjacent\nmidpoints are 1/(k+1) apart; so at most card S ≤ k of the k+1 midpoints\nare blocked.) -/\ntheorem exists_avoiding_midpoint {k : ℕ} (a : ℝ) (S : Finset ℝ)\n    (hS : ∀ x ∈ S, a ≤ x ∧ x ≤ a + 1) (hcard : S.card ≤ k) :\n    ∃ T : ℝ, a ≤ T ∧ T ≤ a + 1 ∧\n      ∀ x ∈ S, 1 / (2 * (k + 1)) ≤ |x - T| := by\n  classical\n  set w : ℝ := 1 / (2 * (k + 1)) with hw_def\n  have hk1 : (0:ℝ) < 2 * (k + 1) := by positivity\n  have hw : 0 < w := one_div_pos.mpr hk1\n  set c : ℕ → ℝ := fun j => a + (2 * j + 1) * w with hc_def\n  -- candidate spread: c i − c j = 2(i − j)·w\n  have hcd : ∀ i j : ℕ, c i - c j = 2 * ((i : ℝ) - (j : ℝ)) * w := fun i j => by\n    simp only [hc_def]; push_cast; ring\n  -- each candidate lies in [a, a+1]\n  have hc_mem : ∀ j < k + 1, a ≤ c j ∧ c j ≤ a + 1 := by\n    intro j hj\n    have hjl : (0:ℝ) ≤ 2 * j + 1 := by positivity\n    have hju : (2:ℝ) * j + 1 ≤ 2 * (k + 1) := by\n      have : j ≤ k := Nat.lt_succ_iff.mp hj\n      nlinarith [this]  hmm — (2j+1) ≤ 2k+1 < 2(k+1)? 2j+1 ≤ 2k+1 and 2(k+1) = 2k+2: 2j+1 ≤ 2(k+1) ⟺ j ≤ k + 1/2 ✓ from j ≤ k. linarith after cast.\n    constructor\n    · have : 0 ≤ (2 * j + 1) * w := mul_nonneg hjl hw.le\n      simp only [hc_def]; linarith\n    · have : (2 * j + 1) * w ≤ 1 := by\n        rw [hw_def]; rw [div_le_iff hk1]... (2j+1)·(1/(2(k+1))) ≤ 1 ⟺ 2j+1 ≤ 2(k+1) ✓\n        calc (2 * (j:ℝ) + 1) * (1 / (2 * (k + 1))) = (2*j+1)/(2*(k+1)) := by ring\n          _ ≤ 1 := by rw [div_le_one hk1]; exact hju\n      simp only [hc_def]; linarith\n  ...\n```\n\nThen the Bad set & injection:\n\n```lean\n  -- bad candidates\n  set Bad : Finset ℕ := (Finset.range (k + 1)).filter\n    (fun j => ∃ x ∈ S, |x - c j| < w) with hBad_def\n  -- choose, for each bad j, a witness x j ∈ S\n  have hbad_wit : ∀ j ∈ Bad, ∃ x ∈ S, |x - c j| < w := fun j hj =>\n    (Finset.mem_filter.mp hj).2\n  choose! f hfS hfw using hbad_wit   -- classical choice on finset\n```\n\nHmm — `choose!` on ∀ j ∈ Bad, ∃ x ∈ S, ... gives f : ℕ → ℝ with hfS : ∀ j ∈ Bad, f j ∈ S and hfw : ∀ j ∈ Bad, |f j − c j| < w. ✓ (`choose!` tactic exists in Mathlib).\n\n```lean\n  -- f is injective on Bad\n  have hinj : Set.InjOn f Bad := by\n    intro i hi j hj hij\n    simp only [Finset.coe_sort] at *   -- hmm Bad is Finset; InjOn on ↑Bad\n    by_contra hne\n    have h1 : |f i - c i| < w := hfw i hi\n    have h2 : |f j - c j| < w := hfw j hj\n    have hcc : |c i - c j| ≤ |c i - f i| + |f i - c j| := by\n      have := abs_sub_le (c i) (f i) (c j)  -- |a−c| ≤ |a−b|+|b−c|\n      ... \n    have hfi : |c i - f i| = |f i - c i| := abs_sub_comm _ _\n    have hfj : f i = f j := hij\n    rw [hfj] at ... \n    -- so |c i − c j| < 2w\n    have hlt : |c i - c j| < 2 * w := by linarith [h1, h2, ...]\n    -- but |c i − c j| = 2|i−j|w ≥ 2w\n    rw [hcd i j] at hlt\n    have h3 : (1:ℝ) ≤ |(i : ℝ) - (j : ℝ)| := by\n      rw [← Nat.cast_one, ...]\n      rcases lt_or_gt_of_ne hne with h | h\n      · have : (i:ℝ) + 1 ≤ j := by exact_mod_cast Nat.add_one_le_of_lt h  -- i < j\n        rw [abs_of_nonpos (by linarith)]; linarith\n      · have : (j:ℝ) + 1 ≤ i := by exact_mod_cast Nat.add_one_le_of_lt h\n        rw [abs_of_nonneg (by linarith)]; linarith\n    have hge : 2 * w ≤ |2 * ((i:ℝ) - (j:ℝ)) * w| := by\n      rw [abs_mul, abs_mul, abs_of_pos hw, abs_of_pos (by norm_num : (0:ℝ) < 2)]\n      nlinarith [h3, hw]\n    linarith [hlt, hge]\n  -- cardinalities\n  have hcardBad : Bad.card ≤ S.card :=\n    Finset.card_le_card_of_injOn f (fun j hj => hfS j hj) hinj\n  -- some candidate is not bad\n  have hlt2 : Bad.card < (Finset.range (k + 1)).card := by\n    rw [Finset.card_range]\n    exact Nat.lt_succ_of_le (hcardBad.trans hcard)\n  obtain ⟨j, hj, hjB⟩ : ∃ j ∈ Finset.range (k + 1), j ∉ Bad := by\n    by_contra hcon\n    push_neg at hcon\n    have : (Finset.range (k + 1)).card ≤ Bad.card :=\n      Finset.card_le_card (fun x hx => by ... hcon x hx → x ∈ Bad)\n    -- hcon : ∀ j, j ∈ range → j ∈ Bad (after push_neg of ∃ j ∈ range, j ∉ Bad)\n    linarith [hlt2]  / exact absurd (this) (by omega using hlt2)\n  ...\n```\n\nCareful: push_neg on ¬∃ j ∈ range, j ∉ Bad gives ∀ j ∈ range, j ∈ Bad ✓ (`Finset.forall_mem_...` push_neg handles ∈ patterns ✓).\n\n  Then:\n```lean\n  have hjk : j < k + 1 := Finset.mem_range.mp hj\n  refine ⟨c j, (hc_mem j hjk).1, (hc_mem j hjk).2, fun x hx => ?_⟩\n  have : ¬ |x - c j| < w := by\n    intro hlt\n    exact hjB (Finset.mem_filter.mpr ⟨hj, ⟨x, hx, hlt⟩⟩)\n  exact not_lt.mp this\n```\n\nWait — hjB : j ∉ Bad; membership: j ∈ Bad ⟺ j ∈ range ∧ ∃ x ∈ S, ... ✓ mem_filter. ✓.\n\nThe `Set.InjOn f Bad` — InjOn expects a Set; Bad coerces ✓. `Finset.card_le_card_of_injOn (f : α → β) (hf : ∀ a ∈ s, f a ∈ t) (inj : Set.InjOn f s) : s.card ≤ t.card` ✓ exists in Mathlib (Finset.card_le_card_of_injOn).\n\nOne subtlety: `choose!` — syntax: `choose! f hfS hfw using hbad_wit` where hbad_wit : ∀ j ∈ Bad, ∃ x ∈ S, |x − c j| < w. Hmm — ∀ j ∈ Bad desugars to ∀ j, j ∈ Bad → ∃ x, x ∈ S ∧ ...; choose! should give f : ℕ → ℝ, hfS : ∀ (j : ℕ), j ∈ Bad → f j ∈ S, hfw : ∀ (j : ℕ), j ∈ Bad → |f j − c j| < w. I believe choose/choose! handles this ✓.\n\nThen §3:\n\n```lean\n/-! ## 3. L3: the zero-avoiding ordinate -/\n\n/-- **L3** (D-036 §2): given the perimeter count bound `ZeroCountProp`,\nevery unit window [a, a+1] (a ≥ 2) contains an ordinate T at distance\n≥ 1/(3·Ĉ₀(a+1)) from every zero ordinate in the window. -/\ntheorem exists_zero_avoiding_T (hZC : ZeroCountProp) {a : ℝ} (ha : 2 ≤ a) :\n    ∃ T : ℝ, a ≤ T ∧ T ≤ a + 1 ∧\n      ∀ ρ : ℂ, IsNontrivialZero ρ → a ≤ ρ.im → ρ.im ≤ a + 1 →\n        1 / (3 * C0hat (a + 1)) ≤ |ρ.im - T| := by\n  classical\n  have hfin := zeroWindow_finite a\n  haveI : Finite (zeroWindow a) := Set.finite_coe_iff.mpr hfin  -- or Fintype\n  ...\n```\n\nHmm — for Nat.card of the subtype: `Nat.card (zeroWindow a)` — needs `Finite ↥(zeroWindow a)` instance — haveI with Set.finite_coe_iff... hmm actually Set.finite_coe_iff : ↥s.Finite ↔ Finite ↥s? It's `Set.finite_coe_iff : s.Finite ↔ Finite s` ✓.\n\nThen:\n```lean\n  set WF : Finset ℂ := hfin.toFinset with hWF\n  have hWFmem : ∀ ρ : ℂ, ρ ∈ WF ↔ ρ ∈ zeroWindow a := Set.Finite.mem_toFinset hfin\n  set S : Finset ℝ := WF.image Complex.im with hS_def\n  have hScard : S.card ≤ WF.card := Finset.card_image_le\n  -- WF.card = Nat.card (zeroWindow a)\n  have hWFcard : (WF.card : ℝ) ≤ C0hat (a + 1) := by\n    have h1 := hZC a ha\n    have h2 : Nat.card (zeroWindow a) = WF.card := by\n      rw [Set.Nat.card_coe_set_eq]  -- Nat.card ↥s = s.ncard\n      rw [hWF]; exact (Set.Finite.ncard_toFinset hfin).symm? \n    rw [h2] at h1; exact h1\n```\n\n`Set.Finite.ncard_toFinset`? Let me think: `Set.Finite.toFinset` card relation: I believe `Set.Finite.card_toFinset : hs.toFinset.card = s.ncard`? Hmm — Mathlib: `Set.Finite.toFinset (hs : s.Finite) : Finset α`; lemmas: `Set.Finite.mem_toFinset`, `Set.Finite.toFinset_subset...` and `Set.Finite.card_toFinset : hs.toFinset.card = s.ncard`?? hmm. Hmm, actually I recall `Set.Finite.toFinset` uses `Set.ncard` in `Set.Finite.card_toFinset (hs : s.Finite) : hs.toFinset.card = s.ncard`. I'll check in implementation.\n\n  Then apply exists_avoiding_midpoint with k := WF.card, a, S:\n  - hS: ∀ x ∈ S, a ≤ x ∧ x ≤ a+1: x ∈ S ⟹ x = ρ.im for some ρ ∈ WF ⟹ ρ ∈ zeroWindow a ⟹ bounds ✓.\n  - hcard: S.card ≤ WF.card ✓ (image).\n  Get T, hT1, hT2, hT3 : ∀ x ∈ S, 1/(2(WF.card+1)) ≤ |x − T|.\n  \n  Then final: for ρ hyp: ρ.im ∈ S: `Finset.mem_image.mpr ⟨ρ, mem, rfl⟩` ✓. So 1/(2(k+1)) ≤ |ρ.im − T|. And 1/(3C) ≤ 1/(2(k+1)): one_div_le_one_div_of_le:\n  - 0 < 2(k+1): positivity ✓.\n  - 2(k+1) ≤ 3C: (k:ℝ) ≤ C (hWFcard), C ≥ 2 (two_le_C0hat, a+1 ≥ 3 ≥ 1) ⟹ 2(k+1) ≤ 2C+2 ≤ 3C ⟺ C ≥ 2 ✓ linarith/nlinarith.\n\n  Both sides: target `1 / (3 * C0hat (a + 1)) ≤ |ρ.im - T|` via le_trans (one_div_le_one_div_of_le (show 0 < 2*((k:ℝ)+1) ...) (show 2*((k:ℝ)+1) ≤ 3*C ...)) (hT3 ρ.im (mem)) — careful direction: one_div_le_one_div_of_le (ha : 0 < a) (h : a ≤ b) : 1 / b ≤ 1 / a. With a := 2(k+1), b := 3C: gives 1/(3C) ≤ 1/(2(k+1)) ✓ then trans with hT3 ✓.\n\nCast care: 2 * (k+1) with k : ℕ vs the real 2*(k+1) — in exists_avoiding_midpoint the clearance is `1 / (2 * (k + 1))` with (k+1 : ℝ)? The statement writes `2 * (k + 1)` — with k : ℕ and T : ℝ, Lean elaborates 2*(k+1) in ℝ with Nat casts: 2 * (↑k + 1)? Hmm — `1 / (2 * (k + 1))`: the whole expression is ℝ (since |x − T| : ℝ and ≤ between ℝ). 2*(k+1): k : ℕ coerced... (k+1) would elaborate in ℕ then cast? `2 * (k + 1)` with expected ℝ: 2 is ℝ, so (k+1) must be ℝ: k coerced to ℝ, 1 : ℝ — so it's 2 * (↑k + 1) ✓ good (not ↑(k+1) — actually both are equal by push_cast but elaboration gives (↑k + 1): fine, push_cast/norm_cast handles).\n\nIn hcardBad/trans: Nat.lt_succ_of_le : n ≤ k → n < k+1 ✓.\n\nOK — I'm confident in the overall shape. Time to write and compile iteratively. For iterations, single-file check: cd research/lean/NguyenRH1 && export PATH and lake env lean.\n\nLet me write §1–3 now (L3 complete), compile, fix, commit (sub-stage 4a). Then proceed to 4b.\n\nOne more consideration on `hc_mem` upper bound: c j = a + (2j+1)w with j ≤ k: (2j+1) ≤ 2k+1; w = 1/(2(k+1)): (2j+1)w ≤ (2k+1)/(2(k+1)) ≤ 1 ✓. linarith-friendly.\n\nActually — do I even need the candidates' membership hS hypothesis? The pigeonhole as designed doesn't use hS (points outside [a,a+1] would still only kill one candidate each)! Interesting — the candidate argument works for ANY finite S with card ≤ k. hS is unneeded. But keeping it is harmless... no — REMOVE it: simpler statement, and the wrapper doesn't even need the window bounds for S. Wait, but then the \"T ∈ [a, a+1]\" conclusion is independent of S ✓ true regardless. Yes — drop hS from exists_avoiding_midpoint (simpler). Hmm — but semantically the \"right\" statement includes it... For Lean economy: drop it. Actually wait, let me keep it minimal: drop.\n\nHmm, one catch — I should double-check `Finset.card_le_card_of_injOn` signature: `theorem Finset.card_le_card_of_injOn {s : Finset α} {t : Finset β} (f : α → β) (hf : ∀ a ∈ s, f a ∈ t) (f_inj : Set.InjOn f s) : s.card ≤ t.card` ✓ that's right.\n\nAnd `Set.InjOn f Bad` where Bad : Finset ℕ — coercion to Set ℕ ✓.\n\nAlright, writing the file now. I'll write §1–§3, compile.","signature":""},{"type":"text","text":"Conventions clear. Marking docs read and starting ii′-4a (L3)."},{"type":"tool_use","id":"TodoWrite_61","name":"TodoWrite","input":{"todos":[{"activeForm":"Reading design docs for ii′-4 content","content":"Read design docs: D-036 §2, D-064 §4, D-066 §6 (zeroMult route)","status":"completed"},{"activeForm":"Surveying Lean package state","content":"Survey Lean package state (LiSkeleton perimeter, LiSides zeroMult/Jlag)","status":"completed"},{"activeForm":"Implementing L3 zero-avoiding T","content":"ii′-4a: L3 pigeonhole — zeroWindow/ZeroCountProp + exists_avoiding_midpoint + exists_zero_avoiding_T","status":"in_progress"},{"activeForm":"Implementing L1 kernel bounds","content":"ii′-4b: L1 kernel bounds (kFun ≤ 2, e⁴+1, e^{√n/2}+1, kFun(−2))","status":"pending"},{"activeForm":"Proving trivial-zero simplicity","content":"ii′-4c: zeroMult(−2) = 1 via FE + ΓR pole + ζ(3) ≠ 0","status":"pending"},{"activeForm":"Building and auditing axioms","content":"Full build + axiom audit","status":"pending"},{"activeForm":"Running session end protocol","content":"Session end protocol: journal-021, NGUYEN.md, STATE.md, commit","status":"pending"}]},"extra_content":null}]