D-062 — Tier (ii) design: SfBoundProp isolation, triage, and the perimeter decision

Date: 2026-08-20 | Session: 012 | Task: 5.1 tier (ii) steps 1–2 Status: step 1 COMPLETE (assembly proved in Lean); triage COMPLETE; step 2 (base-point discharge) PLAN VALIDATED (§5), execution queued. Origin: session-012-notes.txt (user-supplied design directive).

1. The assembly-first decision (notes step 1), executed

Per the notes' directive, tier (ii) was split before grinding: lambda_pos_finite_height is now PROVED in Lean (NguyenRH1, LiSkeleton.lean §4) from exactly five named hypotheses:

lambda_pos_finite_height
    (_hRH    : RHUpTo (3 * 10 ^ 12))          -- perimeter (Platt–Trudgian 2021)
    (hfinite : LiVerifiedUpTo (5 * 10 ^ 5))   -- perimeter (E-011/E-015 + Misguich–Voros)
    (hbase   : 0 < marginTilde FAlt 80000)                -- elementary evaluation
    (hbase2  : marginTilde FAlt 80000 < marginTilde FAlt 100000)  -- elementary
    (hSf     : SfBoundProp)                   -- ⭐ THE analytic obligation
    : ∀ n, 1 ≤ n → (n : ℝ) ≤ (3*10^12 − 1)^2 → 0 < (liCoeff n).re

PrintAxioms: [propext, Classical.choice, Quot.sound] — no sorryAx. The paper's claim is thereby upgraded to: R-004 is Lean-verified modulo one named analytic hypothesis (SfBoundProp), the declared computational perimeter, and two elementary evaluations of an explicit real function.

Design choices made during execution (each logged with rationale):

1. Sf definition. Sf n := SInfty n + 1 − (liCoeff n).re — the Bombieri–Lagarias Thm 2 identity λ_n = S_∞ − S_f + 1 holds by construction. No separate BL-Thm-2 formalization is needed downstream: the D-036 contour computation (Lagarias Thm 6.1 variant B) produces the identity AND the bound in one stroke, so SfBoundProp as stated is exactly what the contour argument proves directly.
2. FAlt majorant swap. The Lean margin uses FAlt(T) = (1/2π)T log T + 0.137 log T + 0.443 log log T + (7/8+1.588) — Trudgian's F(T) + S_b(T) with the negative-weight term −(log 2πe/2π)·T DROPPED. Rationale: ψ[F + S_b] crosses POSITIVE on [5.47, ~16] (negative weight × negative-ψ T-block), violating the marginTilde_convex hypothesis hψ; every FAlt block has provably negative ψ (D-057 rows #1/#3/#4 → FAlt_psi_neg). FAlt ≥ F + S_b pointwise for T ≥ 0, so the literature majorant property upgrades unchanged. Margin cost 2(log 2πe/2π)T ≈ 0.9√n — 256 at n = 8×10⁴ against margiñ = 15 764 (E-028-scale): negligible.
3. Two-point base (secant) instead of derivative base. pos_of_convex_of_two_points (ConvexOn.slope_mono_adjacent) replaces margiñ′(N₀) > 0: the remaining numeric obligations are two plain evaluations of the explicit margin function — no derivative machinery needed for the discharge. (pos_of_convex_of_base, the MVT + monotone-derivative variant, remains proved in the file.)
4. Regime split at n = 10⁵. Finite verification (perimeter, to 5×10⁵) covers n < 10⁵; the margin argument covers n ≥ 10⁵ via the two base points 8×10⁴ < 10⁵. SfBoundProp range: [10⁵, N₁]. (Convexity + two-point positivity does NOT give positivity between the points — convex functions can dip — hence the split at the second point, not the first.)

2. The isolated obligation

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

with Bn FAlt n the explicit D-037 (4.1) bound at A = 10.5, B₀ = 48 (D-056), Ĉ₀/Ĥ closed forms, M₀ = 1.3352, IIMaj, T = √n + 1.

3. Triage: what is inside SfBoundProp

Layer-by-layer decomposition of its eventual proof (D-036/D-037/D-056), with tractability verdicts:

4. The perimeter decision (deliberate, per the notes' instruction)

Decision: Trudgian 2014's explicit N(T)/S(T) bounds go INSIDE the trusted perimeter — the same class as Platt–Trudgian 2021 (which is already a named hypothesis RHUpTo) and zeta-23-lean's treatment of published inputs (hEF/hRvM). Rationale:

• Trudgian 2014 is refereed, published, with machine-checked constants; it is infrastructure, not part of this paper's contribution. Our contribution (R-004) is the ASSEMBLY — the S_∞ lower bound, the margin convexity, the bridge window, the traced R-bound — all of which are either already Lean-proved (tier (i)) or Mathlib-tractable (L1–L3).
• Formalizing Trudgian from scratch is Backlund–Rosser-class explicit zero-counting: plausibly a larger project than everything formalized so far combined (the notes' warning), with zero insight gained into R-004's actual content.
• Perimeters are honest when declared. The paper's Formal verification appendix now declares exactly: Platt–Trudgian (computational), Misguich–Voros/E-011/E-015 (computational), Trudgian 2014 (published explicit bounds), M₀ (interval-arithmetic certificate, after E-023b).

Consequence for the tag when L0–L3 are eventually discharged: R-004 would read [Lean-verified modulo published explicit N(T)/S(T) bounds (Trudgian 2014) + computational certificates (Platt–Trudgian RH-to-3×10¹²; Li verification to 5×10⁵; M₀ acb certificate)] — a fully honest, fully declared endpoint. No further shrinkage is meaningful without formalizing published infrastructure.

5. Step-2 discharge plan (base points) — VALIDATED NUMERICALLY

hbase and hbase2 reduce to rational interval bounds on log/exp/√ at n = 8×10⁴ and n = 10⁵. Certified constants and every link pre-verified (mpmath dps 40, session 012):

Primitives: e ∈ [2.7182818283, 2.7182818286] (Mathlib d9), π ∈ [3.1415926535, 3.1415926536] (d9), log 2 ∈ [0.6931471803, 0.6931471808] (d9); exp lower bounds by partial sums (Real.sum_le_exp_of_nonneg), exp upper bounds by exp x = (exp(x/16))¹⁶ ≤ (1/(1−x/16))⁻¹⁶ (from Real.add_one_le_exp at −x/16).

Verified links (bound, target, margin):

• e^11.263 ≤ 78056 < 80000 (2.4%) ⟹ log 80000 ≥ 11.263
• e^11.3 ≥ 80822 > 80000 (1.0%) ⟹ log 80000 ≤ 11.3
• e^11.5 ≤ 99507 < 100000 (0.5%) ⟹ log 100000 ≥ 11.5
• e^5.7 ≥ 298.9 > 286 (4.5%) ⟹ log T, log(T+2) ≤ 5.7 (n = 8×10⁴)
• e^5.8 ≥ 330.3 > 320 (3.2%) ⟹ log T, log(T+2) ≤ 5.8 (n = 10⁵)
• e^1.75 ≥ 5.755 > 5.7 (1.0%) ⟹ log log ≤ 1.75; e^1.77 ≥ 5.871 > 5.8 (1.2%) ⟹ log log ≤ 1.77
• e^5.6 ≤ 273.6 < 285 (4.0%) ⟹ log 285 ≥ 5.6 (lower-bound side at 8×10⁴)
• e^1.14 ≤ 3.1287 < π (0.41%) ⟹ log π ≥ 1.14; e^1.1448 ≥ 3.14182 > π (0.007% — tightest link; exact rational arithmetic, acceptable) ⟹ log π ≤ 1.1448
• e⁴ ∈ [54.5978, 54.6015] (exact pow of the d9 bounds)
• √80000 ≤ 283 (283² = 80089 ≥ 80000), √100000 ≤ 317 (317² = 100489)
• IIMaj ≤ 4.56(s+1)·2 via e^{−as}, e^{−bs} ≤ 1 (crude, slack absorbs)

Resulting certified values (computed with the certified constants):

• slower(8×10⁴) ≥ 336 998; Bn(8×10⁴) ≤ 327 038 ⟹ margin ≥ 9 960 > 0 ✓ (hbase)
• slower(10⁵) ≥ 433 098; Bn(10⁵) ≤ 346 878 ⟹ margin(10⁵) ≥ 86 220
• slower(8×10⁴) ≤ 338 671; Bn(8×10⁴) ≥ 274 683 ⟹ margin(8×10⁴) ≤ 63 989 < 86 220 ≤ margin(10⁵) ✓ (hbase2)

(True values: 15 764 and ~93 000 — the certified plan has ≥ 9 960 and ≥ 22 000 slack on the two comparisons respectively.) Estimated Lean effort: ~400–600 lines of interval grind following the block_range_bounds/iimaj_bracket_bound patterns.

EXECUTED 2026-08-20 (session 012, tier (ii) step 2). Discharged in full: NguyenRH1/LiBasePoints.lean (~560 lines), committed as fc2e55e. Execution notes vs the plan above: (i) the final certified targets were rounded outward for norm_num comfort — sInftyLower(8×10⁴) ∈ [336 000, 339 000], Bn(8×10⁴) ∈ [274 000, 328 000], sInftyLower(10⁵) ≥ 432 500, Bn(10⁵) ≤ 347 000 — giving the consumed bounds margin(8×10⁴) ≥ 8 001 (not the plan-stage 9 960) and margin(10⁵) ≥ 85 501 vs margin(8×10⁴) ≤ 65 001; (ii) log π ≤ 1.1448 was replaced by the comfortable log π ≤ 1.15 (e¹·¹⁵ ≥ 3.1582 > π, 0.5% margin), cost ~104 units, absorbed; (iii) 1/(2π) ≤ 1/6 used instead of 0.1592 (cost ~25); (iv) one real arithmetic slip caught by Lean: the Bn lower-bracket constant 110.34987 → 110.3498 ((2/3)·5.3248 = 3.549866… rounds DOWN) — exactly the kind of error the formalization exists to catch. Result: lambda_pos_finite_height_verified — R-004 machine-verified modulo SfBoundProp + the declared computational perimeter only. PrintAxioms: 3 standard axioms, no sorryAx.

Number-trail note (filed per the session-012-end-notes review): this §5 plan's dps-40 mpmath bound (> 9 960) and the Lean-certified bound (≥ 8 001) BOTH appear in the archive. The gap is expected and harmless: the Lean discharge deliberately rounds its interval targets outward (coarser than the dps-40 plan) for norm_num comfort — e.g. 336 000/328 000 instead of the plan's 336 998/327 038. Both bounds are comfortably positive and both suffice (the true value is 15 764). No two archive numbers disagree without a filed explanation; this is that explanation.

6. Roadmap after step 2