Session 014 — 2026-08-21 — Tier ii′ launched: design + two discoveries

Directive

User chose option (a): do tier ii′ (close SfBoundProp in Lean) BEFORE submission, with Paper A frozen and submittable at all times. Freeze protocol in force: no edits to paperA.tex/paperB.tex/draft.tex/ references.bib until ii′-7; no edits to existing Lean proofs except the liCoeff correctness fix (below, flagged); commit at every sub-stage.

Work done (sub-stage ii′-0: design → D-064)

1. Baseline verified clean (git: only untracked LaTeX artifacts).
2. Two parallel inventory agents surveyed: (i) vendored residue/ meromorphic API; (ii) Zeta23 zero infrastructure + NguyenRH1 defs + Mathlib zeta/digamma/Jensen/Borel–Carathéodory surface.
3. Read liCoeff/Sf/perimeter defs, D-036, D-056, D-037 (full), and the primary source (Lagarias math/0404394 §4–6, archived PDF).
4. Axiom-checked all planned Zeta23 dependencies LIVE: zero_sum_inv_sq, zeta_local_zero_count, zeta_reflect_zero, zeta_mult_reflect, RectangleIntegral'_eq_sumResiduesIn, ResidueMult, logDerivResidue, riemannZetaLogDerivResidue — ALL 3 standard axioms only.
5. Settled the exact identity chain NUMERICALLY (dps 40–50, mpmath + E-021 zero cache; see D-064 §3 table).
6. Wrote D-064 (design doc: discoveries, routes R1–R5, lemma graph, revised sub-stage map ii′-1a..7). Registered in index.md + db.

DISCOVERY 1 — liCoeff encoding defect (correctness, not cosmetic)

liCoeff (LiSkeleton.lean:39) is an unordered tsum whose family is NOT Summable for any n ≥ 1 (summand ~ n/|γ|, Σ mult/|ρ| = ∞ by RvM). Therefore liCoeff n = 0 (junk), making LiVerifiedUpTo FALSE and SfBoundProp FALSE as encoded (at n = 10⁵: |Sf| ≥ 432 501 > 347 000 ≥ Bn by the certified LiBasePoints bounds). The session-012 theorems are vacuously true; the session-013 audit could not see this (it checks axioms, not hypothesis truth). Paper A's mathematics is unaffected — pure encoding defect. FIX DESIGNED (D-064 §1): paired symmetric form (manifestly real, absolutely summable via pair bound |pair| ≤ C(n)·mult/|ρ|² + Zeta23's proved zero_sum_inv_sq). Scheduled as sub-stage ii′-1a (first executable item).

DISCOVERY 2 — the crux identity is Sf = Res₁ EXACTLY

The D-036/D-037 bookkeeping, settled against Lagarias's paper and verified numerically:

• Sf(n) := S_∞(n) + 1 − λ_n = Res₁(n) = Σ_{j=1}^n C(n,j)·c_{j−1} (c_k = Laurent coefficients of −ζ′/ζ at 1). Follows from Lagarias (4.10) [τ_j = η_j + (−1)ʲσ_{j+1} − (−1)ʲδ] summed binomially. Verified: (4.10) at j=0 exact to 15 digits (λ₁ = 0.02309570896612103); crux consequence λ₂ = 0.09234573523 matches E-015's certified 0.09234573522804667 exactly.
• Residue theorem: sides(T) = λ_n(T) + triv + Res₁(n), verified to 2e-21 (n=2) by direct contour integration.
• Assembly is TAIL-FREE: |Sf| ≤ |λ_n(T)| + |sides| + |triv| ≤ 2N(T) + [side pieces] + 1 = B(n) — no tail term anywhere (the crux absorbs it). This is why D-037's B(n) has none.
• The w=1 pole (order n+1) residue computation reduces to a Leibniz rule: (w−1)^{n+1}J = [wⁿ − (w−1)ⁿ]h(w), h = (w−1)(−ζ′/ζ) analytic — Res = Σ_j C(n,j)c_{j−1} confirmed algebraically.
• SIDE EFFECT: D-037's line-63 compressed identity needs an erratum pointer to D-064 (correct reading: Sf = Res₁ = sides − λ_n(T) − triv).

Inventory highlights (why tier ii′ is feasible)

• Rectangle residue theorem EXISTS (vendored FromPNTPlus RectangleIntegral'_eq_sumResiduesIn, axiom-clean) — needs the simple-pole scaffold extended to finite order (bounded, R1).
• logDerivResidue, ResidueMult, riemannZetaLogDerivResidue vendored and clean.
• Mathlib HAS Borel–Carathéodory, Jensen's formula, digamma, HadamardThreeLines, MeromorphicAt/Order/NormalForm/FactorizedRational.
• Zeta23 HAS proved Σ mult/(1+‖γ_ρ‖²) < ∞ (zero_sum_inv_sq), local zero count, RvM, reflect/conj symmetry, window finiteness.
• Mathlib has NO Weierstrass/Hadamard factorization; FromPNTPlus StrongPNTPrefix has the local Blaschke/Borel toolkit.

Route decisions (D-064 §4)

R1 build higher-order residue machinery (1–2 sess); R2 crux via (4.10) — investigate zeta-23 EF reuse (β2) first, Hadamard fallback (β1) (2–4 sess, the long pole); R3 R-bound via LOCAL route (Borel–Carathéodory/Jensen/Blaschke — machinery exists) (2–3 sess); R4 the old "w=1 ↔ S_∞" monster is KILLED by Discovery 2 (factors into R1's Leibniz computation + R2's (4.10)); R5 perimeter unchanged.

State at stop

D-064 complete; sub-stage map ii′-1a..7 (total ~9–16 sessions). NEXT: ii′-1a (liCoeff pairing fix + summability). Paper A untouched (compiles at session-013 state; submission-ready fallback intact — D-064 §8).