Session 023 — 2026-08-22 — ii′-5c (half): route revision + disc build to the Jensen count

Directive

Continue tier ii′-5 (the R-bound). User guidance endorsed the Davenport-disc machinery (g = ζ/∏(s−ρₖ)^mₖ, holomorphic log, Borel–Carathéodory) with the caveat "constants must survive the whole chain to 10.5 log(|t|+2) + 48" and a warning on multiplicity bookkeeping.

MAJOR FINDING: the BC constant obstruction (D-067 §6, committed 3a6ddc8)

Costing the disc route against the BAKED constants (marginTilde/Hhat in LiSkeleton have A = 10.5, B₀ = 48 as literals inside proved, frozen lemmas — marginTilde_convex, LiBasePoints): the disc's final log-coefficient is (M's log-coeff ~2.7) × (BC derivative factor 16R²/(R−r)³ = 100 at R = 5/2, r = 3/2) ≈ 270. Even the classically sharp 2R/(R−r)² = 5 gives ≈ 13.5; inf over R is 16. No disc-only constant reaches 10.5. Resolution (two-stage plan): the loose disc bound is the GROWTH INPUT for the partial-fraction identity (series converges via Zeta23's mult-weighted zero_sum_inv_sq; F := LHS−RHS entire by residue cancellation; |F| = o(R) on γ-gap circles ⟹ F constant); the tight A = 10.5, B₀ = 48 then comes from D-056's reference-point analysis OF THE IDENTITY. Loose disc constants never propagate. New sub-stages ii′-5e (identity) + ii′-5f (tight analysis); total ii′-5 estimate ~4 sessions.

ii′-5c build progress (LiDisc.lean, 2 commits: c3ebc30, 3760aab)

• zeroDiscFinset (zeros of ζ in closedBall(2+it, 5/2)) + zeroDisc_isNontrivial: every disc zero is nontrivial (re ≥ 1 via Mathlib riemannZeta_ne_zero_of_one_le_re — the PNT-level input is in Mathlib; re ≤ 0 via the ΓR-pole/FE argument + riemannZeta_zero = −1/2).
• scaledZeta (the unit-disc scaling F(w) = ζ(s₀+(5/2)w)/ζ(s₀)), scaledZeta_zero (F(0) = 1) — the center lower bound came FREE from Zeta23's RvM.zeta_lower_bound_two (‖ζ(2+it)‖ ≥ 1/3), eliminating the μ-series build entirely; scaledZeta_analytic.
• Multiplicity bookkeeping chain (the user-flagged point): analyticOrderNatAt_riemannZeta_affine (order invariance under the affine map, via the local-factorization pullback through EventuallyEq.comp_tendsto + analyticOrderAt_eq_natCast), analyticOrderNatAt_const_mul (nonzero constant factor), analyticOrderNatAt_scaledZeta.
• scaledZeta_zeros_finite (affine preimage of the discrete zero set).
• scaledZeta_jensen_count: mult-weighted count ≤ log((9/4)|t|²)/log(33/32) via Zeta23's ZerosBound (Jensen) with B = (9/4)|t|² (the ii′-5b disc bound ‖ζ‖ ≤ (3/4)|t|² over ‖ζ(s₀)‖ ≥ 1/3).

Banked gotchas (session 023 additions)

• analyticOrderNatAt f z₀ = (analyticOrderAt f z₀).toNat by DEF — the ⊤ case of order lemmas is just toNat-top (= 0), no cast lemma needed there.
• EventuallyEq.congr'/EventuallyEq.symm fail as DOT notation when the hypothesis displays in the unfolded filter form — use the full Filter.EventuallyEq.xxx term form (same gotcha as 021's hEv.symm).
• AnalyticAt.comp_of_eq hf hg rfl — the beta-reduced-point fix from journal-019/020 confirmed working (used twice).
• Nat.cast_analyticOrderNatAt (hf : analyticOrderAt f z₀ ≠ ⊤): ↑(analyticOrderNatAt) = analyticOrderAt — the order-cast bridge.
• Set.Finite.preimage (hfin) (InjOn-proof) for the affine-preimage finiteness.
• Set.mem_setOf_eq is deprecated → Set.mem_ofPred_eq (or just use .1/.2 on the membership directly).

Status / next

ii′-5c half done. Remaining 5c: the R-gap selection (scaled midpoint pigeonhole over the zero-distance values, count from Jensen), then g := ζ/∏(s−ρₖ)^mₖ analytic + nonvanishing on the closed disc, then outer-circle |g| bound + LogOfAnalyticFunction + BorelCaratheodoryDeriv

• the R-sum split ⟹ the LOOSE R-bound ‖logDeriv ζ s − Σ_near m/(s−ρ)‖ ≤ C·(log|t|)² on σ ∈ [1/2, 7/2], |t| ≥ 10. Then 5d (FE-reflection), 5e (identity via growth), 5f (tight analysis → 10.5/48).