D-071 — Tier ii′ sub-stage ii′-6 design: the L0 assembly + the honest-Bn correction

Date: 2026-08-24 | Session: 038 (ii′-6-0) | Task: 5.1 tier ii′ sub-stage 6 (design) Status: design COMPLETE — findings F-A/F-B/F-C documented, user approvals recorded, sub-stage map ii′-6-a..e decided. Numerical validation: E-030 (ALL CHECKS PASS).

0. What ii′-6 must prove

SfBoundProp : ∀ n : ℕ, 10⁵ ≤ n → (n : ℝ) ≤ (3·10¹² − 1)² → |Sf n| ≤ Bn FAlt n

The chain (D-064 §5, all inputs now in hand): the crux sf_eq_resW1 (ii′-3c) turns Sf into ResW1; rectInt'_Jlag (ii′-1b) on the D-036 variant-B rectangle (σ₀ = −5/2, σ₁ = 2√n, im = ±T, T zero-avoiding in [√n, √n+1]) gives ResW1 = RectInt − λ_n(T) − triv(−2); the four sides are bounded by the L1 kernel bounds (ii′-4) + the tight R-bound (ii′-5f) + M₀; the bridge bounds |λ_n(T)| via RHUpTo + the global Trudgian count.

1. THREE FINDINGS (this session; the fold analysis)

F-A: the bridge factor-2 (paper erratum, R-004 unaffected)

The residue sum λ_n(T) = Σ_{ρ ∈ Sz} mult·(1−(ρ/(ρ−1))ⁿ) runs over zeros with |γ| ≤ T — BOTH signs. On the line (RHUpTo), |ρ/(ρ−1)| = 1, so each term ≤ 2·mult, giving the honest bound

|λ_n(T)| ≤ 2·(mult-weighted both-signs count) ≤ 4·FAlt(T),

since the mult-weighted one-sign count ≤ FAlt(T) (Trudgian N(T) ≤ F + S_b upgraded to FAlt, LiSkeleton:2396). D-036 §4 / D-037 (4.1) / E-023's B_bound charge 2·FAlt (their N(T) is the one-sign count but the sum is both-signs) — a factor-2 accounting slip inherited into Bn's 2 * F T term. Impact: +2F ≈ +589 at n = 10⁵ (0.17% of Bn), ≈ +2.8×10¹³ at N₁ vs margin(N₁) = 2.458×10²⁶ — R-004's theorem is unaffected; the Lean assembly must charge 4F; the paper gets an explicit correction note at ii′-7 (user protocol step 7).

F-B: I_III's near-sum needs the two-unit count (D-069 Finding 2 confirmed)

On the left vertical σ₀ = −5/2 every zero is at distance ≥ 3/2, so the near sum ≤ (2/3)·(near count) — but the near window |γ−t| < 1 is a TWO-unit window, honestly counted by Z2(t) = 0.6·log(t+2) + 0.886·log log(t+2) + 2.7 (ZeroCountProp2), not by Ĉ₀(t) = 0.433·log(t+2) + 0.886·log log(t+2) + 2.9. Bn's baked (2/3) * C0hat T undercounts by (2/3)(Z2 − Ĉ₀) ≈ (2/3)(0.167·log T − 0.2). This is the D-069 Finding-2 "(4/3)-ish" correction made exact.

F-C: the baked Bn is unprovable beyond n ≈ 5×10⁷ (E-030 V1)

The two killers (F-A's +2F, F-B's +(2/3)(Z2−Ĉ₀)·4T) grow like T·log T and eventually outgrow the horizontal slack (which grows like (log T)²): the honest assembly / baked Bn ratio is 0.656 at 10⁵, 0.980 at 10⁸, 1.012 at 10¹², 1.015 at N₁. With the baked Bn the fold FAILS asymptotically — SfBoundProp as baked is true but not provable via the contour assembly.

Resolution (user-approved, session 038): redefine Bn to the honest form — bridge 2F → 4F, I_III (2/3)Ĉ₀ → (2/3)Z2 — a freeze-protocol exception approved by the user with the 8-step protocol of §5. The fold then works on all of [10⁵, N₁] (E-030 V4), the margin stays positive everywhere (V2: margin with corrected Bn > 0 on the grid, and LARGER than the baked margin near 10⁵ — the corrected Bn is smaller there), and the horizontal segment-integral fits under its baked share by 2.5–4× everywhere (V3: ratio 0.24–0.40).

2. The corrected Bn (user protocol step 1)

Bn(F, n) := 4·F(T) + 4T[(2/3)·Z2(T) + 10.5·log(T+2) + 48] + 40·1.3352
          + 2(e⁴+1)·[7·Ĥ(T) + 3.3] + IIMaj(n) + 1,   T = √n + 1

with the NEW Z2hat t := 0.6·log(t+2) + 0.886·log log(t+2) + 2.7 (the ZeroCountProp2 bound form, named for use in Bn; ZeroCountProp2's statement is untouched — its consumers (5f) are unaffected; Z2hat is definitionally the same closed form). Ĥ, IIMaj, C0hat unchanged. The identifier Bn is retained with an explicit correction comment (user protocol step 2) pointing here and to E-030; the old form is preserved in git history + the audit trail (step 8).

Per-piece fold (the assembly proves these, then sums): | piece | Lean charge | Bn share | fit | |---|---|---|---| | bridge | 4·FAlt T | 4·F T | identity | | I_III long | 4T[(2/3)Z2 + 10.5 log + 48] | same | identity | | I_III short | 40·M₀ | 40·1.3352 | identity | | horizontals | 2(e⁴+1)·[NI + 5.5(10.5 log + 48) + 3.3] | 2(e⁴+1)[7Ĥ+3.3] | V3: ≤ 0.40 | | I_I | IIMaj n | IIMaj n | identity | | triv | ≤ 1 | +1 | identity |

NI(T) := Z2(T)·2·log(16.5/c), c = 1/(9·C0hat(√n+3)) the extended pigeonhole clearance (§4.3).

3. Perimeter additions (user-approved session 038; D-062 §4 classes)

• ZeroCountGlobalProp : ∀ T : ℝ, 2 ≤ T → (mult-weighted one-sign count of nontrivial zeros with 0 < γ ≤ T : ℝ) ≤ FAlt T. The global Trudgian N(T) form (the same declared source as ZeroCountProp, which is its unit-window corollary; the unit form does NOT imply the global form at the FAlt level — summing windows gives 0.433·T·log T > 0.159·T·log T). Used by the bridge.
• MZeroProp : ∀ t : ℝ, |t| ≤ 10 → ‖logDeriv riemannZeta (-5/2 + t·I)‖ ≤ 1.3352. The M₀ = 1.3352 interval-certificate (E-023 grid + sampled-Lipschitz ×2; the D-062 §4 L6 entry, E-023b acb upgrade optional). Used by I_III's short piece.

4. Component designs (the five pieces)

4.1 The sides identity

rectInt'_Jlag on the rectangle z = −5/2 − iT, w = 2√n + iT:

• 1 interior: re 1 ∈ (−5/2, 2√n) ✓, im 0 ∈ (−T, T) ✓.
• ζ ≠ 0 on the border: horizontals via the zero-avoiding T (im = ±T, and trivial zeros have im = 0); left vertical σ = −5/2 via the zero classification (zeros = nontrivial ∪ {0} ∪ {−2n}: none at re = −5/2); right vertical σ = 2√n ≥ 2 via re > 1 nonvanishing.
• Sz = {nontrivial zeros with |γ| ≤ T} ∪ {−2} (zeroMult(−2) = 1, ii′-4); ζ(0) = −1/2 ≠ 0. ⟹ ResW1 n = RectInt − Σ_{Sz} mult·(1−(ρ/(ρ−1))ⁿ), and |Sf n| = |(ResW1 n).re| ≤ ‖ResW1 n‖ ≤ ‖RectInt‖ + |λ_n(T)| + |triv|. RectangleIntegral' is (2πi)⁻¹-normalized: ‖RectInt‖ ≤ (Σ side integrals)/(2π) ≤ Σ side integrals — Bn charges the raw side bounds (the paper's convention; the 2π factor is spare slack).

4.2 The bridge (uses hRH + ZeroCountGlobalProp)

T = √n + 1 ≤ 3×10¹² (from n ≤ N₁ = (3×10¹²−1)²): every zero in Sz is on the line (hRH) ⟹ |ρ/(ρ−1)| = 1 (|ρ|² = |1−ρ|² at re = 1/2) ⟹ |1−(ρ/(ρ−1))ⁿ| ≤ 2·mult. Count: both-signs = 2·(one-sign) ≤ 2·FAlt(T) (conj symmetry, no real zeros). ⟹ |λ_n(T)| ≤ 2·mult·count ≤ 4·FAlt(T). (The conj-pairing |2 − wⁿ − w⁻ⁿ| ≤ 4 gives the same constant — recorded as the alternative accounting; no improvement possible: nθ can be extremal.)

4.3 The extended pigeonhole (Finding-2 repair)

exists_zero_avoiding_T_wide: T ∈ [a, a+1] with clearance c = 1/(9·C0hat(a+2)) against ALL zeros with im ∈ (a−1, a+2) (3-unit window count ≤ 3·C0hat(a+2) from ZeroCountProp applied to the three unit sub-windows — NO new perimeter needed; the midpoint-pigeonhole machinery of exists_zero_avoiding_T cloned at 3× count, a ≥ 3 so a−1 ≥ 2 ✓; √n ≥ 316 ≫ 3 ✓).

4.4 The four sides

• I_III (left vertical σ = −5/2, length 2T): kernel ≤ 2 (kFun_norm_le_two ✓). For |t| ≥ 10: tight R-bound (5f capstone, σ ∈ [−5/2, 3] ✓) + near sum ≤ (2/3)·Z2 (|w−ρ| ≥ 3/2 since re ρ ≤ 1). For |t| ≤ 10: MZeroProp ⟹ |ζ′/ζ| ≤ 1.3352, segment length 20, kernel ≤ 2 ⟹ ≤ 40·1.3352.
• I_II/I_IV (horizontals, the crux): kernel ≤ e⁴+1 on [−3, 3] (kFun_shift_norm_le_exp_four_add_one ✓). Tight R-bound at height T (T ≥ √10⁵ ≥ 316 ≥ 10 ✓). The near-sum INTEGRAL (NOT the max×length — this is what makes the fold fit): with w = x + iT, x ∈ [−5/2, 3], ρ = β + iγ, δ = |T−γ| ≥ c (extended pigeonhole): ∫{-5/2}^{3} dx/|w−ρ| ≤ asinh((3−β)/δ) + asinh((β+5/2)/δ) ≤ 2·asinh(5.5/δ) ≤ 2·log(16.5/c), so Σ{near} mult·∫ ≤ Z2(T)·2·log(16.5/c) =: NI(T). The R-part integrates to 5.5·(10.5·log(T+2) + 48). The right tail [3, 2√n]: Dirichlet stepping (|ζ′/ζ(σ+iT)| ≤ 2^{−(σ−2)}·dirichletC2 via the LSeries vonMangoldt form; geometric sum ≤ e·dirichletC2·2 ≤ 3.3 with the kernel stepping kFun_shift_norm_le_exp_sqrt_half_add_one — the (6.12) argument). Total per horizontal: (e⁴+1)·[NI + 5.5·(10.5 log + 48) + 3.3]; E-030 V3 certifies NI + 5.5·(10.5 log + 48) + 3.3 ≤ 0.40·(7Ĥ + 3.3) on the grid (and the formal fold needs only ≤ 7Ĥ + 3.3 — the Ĉ₀² term dwarfs everything: NI ~ 1.2·L·log L vs 21Ĉ₀² ~ 3.94·L²).
• I_I (right vertical σ₁ = 2√n): |ζ′/ζ| ≤ 2^{−(σ₁−2)}·dirichletC2 (Dirichlet stepping) ≤ 2^{−(2√n−2)}·0.57; kernel ≤ e^{√n/2}+1 (kFun_shift_norm_le_exp_sqrt_half_add_one ✓); length 2T ⟹ ≤ IIMaj n.
• triv(−2): term = mult·(1−((−2)/(−3))ⁿ) = 1 − (2/3)ⁿ ≤ 1 (zeroMult_neg_two = 1 ✓; |2/3|ⁿ ≤ 1).

4.5 The fold

|Sf n| ≤ ‖RectInt‖ + |λ_n(T)| + |triv| ≤ [NI + 5.5(10.5 log + 48) + 3.3]·2(e⁴+1)/(2π)·... — NO: Bn charges the raw side bounds (the paper's convention; RectangleIntegral' is 2π-normalized so ‖RectInt‖ ≤ Σ sides/(2π) ≤ Σ sides ✓ the fold is immediate per-piece). The per-piece fits of §2 give |Sf n| ≤ Bn FAlt n on [10⁵, N₁] — the only real-analytic comparison needed is the horizontal share NI + 5.5·(10.5 log + 48) + 3.3 ≤ 7Ĥ + 3.3, an explicit inequality in L = log T, LL = log log T for L ≥ log(√10⁵+1) (the pinch-lemma pattern from 5f-iii: certified endpoint evaluation + growth-direction argument; E-030 V3 is the numeric witness: ratio 0.398 → 0.241 decreasing).

5. The user-approved 8-step protocol (session 038, verbatim decision)

1. Change Bn to the honest expression: 2F → 4F, (2/3)Ĉ₀ → (2/3)Z2.
2. Fresh explicitly-documented corrected definition (identifier Bn retained, correction comment + pointer here).
3. Re-run the structural convexity proof (marginTilde_convex — prove again, don't assume survival).
4. Re-certify both base points with rational interval arithmetic (margiñ(8×10⁴), margiñ(10⁵) — values IMPROVE: the corrected Bn is smaller there).
5. Re-run the endpoint margin calculations.
6. Complete ii′-6 against the corrected Bn.
7. At ii′-7: Paper A correction note (both-signs factor + I_III two-unit count).
8. Preserve the old results in the audit history (git history + E-030 + this document + the journal).

6. Sub-stage map

7. Affected declarations of the Bn redefinition (mapped, session 038)

• Bn (LiSkeleton:2413), marginTilde (754 — the duplicated expression, lockstep), marginExpanded + the mK constant (1819 — the I_III constant block changes (2/3)·2.9 → (2/3)·2.7 and the F-block doubles), marginTilde_eq_expanded (bookkeeping re-run), marginTilde_convex (ψ-table: the 4F block scales ×2 — still negative; the I_III (2/3)Z2 block — same log/loglog form as the (2/3)Ĉ₀ block — re-prove the two changed rows), marginTilde_eq_sub (bookkeeping re-run).
• LiBasePoints: marginTilde_FAlt_80000_pos, marginTilde_FAlt_80000_lt_100000 — re-certify with rational interval arithmetic (same machinery; the values grow by the baked−corrected difference ≈ 1.2×10³ at 8×10⁴ / 1.24×10³ at 10⁵).
• lambda_pos_finite_height_verified — statement Bn-independent (0 < (liCoeff n).re); proof re-checks against the changed pieces.

8. Risks

• The convexity re-proof's changed rows may need new psi-arguments if the Z2 block's ψ ≠ the Ĉ₀ block's ψ shape (both are α·log(T+2)+β·log log(T+2)+const with α > 0, β ≥ 0 — D-057's rows cover this form structurally; expected mechanical).
• The horizontal segment-integral's asinh/log elementary bounds are the usual certified-numerics grind (LiTightR piece-3-class; budgeted).
• The bridge's both-signs count uses conj symmetry of the zero set (isNontrivialZero_conj ✓ in hand) — mechanical.