Session 015 — 2026-08-21 — Tier ii′ sub-stage ii′-1a COMPLETE

Directive

Continue tier ii′ per D-064: sub-stage ii′-1a — the liCoeff pairing fix + summability proof. (Pre-work: Phase 5B checklist added to NGUYEN.md per user request, commit 7a395b2.)

Work done — ii′-1a COMPLETE (liCoeff defect repaired)

1. Defect confirmed and fixed (D-064 §1): the old liCoeff was an unordered tsum of a non-summable family (summand ~ n/|γ|, Σ mult/|ρ| = ∞ by RvM) ⟹ junk value 0; LiVerifiedUpTo/SfBoundProp were FALSE as encoded. Replaced by the paired symmetric form liSummand n ρ = (mult/2)·(f ρ + f ρ̄), f ρ = 1−(1−1/ρ)ⁿ — the classical Bombieri–Lagarias convention; manifestly real (liSummand_eq: summand = mult·(Re f ρ : ℂ)).
2. Summability PROVED (liSummable, LiSkeleton.lean §1b): - re_li_summand_le: |Re f(ρ)| ≤ 2n²/‖ρ‖² for ‖ρ‖ ≥ 2n (n ≥ 1) — geometric-sum identity 1−wⁿ = (1/z)·Σw^j, kernel bound (1+1/(2n))ⁿ ≤ 2 (pow_one_add_inv_two_mul_le via exp). - normSq_gammaOf_le_mul_norm_sq: 1+‖γ_ρ‖² ≤ (9/4)‖ρ‖² on the tail. - liSummand_norm_le: ‖liSummand‖ ≤ (9/2)n²·mult/(1+‖γ_ρ‖²) tail. - Assembly: Zeta23's PROVED WeilEF.zero_sum_inv_sq (Σ mult/(1+‖γ‖²) < ∞, 3 standard axioms — live-checked session 014) dominates the tail; the ball {‖ρ‖ < 2n} is finite via Mathlib IsCompact.inter_riemannZetaZeros_finite; dominator + finite support modification + Summable.of_norm_bounded.
3. Package rebuild GREEN (8741 jobs): LiSkeleton + LiBasePoints + NguyenRH1 all compile; downstream uses of liCoeff (Sf, SfBoundProp, LiVerifiedUpTo, lambda_pos_finite_height(_verified)) needed zero changes (liCoeff used abstractly) — they are now TRUE statements rather than vacuous ones.
4. Axiom audit: all 7 new declarations + lambda_pos_finite_height, lambda_pos_finite_height_verified, sInfty_lower_bound, marginTilde_convex — 3 standard axioms ONLY, no sorryAx. (sorryAx remains only on the 5 intended skeletons.)

New Lean code (~340 lines in LiSkeleton.lean §1)

liSummand, summand_conj, liSummand_eq, pow_one_add_inv_two_mul_le, re_li_summand_le, normSq_gammaOf_le_mul_norm_sq, liSummand_norm, liSummand_norm_le, liSummable. Imports added: Zeta23.WeilEF.ZeroSummability, Zeta23.Statement.SeamClosed.

Notes for future sessions (hard-won this session)

• conj notation is scope-locked (ComplexConjugate); use starRingEnd ℂ directly — map_sub/map_one/map_pow/map_div₀ apply.
• Complex.add_conj : z + starRingEnd ℂ z = ((2*z.re : ℝ):ℂ).
• mul_geom_sum : (x−1)·Σx^i = x^n − 1 (the needed direction).
• Complex.normSq_eq_norm_sq : normSq z = ‖z‖²; Complex.inv_re.
• div_le_iff₀ / le_div_iff₀ / abs_add_le / pow_le_pow_left₀ / pow_le_pow_right₀ (1 ≤ a form) — current Mathlib names.
• Nat-literal trap: write (n : ℝ) explicitly in mixed ℕ/ℝ bounds or the whole expression elaborates in ℕ (1/(2n) = 0!).
• rw [hS] with S := set-variable rewrites occurrences inside its own RHS replacement — use nth_rewrite 1 to hit only the outer one.
• summable_of_hasFiniteSupport (not summable_of_finite_support, deprecated); Set.Finite.of_finite_image; Subtype.val_injective.injOn.
• zero_sum_inv_sq's subtype (zetaZeros zetaSeam).carrier is DEFEQ {ρ // IsNontrivialZero ρ} (zetaZeroConfig_carrier rfl) — exact works.

State at stop

ii′-1a COMPLETE. The liCoeff encoding defect is repaired: the R-004 Lean chain is now meaningful (hypotheses are true statements), not vacuous. Paper A untouched (freeze intact). Next: ii′-1b (residue machinery R1) — general finite-order residue + rectangle theorem extension + w=1 Leibniz residue + zero residues.