[{"type":"thinking","thinking":"The user wants:\n1. Update NGUYEN.md to track tier ii′ as a proper checklist (sub-stages ii′-1a..7).\n2. Any other places that need documentation of this new project, documented fully and correctly.\n3. Then proceed with session 015: ii′-1a — liCoeff pairing fix + summability proof.\n\nLet me first add the checklist to NGUYEN.md. Where? §5 Phase 5 area — a new subsection for tier ii′ with checkboxes. Also check other places: STATE.md already has the plan. The session log in NGUYEN.md §8.6 has session 014. Maybe also add a \"TIER ii′\" checklist block under Phase 5 item 5.1 or as a new Phase 5B.\n\nOther documentation places:\n- research/derivations/index.md — done (D-064 registered).\n- STATE.md — done.\n- research/journal/session-014.md — done.\n- NGUYEN.md §5 — needs the checklist.\n- Maybe the graveyard/ledger — no (no results/dead ends yet).\n- The dashboard mentioned in commit 4ad1f1b \"parses NGUYEN.md §5 live\" — the website dashboard parses §5, so format the checklist consistently with existing checkbox syntax ([ ]/[x]).\n\nLet me add a checklist block. I'll add it right after the 5.1/5.2/5.3/5.4 items in Phase 5, or as a dedicated \"PHASE 5B — TIER ii′\" section. Looking at the structure, Phase 5 has items 5.1–5.4. I'll add a nested checklist under 5.1's tier-ii′ paragraph or as its own subsection. Cleanest: a new subsection \"### 🔶 PHASE 5B — TIER ii′ (close SfBoundProp)\" after Phase 5, with items ii′-0 through ii′-7, marking ii′-0 complete.\n\nLet me write it, then start ii′-1a.\n\nFor ii′-1a, the work:\n1. Check Mathlib for the conjugation lemma `riemannZeta (conj s) = conj (riemannZeta s)`.\n2. Design the new liCoeff definition:\n\n```lean\ndef liCoeff (n : ℕ) : ℂ :=\n  ∑' ρ : {ρ // IsNontrivialZero ρ},\n    (zeroMult ρ : ℂ) / 2 * ((1 - (1 - 1/(ρ:ℂ))^n) + (1 - (1 - 1/(star ρ:ℂ))^n))\n```\n\nWait — need care: star ρ for ρ in the subtype; star (ρ:ℂ) is conj. The summand: (mult/2)·(f ρ + f ρ̄). Since f ρ̄ = conj (f ρ) (because the operations are real-rational: 1 − (1 − 1/ρ̄)ⁿ = conj(1 − (1−1/ρ)ⁿ) — true: conj is a ring hom), the summand is (mult/2)·2·Re(f ρ) = mult·Re(f ρ) — real.\n\nSummability proof: ‖summand‖ = mult·|Re(f ρ)| ≤ mult·(|f ρ| + |f ρ̄|)/2 = mult·|f ρ| (since |f ρ̄| = |f ρ|). Hmm — that bound gives mult·|f ρ| ~ n·mult/|ρ| — NOT summable! The whole point is the CANCELLATION in Re(f ρ): Re(f ρ) = Re[1−(1−1/ρ)ⁿ] and for large ρ this is ≈ n·σ/|ρ|² + O(n²/|ρ|²) = O(n²/|ρ|²). So need the sharper bound |Re(f ρ)| ≤ C(n)/|ρ|².\n\nLet me get the bound right: f(ρ) = 1 − wⁿ with w = 1 − 1/ρ. Write wⁿ = exp(n log w)? Avoid complex log. Better: wⁿ − 1 = (w−1)·Σ_{j=0}^{n−1} w^j. So f(ρ) = −(w−1)·S, S = Σ_{j=0}^{n−1} w^j, w−1 = −1/ρ. f(ρ) = S/ρ. Re f(ρ) = Re(S/ρ). Hmm, need Re(S/ρ) = O(n²/|ρ|²):\n\nS = Σ w^j, and S/ρ: write S = n + Σ_{j}(w^j − 1). w^j − 1 = (w−1)Σ_{i<j} w^i, so |w^j − 1| ≤ j·|w−1|·M where M = max(1,|w|)^{n−1}. |w−1| = 1/|ρ|. So |S − n| ≤ |w−1|M·Σ j = |w−1|M·n(n−1)/2 ≤ n²/(2|ρ|)·M.\n\nf(ρ) = S/ρ = n/ρ + (S−n)/ρ. Re(n/ρ) = nσ/|ρ|². So Re f(ρ) = nσ/|ρ|² + Re((S−n)/ρ), and |Re((S−n)/ρ)| ≤ |S−n|/|ρ| ≤ n²M/(2|ρ|²).\n\n|Re f(ρ)| ≤ nσ/|ρ|² + n²M/(2|ρ|²) ≤ n/|ρ|² + n²M/(2|ρ|²) (σ ≤ 1).\n\nM = max(1,|w|)^{n−1}: |w| = |1−1/ρ| ≤ 1+1/|ρ| ≤ 1+1/(2n) for |ρ| ≥ 2n. So M ≤ (1+1/(2n))^n ≤ e^{1/2} ≤ 2. So:\n\n**|Re f(ρ)| ≤ (n + n²)/|ρ|² ≤ 2n²/|ρ|² for |ρ| ≥ 2n.**\n\nAnd for |ρ| < 2n (finitely many zeros — finite by compactness/zerosIn_finite): the sum over them is a finite sum — fine (Summable on a finite set + summable tail).\n\nSo the summand g(ρ) = mult·Re f(ρ) satisfies |g(ρ)| ≤ 2n²·mult/|ρ|² for |ρ| ≥ 2n. And Σ_{|ρ|≥2n} mult/|ρ|² < ∞ follows from zero_sum_inv_sq: Σ mult/(1+‖γ_ρ‖²) < ∞ with 1+‖γ_ρ‖² = 1 + γ² + (1/2−σ)² ≤ ... hmm need the comparison direction: want Σ mult/|ρ|². |ρ|² = σ²+γ². 1+‖γ_ρ‖² = 1+γ²+(1/2−σ)². Since σ ∈ (0,1): (1/2−σ)² ≤ 1/4, σ² ≤ 1. So 1+‖γ_ρ‖² ≤ 1+γ²+1/4 ≤ ... and |ρ|² = σ²+γ² ≤ 1+γ². Hmm: |ρ|² ≤ γ²+1 and 1+‖γ_ρ‖² ≥ 1+γ². So |ρ|² ≤ 1+‖γ_ρ‖². Therefore mult/|ρ|² ≥ mult/(1+‖γ_ρ‖²) — WRONG DIRECTION for comparison (we have summability of the SMALLER terms). \n\nNeed: Σ mult/|ρ|² < ∞ from Σ mult/(1+‖γ_ρ‖²) < ∞. |ρ|² = σ²+γ² ≤ 1+γ² ≤ 1+γ²+(1/2−σ)² = 1+‖γ_ρ‖² + ... no: 1+‖γ_ρ‖² = 1+γ²+(1/2−σ)² ≥ 1+γ² ≥ |ρ|²... wait σ² ≤ 1 so |ρ|² = σ²+γ² ≤ 1+γ² ≤ 1+‖γ_ρ‖² ✓. So |ρ|² ≤ 1+‖γ_ρ‖², i.e. 1/|ρ|² ≥ 1/(1+‖γ_ρ‖²). So the summable family mult/(1+‖γ_ρ‖²) is termwise ≤ mult/|ρ|² — comparison test gives nothing (summability of smaller terms doesn't imply summability of larger).\n\nHmm! But wait — that can't be right: Σ mult/|ρ|² DOES converge (standard). The issue is |ρ|² vs ‖γ_ρ‖²: ‖γ_ρ‖² = γ² + (1/2−σ)². |ρ|² = γ² + σ². These are comparable: |ρ|² ≤ γ² + 1 ≤ (1+γ²) and ‖γ_ρ‖² ≥ γ². So mult/|ρ|² ≤ mult/(γ²) ≤ mult/(‖γ_ρ‖²)·(‖γ_ρ‖²/γ²)·... For γ ≥ 1: ‖γ_ρ‖² = γ² + (1/2−σ)² ≤ γ² + 1/4 ≤ (5/4)γ². So mult/|ρ|² ≤ mult/γ² ≤ (5/4)·mult/‖γ_ρ‖² ✓. And mult/(1+‖γ_ρ‖²) vs mult/‖γ_ρ‖²: comparable for ‖γ_ρ‖ ≥ 1. So Σ mult/|ρ|² converges by the chain: mult/|ρ|² ≤ mult/γ² ≤ (5/4)mult/‖γ_ρ‖² ≤ (5/4)·2·mult/(1+‖γ_ρ‖²) for ‖γ_ρ‖ ≥ 1 ✓. So summability of Σ_{‖γ_ρ‖≥1} mult/|ρ|² follows. And ‖γ_ρ‖ ≥ |γ| so the |ρ| ≥ 2n tail is covered. Good — the comparison works out (constants 5/2-ish). The Lean proof will need this chain — elementary but needs care.\n\nALTERNATIVELY — simpler: use `zero_sum_inv_sq` more directly: the family there is mult/(1+‖gammaOf ρ‖²) — REAL-valued. Our summand bound: |g(ρ)| ≤ 2n²·mult/|ρ|². Instead of comparing with |ρ|², compare with (1+‖γ_ρ‖²): need |g(ρ)| ≤ C·mult/(1+‖γ_ρ‖²): |g(ρ)| ≤ 2n² mult/|ρ|² and 1/(1+‖γ_ρ‖²) ≥ 1/(1+γ²+1/4) ≥ 1/((5/4)(1+γ²))·... and |ρ|² = σ²+γ² ≤ 1+γ²: so 1+‖γ_ρ‖² ≤ 5/4+γ² ≤ (5/4)(1+γ²)·... hmm 1+γ²+(1/2−σ)² ≤ 1+γ²+1/4 = (5/4)+γ² ≤ (5/4)(1+γ²)·(1)... (5/4)+γ² vs (5/4)(1+γ²) = 5/4 + (5/4)γ²: since γ² ≤ (5/4)γ²... yes (5/4)+γ² ≤ (5/4)+(5/4)γ² = (5/4)(1+γ²) ✓. So 1/(1+‖γ_ρ‖²) ≥ 1/((5/4)(1+γ²)) ≥ 1/((5/4)(1+γ²))·(|ρ|²/|ρ|²) ≥ |ρ|²... let me just: want |g| ≤ C·mult/(1+‖γ‖²): suffices 2n²/|ρ|² ≤ C/(1+‖γ‖²) ⟺ C ≥ 2n²(1+‖γ‖²)/|ρ|². (1+‖γ‖²)/|ρ|² = (1+γ²+(1/2−σ)²)/(σ²+γ²) ≤ (5/4+γ²)/γ² ≤ (5/4)/γ² + 1 ≤ 5/4 + 1 = 9/4 for γ² ≥ 1. So C = 2n²·9/4 = 4.5n² works for γ ≥ 1. And ‖γ_ρ‖ ≥ |γ| ≥ 1 means... our tail |ρ| ≥ 2n implies |γ| ≥ 2n−1 ≥ 1 for n ≥ 1 ✓. So:\n\n**|g(ρ)| ≤ (9/2)n²·mult/(1+‖γ_ρ‖²) for |ρ| ≥ 2n** — direct comparison with zero_sum_inv_sq's family. \n\nSo the summability proof: split subtype into {ρ : |ρ| < 2n} (finite — needs zero finiteness in a ball: `IsCompact.inter_riemannZetaZeros_finite` from Mathlib ZetaZeros, or Zeta23's zerosIn_finite... our subtype is IsNontrivialZero; the ball is compact; need {ρ nontrivial} ∩ ball finite — from `riemannZeta_zeros_locallyFinite` or the ZetaZeros compact-finiteness + strip containment... actually IsNontrivialZero ⊆ riemannZetaZeros and ball ∩ riemannZetaZeros finite by Mathlib's IsCompact.inter_riemannZetaZeros_finite ✓) and the tail (bounded by the summable family). Standard `Summable` glue: summable on finite set + summable norm-dominated tail.\n\nWait — actually simpler: `Summable` of g ⟸ `Summable` of ‖g‖ (absolute); use `Summable.of_norm_bounded` with the dominating family split: for the finite part use a constant function... hmm, `Summable.of_norm_bounded` needs the dominating function summable on the WHOLE index type. Define D(ρ) = (9/2)n²·mult/(1+‖γ_ρ‖²) for |ρ| ≥ 2n, and D(ρ) = ‖g(ρ)‖ for |ρ| < 2n. D differs from the summable family on a FINITE set ⟹ D summable (`Summable.congr_finite` or `summable_of_finite_support`... there's `Summable.congr` on finite set changes — `summable_of_finite_preimage`? The standard: if f = g on cofinite and one is summable... For subtypes: modify finitely many values — `Summable.congr_finite`? There is `Summable.of_norm_bounded` + finite-set modification lemma. Fine — engineering details at proof time.)\n\n3. After the def replacement + summability: the OLD `liCoeff` name is used in Sf, SfBoundProp, LiVerifiedUpTo, and in LiBasePoints.lean (final theorem). The def replacement keeps the name — downstream proofs recompile unchanged (they don't unfold liCoeff). Then rerun axiom audit + full build.\n\n4. Also the honesty note comment at liCoeff should be updated (the summability is now proved, not a note).\n\nOne more check — is there anything else that uses `liCoeff` numerically (e.g., E-023-related Lean)? No, liCoeff is only in the skeleton chain.\n\nAlso the OLD def's honesty note says \"it follows from Σ|ρ|⁻² < ∞ and |1−(1−1/ρ)ⁿ| = O(n/|ρ|)\" — that reasoning was WRONG (O(n/|ρ|) is not summable). The new comment should record the pairing reason.\n\nNow, about the conj-symmetry: the new def sums f ρ + f (star ρ) — do we need conj-invariance of the ZERO SET for the def? For the DEFINITION: no — it's just a sum over the subtype of a function (each term is fine whether or not ρ̄ is a zero). For CORRECTNESS (the def equals the classical λ_n): the pairing matters for convergence/correctness of the value, but as a definition it's self-consistent. The value equals Σ mult·Re f(ρ) — and classically λ_n = Σ mult·Re[1−(1−1/ρ)ⁿ] IS the correct value (each pair contributes 2Re f). So no conj-invariance lemma is needed even for correctness! The paired form is exactly \"Σ mult·Re f(ρ)\" — convergent and correct. (The conj-invariance would be needed only to relate the paired form to an upper-half-zeros enumeration.) EXCELLENT — the fix doesn't need the conj lemma at all.\n\nWait, one subtlety: does Σ mult·Re f(ρ) equal the classical λ_n? Classical: λ_n = Σ'_ρ [1−(1−1/ρ)ⁿ] with the sum understood as lim over T of symmetric truncation. The symmetric truncation Σ_{|γ|≤T} pairs ρ with ρ̄ automatically (the set {|γ|≤T} is conj-invariant). Pair contribution: mult·(f ρ + f ρ̄) = 2·mult·Re f(ρ). So the classical sum = Σ_upper mult·2Re f /... = Σ_all mult·Re f ✓ SAME. And our absolute summability of Re f (pair-cancelled form... wait — is Σ mult·|Re f(ρ)| convergent? |Re f(ρ)| ≤ 2n²/|ρ|² for |ρ| ≥ 2n — YES as shown. And the classical conditional sum equals the absolutely convergent Σ mult·Re f(ρ) by rearrangement (absolute convergence allows any rearrangement) ✓. So the def is correct AND summable. \n\nSo ii′-1a plan (concrete):\n1. Edit `liCoeff` in LiSkeleton.lean: new def + updated comment.\n2. Prove `liCoeff_summand_summable (n : ℕ) : Summable (fun ρ : {ρ // IsNontrivialZero ρ} => (zeroMult ρ : ℂ)/2 * (f ρ + f (star ρ)))` — actually define the def directly with the paired summand and prove its summability as a theorem.\n3. Rebuild package (lake build) — ensure LiSkeleton/LiBasePoints still compile.\n4. Rerun PrintAxioms on the key theorems + the full audit sweep (PrintAxiomsAll).\n5. Update D-064 (mark ii′-1a done), journal, STATE, NGUYEN checklist (ii′-1a checked), commit.\n\nFirst, the NGUYEN.md checklist. Then start the Lean work.\n\nLet me add the checklist to NGUYEN.md §5 as a new subsection after Phase 5's items (before §6 GRAVEYARD). Also fix: the §5 phase 5 header says \"⬜ PHASE 5\" — update? It's currently \"⬜ PHASE 5 — Verification & Write-up (Track D)\". Leave the icon.\n\nThe checklist:\n\n### 🔶 PHASE 5B — TIER ii′: close SfBoundProp (ACTIVE 2026-08-21; user directive — BEFORE submission; design D-064)\n- [x] ii′-0 Design + capability inventory → D-064 (session 014): two discoveries (liCoeff defect; crux Sf = Res₁ EXACT, tail-free assembly); routes R1–R5; all 8 planned Zeta23 dependencies axiom-checked live.\n- [ ] ii′-1a liCoeff pairing fix + summability\n- [ ] ii′-1b R1 residue machinery (finite-order residue + rectangle extension + w=1 Leibniz + zero residues)\n- [ ] ii′-2 R2(i)/(ii) elementary swaps (λ_n binomial; S_∞ binomial)\n- [ ] ii′-3 R2(iii) Lagarias (4.10) Laurent relation — EF-reuse (β2) first, Hadamard fallback (β1) [LONG POLE]\n- [ ] ii′-4 L3 zero-avoiding T + L1 kernel bounds\n- [ ] ii′-5 R3 R-bound via local route (Borel–Carathéodory/Jensen/Blaschke)\n- [ ] ii′-6 L0 sides identity + bridge + assemble |Sf| ≤ Bn\n- [ ] ii′-7 Close SfBoundProp + axiom audit + paper Appendix B/tag + archive closure\n\nWhere exactly? After 5.4 item, before \"## 6. GRAVEYARD\". Let me find the text.\n\nAlso — the freeze protocol note should be recorded in NGUYEN.md too (it's in STATE + session log; a line in the checklist header covers it).\n\nThen start ii′-1a. Let me look at the current liCoeff surroundings in LiSkeleton.lean once more (lines 32–55 read already) and make the edit.\n\nActually one more design decision for the new def: keep the name `liCoeff` and the exact downstream shape. Current: \n\ndef liCoeff (n : ℕ) : ℂ := tsum fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => (zeroMult ρ : ℂ) * (1 - (1 - 1 / (ρ : ℂ)) ^ n)\n\nNew:\n\ndef liCoeff (n : ℕ) : ℂ := tsum fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n  (zeroMult ρ : ℂ) / 2 * ((1 - (1 - 1 / (ρ : ℂ)) ^ n) + (1 - (1 - 1 / (star (ρ : ℂ))) ^ n))\n\nAnd prove theorem liCoeff_summable (n : ℕ) : Summable (fun ρ : {ρ // IsNontrivialZero ρ} => ...).\n\nHmm wait — actually, simpler and cleaner: define liCoeff via Re directly:\nsummand = (zeroMult ρ : ℂ) * ((1 - (1-1/ρ)^n + (1 - (1-1/ρ̄)^n))/2 — same thing. The /2 form is fine.\n\nActually, cleanest for proofs: `(zeroMult ρ : ℂ) * (((1 - (1 - 1/(ρ:ℂ))^n) + (1 - (1 - 1/(star ρ))^n))/2`. The star is on ℂ: star (ρ:ℂ). For ρ : subtype, (ρ : ℂ) coercion, star of that.\n\nSummability: ‖summand‖ = mult · |Re f(ρ)| — need to show the /2·(f+f̄) equals Re f: (f ρ + f ρ̄)/2 = (f ρ + conj(f ρ))/2 = Re(f ρ) — uses f(conj z) = conj(f z) for f(z) = 1−(1−1/z)ⁿ: conj is a ring hom (star_ring_end) and the expression is rational with real (integer) coefficients — `map_sub`, `map_one`, `map_div`, `map_pow`, `map_natCast`, `map_one`... provable by simp with star lemmas. Then (f + conj f)/2 = (Complex.re f : ℂ) via `Complex.add_conj` (z + conj z = 2·Re z). ✓\n\nSo ‖summand‖ = mult·|Re f(ρ)| — then bound |Re f(ρ)| as computed: Re f(ρ) = nσ/|ρ|² + Re((S−n)/ρ) — hmm, in Lean proving this specific bound |Re f(ρ)| ≤ 2n²/|ρ|² requires the expansion f(ρ) = S/ρ with S = Σ_{j<n} w^j... That's a real little analytic lemma: for w = 1−1/ρ, |ρ| ≥ 2n:\nf = 1 − wⁿ; Re f = Re(1 − wⁿ). \n1 − wⁿ = −(wⁿ − 1) = −(w−1)·Σ_{j<n} w^j = (1/ρ)·S.\nRe(1−wⁿ) = Re(S/ρ).\nWrite S = n + (S−n): Re(S/ρ) = n·Re(1/ρ) + Re((S−n)/ρ) = nσ/|ρ|² + Re((S−n)/ρ).\n|Re((S−n)/ρ)| ≤ |S−n|/|ρ| ≤ [n²/(2|ρ|)·e^{1/2}]/|ρ| ≤ n²/|ρ|² (e^{1/2}/2 ≤ 1).\nSo |Re f| ≤ n/|ρ|² + n²/|ρ|² ≤ 2n²/|ρ|² (n ≥ 1).\n\nIn Lean: |S − n|: S − n = Σ_{j<n} (w^j − 1); |w^j − 1| = |w−1|·|Σ_{i<j} w^i| ≤ |w−1|·j·M with M = max(1,|w|)^{n−1}... |Σ_{i<j} w^i| ≤ Σ |w|^i ≤ j·max(1,|w|)^j ≤ j·M ✓. So |S−n| ≤ |w−1|·M·Σ_{j<n} j = |w−1|·M·n(n−1)/2 ≤ (1/|ρ|)·M·n²/2. M = max(1,|w|)^{n−1} ≤ (1+1/|ρ|)^{n} ≤ (1+1/(2n))^n ≤ e^{1/2} ≤ 2 (for |ρ| ≥ 2n; |w| ≤ 1+1/|ρ| ✓). So |S−n| ≤ n²/|ρ|.\n\nThis is elementary but fiddly in Lean (geometric sums, pow bounds, (1+1/(2n))^n ≤ e^{1/2} — hmm, that needs exp estimation: (1+x)^n ≤ e^{nx} via `Real.add_one_le_exp` pow: (1+x)^n ≤ exp(nx) — there's `Real.pow_le_exp`? Something like (1 + x)^n ≤ Real.exp (n*x) for x ≥ 0: from add_one_le_exp: 1+x ≤ exp x, pow both sides (exp x)^n = exp(nx) via `Real.exp_nat_mul`... fine.)\n\nThen the comparison: Σ_tail mult·|Re f| ≤ 2n²·Σ_tail mult/|ρ|² ≤ 2n²·(9/2)·Σ mult/(1+‖γ_ρ‖²) < ∞.\n\nHmm — the comparison chain |ρ|² vs (1+‖γ_ρ‖²): 1+‖γ_ρ‖² = 1+γ²+(1/2−σ)² ≤ (5/4)(1+γ²)?? — showed (1+‖γ‖²)/|ρ|² ≤ 9/4 for γ ≥ 1. In Lean: need (1 + ‖gammaOf ρ‖²) ≤ (9/4)·|ρ|²·... wait direction: want mult/|ρ|² ≤ (9/4)·mult/(1+‖γ‖²) ⟺ (1+‖γ‖²) ≤ (9/4)|ρ|². Proof: 1+‖γ‖² = 1+γ²+(1/2−σ)² ≤ 1+γ²+1/4 = 5/4+γ² and (9/4)|ρ|² = (9/4)(σ²+γ²) ≥ (9/4)γ²... need 5/4+γ² ≤ (9/4)(σ²+γ²) ⟸ 5/4 + γ² ≤ (9/4)γ² ⟸ 5/4 ≤ (5/4)γ² ⟸ 1 ≤ γ² ✓ (for |γ| ≥ 1; and |ρ| ≥ 2n with σ ∈ (0,1) gives |γ| ≥ |ρ|−1 ≥ 2n−1 ≥ 1 ✓). ✓\n\nAnd zero_sum_inv_sq is stated for `(zetaZeros hs).carrier` with `hs : ZetaSeam` — the carrier subtype {ρ // ρ ∈ (zetaZeros hs).carrier} vs our {ρ // IsNontrivialZero ρ}: zetaZeros's carrier = setOf IsNontrivialZero presumably (SeamClosed: `zetaZeroConfig : ZeroConfig := zetaZeros zetaSeam`, and the simp lemmas relate zetaZeroConfig.N to Ncount...). There should be a definitional/propositional equivalence — `zetaZeros_carrier` simp lemma? The agent noted \"carrier = {ρ | IsNontrivialZero ρ}\". So the subtypes are definitionally the same type (up to the Set coercion) — `Summable` transport via `Equiv.subtypeEquivRight` or just rfl-ish. Engineering detail.\n\nAlso — `zero_sum_inv_sq` returns Summable of a REAL-valued family (zeroMult ρ : ℝ)/(1+normSq...). Our comparison needs ℝ-summability of the dominator D(ρ) = (9/2)n²·mult/(1+‖γ‖²) — that's `(zero_sum_inv_sq hs).mul_left ((9/2)*n^2)` ✓ (Summable.mul_left exists — used in the file itself).\n\nThen: Summable (fun ρ => ‖g ρ‖) via `Summable.of_norm_bounded`? That's for normed space values: `Summable.of_norm_bounded : Summable g → (∀ i, ‖f i‖ ≤ ‖g i‖) → Summable f`? The real lemma names: `Summable.of_norm_bounded (hg : Summable g) (h : ∀ i, ‖f i‖ ≤ g i)` requires g nonnegative-ish — actually `Summable.of_norm_bounded : (Summable g) → (∀ i, ‖f i‖ ≤ g i) → Summable f` in a normed ordered... For ℂ-valued f and ℝ-valued g: `Summable.of_norm_bounded (hg : Summable g) (h : ∀ i, ‖f i‖ ≤ g i) : Summable f` ✓ exists.\n\nThe finite-set modification: D(ρ) must dominate ‖g(ρ)‖ for ALL ρ, not just |ρ| ≥ 2n. For |ρ| < 2n: use a DIFFERENT bound — the finite set {ρ : |ρ| < 2n} is finite (needs proof: zeros in a ball). Simplest: dominate by D'(ρ) = D(ρ) + (indicator of the finite set)·‖g(ρ)‖... or: Summable on subtype ⟸ summable on {ρ : |ρ| ≥ 2n} part + finite part: use `summable_subtype_and_compl`? There is `Summable.of_norm_bounded` with D'(ρ) := if 2n ≤ |ρ| then (9/2)n²·mult/(1+‖γ‖²) else ‖g(ρ)‖: D' = D + (finitely many changes) — `Summable.congr_finite`? Hmm, actually there's a cleaner standard trick: `summable_of_summable_norm`-style. In Mathlib: `Summable.of_norm_bounded` where the dominating function is D', and `D'` summable because it differs from D on a finite set: `Summable.congr_finite (hs : Summable f) (h : ∀ i ∈ s, ...) ` — hmm the exact name... There's `Function.support` finite ⟹ summable trivially; D' = D + E where E has finite support (the modified values) — `Summable.add` with `summable_of_finite_support` (exists: `summable_of_finite_support : (support f).Finite → Summable f`). ✓ all pieces exist.\n\nAnd the zero finiteness in a ball: {ρ : {ρ // IsNontrivialZero ρ} | ‖(ρ:ℂ)‖ < 2n} — the ball is compact (closed ball), IsNontrivialZero ρ ⟹ riemannZeta ρ = 0 ⟹ ρ ∈ riemannZetaZeros; Mathlib: `IsCompact.inter_riemannZetaZeros_finite : IsCompact S → (S ∩ riemannZetaZeros).Finite` ✓ (agent confirmed). So the support of E is finite ✓.\n\nOK — the ii′-1a proof is fully sketched. Effort: maybe 150–300 lines of Lean. Let me start.\n\nActually — one more consideration: should the fix replace `liCoeff` or add a new def? Replace — but keep the name so downstream is untouched. The comment block above it gets rewritten to explain the pairing (and reference D-064 §1 + journal-014).\n\nAlso: `Sf n := SInfty n + 1 - (liCoeff n).re` — with the new real-valued summand, liCoeff n is real-valued (imag part 0) but its TYPE is still ℂ — .re still fine. Downstream untouched ✓.\n\nPlan for NGUYEN.md checklist first, then the Lean edit + build. Let me do the NGUYEN edit, then work on the Lean proof in Scratch.lean before merging (per the scratch workflow note).\n\nActually the workflow note says Scratch.lean is the scratchpad — but I just overwrote it with the axiom check. For ii′-1a I'll develop directly in Scratch.lean then merge into LiSkeleton.lean.\n\nLet me start. First NGUYEN.md checklist.","signature":""},{"type":"text","text":"Good call — let me document tier ii′ properly first, then start ii′-1a."},{"type":"tool_use","id":"Read_74","name":"Read","input":{"file_path":"D:\\Python\\Quantum\\NGUYEN.md","offset":401,"limit":45},"extra_content":null}]