{
  "file_path": "D:\\Python\\Quantum\\research\\derivations\\D-062-SfBound-triage.md",
  "content": "# D-062 \u2014 Tier (ii) design: SfBoundProp isolation, triage, and the perimeter decision\nDate: 2026-08-20 | Session: 012 | Task: 5.1 tier (ii) steps 1\u20132\nStatus: step 1 COMPLETE (assembly proved in Lean); triage COMPLETE;\nstep 2 (base-point discharge) PLAN VALIDATED (\u00a75), execution queued.\nOrigin: session-012-notes.txt (user-supplied design directive).\n\n## 1. The assembly-first decision (notes step 1), executed\n\nPer the notes' directive, tier (ii) was split before grinding:\n`lambda_pos_finite_height` is now PROVED in Lean (NguyenRH1,\nLiSkeleton.lean \u00a74) from exactly five named hypotheses:\n\n```\nlambda_pos_finite_height\n    (_hRH    : RHUpTo (3 * 10 ^ 12))          -- perimeter (Platt\u2013Trudgian 2021)\n    (hfinite : LiVerifiedUpTo (5 * 10 ^ 5))   -- perimeter (E-011/E-015 + Misguich\u2013Voros)\n    (hbase   : 0 < marginTilde FAlt 80000)                -- elementary evaluation\n    (hbase2  : marginTilde FAlt 80000 < marginTilde FAlt 100000)  -- elementary\n    (hSf     : SfBoundProp)                   -- \u2b50 THE analytic obligation\n    : \u2200 n, 1 \u2264 n \u2192 (n : \u211d) \u2264 (3*10^12 \u2212 1)^2 \u2192 0 < (liCoeff n).re\n```\n\nPrintAxioms: `[propext, Classical.choice, Quot.sound]` \u2014 no `sorryAx`.\nThe paper's claim is thereby upgraded to: **R-004 is Lean-verified modulo\none named analytic hypothesis (SfBoundProp), the declared computational\nperimeter, and two elementary evaluations of an explicit real function.**\n\nDesign choices made during execution (each logged with rationale):\n\n1. **Sf definition.** `Sf n := SInfty n + 1 \u2212 (liCoeff n).re` \u2014 the\n   Bombieri\u2013Lagarias Thm 2 identity \u03bb_n = S_\u221e \u2212 S_f + 1 holds by\n   construction. No separate BL-Thm-2 formalization is needed downstream:\n   the D-036 contour computation (Lagarias Thm 6.1 variant B) produces the\n   identity AND the bound in one stroke, so `SfBoundProp` as stated is\n   exactly what the contour argument proves directly.\n2. **FAlt majorant swap.** The Lean margin uses\n   `FAlt(T) = (1/2\u03c0)T log T + 0.137 log T + 0.443 log log T + (7/8+1.588)`\n   \u2014 Trudgian's F(T) + S_b(T) with the negative-weight term\n   \u2212(log 2\u03c0e/2\u03c0)\u00b7T DROPPED. Rationale: \u03c8[F + S_b] crosses POSITIVE on\n   [5.47, ~16] (negative weight \u00d7 negative-\u03c8 T-block), violating the\n   `marginTilde_convex` hypothesis h\u03c8; every FAlt block has provably\n   negative \u03c8 (D-057 rows #1/#3/#4 \u2192 `FAlt_psi_neg`). FAlt \u2265 F + S_b\n   pointwise for T \u2265 0, so the literature majorant property upgrades\n   unchanged. Margin cost 2(log 2\u03c0e/2\u03c0)T \u2248 0.9\u221an \u2014 256 at n = 8\u00d710\u2074\n   against margin\u0303 = 15 764 (E-028-scale): negligible.\n3. **Two-point base (secant) instead of derivative base.**\n   `pos_of_convex_of_two_points` (ConvexOn.slope_mono_adjacent) replaces\n   margin\u0303\u2032(N\u2080) > 0: the remaining numeric obligations are two plain\n   evaluations of the explicit margin function \u2014 no derivative machinery\n   needed for the discharge. (`pos_of_convex_of_base`, the MVT +\n   monotone-derivative variant, remains proved in the file.)\n4. **Regime split at n = 10\u2075.** Finite verification (perimeter, to\n   5\u00d710\u2075) covers n < 10\u2075; the margin argument covers n \u2265 10\u2075 via the\n   two base points 8\u00d710\u2074 < 10\u2075. `SfBoundProp` range: [10\u2075, N\u2081].\n   (Convexity + two-point positivity does NOT give positivity between\n   the points \u2014 convex functions can dip \u2014 hence the split at the second\n   point, not the first.)\n\n## 2. The isolated obligation\n\n```\nSfBoundProp : \u2200 n : \u2115, 10\u2075 \u2264 n \u2192 (n:\u211d) \u2264 (3\u00b710\u00b9\u00b2 \u2212 1)\u00b2 \u2192\n              |Sf n| \u2264 Bn FAlt n\n```\n\nwith `Bn FAlt n` the explicit D-037 (4.1) bound at A = 10.5, B\u2080 = 48\n(D-056), \u0108\u2080/H\u0302 closed forms, M\u2080 = 1.3352, IIMaj, T = \u221an + 1.\n\n## 3. Triage: what is inside SfBoundProp\n\nLayer-by-layer decomposition of its eventual proof (D-036/D-037/D-056),\nwith tractability verdicts:\n\n| Layer | Content | Verdict |\n|-------|---------|---------|\n| L0 | Rectangle contour identity for k_n(w\u22121)(\u2212\u03b6\u2032/\u03b6): residues at zeros give the truncated zero sum; assembling Sf = S_\u221e + 1 \u2212 \u03bb_n from the contour output | **Mathlib-partial**: meromorphic residue machinery on rectangles is thin in current Mathlib; this is the main formalization lift (plain complex analysis, no input obstacles) |\n| L1 | Kernel bounds: \\|k_n\\| \u2264 2, \u2264 e\u2074+1, \u2264 e^{\u221an/2}+1; stepping (6.12); trivial residue \u2264 1 | **Mathlib-tractable** (elementary real/complex estimates; D-036 re-derived) |\n| L2 | Reference-point R-bound (D-056 Thm R: \\|R(s)\\| \u2264 10.5 log(\\|t\\|+2) + 48): partial fractions for \u03b6\u2032/\u03b6 (Hadamard product of \u03be), digamma Lemma D, unit-interval grouping | **Mathlib-tractable modulo L4** (plain complex analysis; the zero-count input C\u2080 is the only non-elementary piece and it enters through L4) |\n| L3 | Zero-avoiding T \u2208 [\u221an, \u221an+1] (pigeonhole gap center, D-036 \u00a72) | **Mathlib-tractable modulo L4** (finite combinatorics on the C\u2080 count) |\n| L4 | **Trudgian 2014 explicit N(T), S(T) bounds** (underlies C\u2080, hence L2/L3, and the 2F(T) zeros term via FAlt) | **PERIMETER (recommended \u2014 decision below)** |\n| L5 | Bridge: zeros with \\|\u03b3\\| \u2264 T \u2264 T\u2080 on the line \u27f9 each zero term \u2264 2 | uses `RHUpTo` \u2014 **already perimeter** |\n| L6 | M\u2080 \u2264 1.3352 on the short piece \\|t\\| \u2264 10 | grid-verified (E-023); **computational perimeter after E-023b** (acb box cover) \u2014 same class as Platt\u2013Trudgian (interval-arithmetic certificate) |\n| L7 | liCoeff summability (the tsum honesty note) | folds into L0 (the contour identity forces the relevant convergence); flag for the formalizer |\n\n## 4. The perimeter decision (deliberate, per the notes' instruction)\n\n**Decision: Trudgian 2014's explicit N(T)/S(T) bounds go INSIDE the\ntrusted perimeter** \u2014 the same class as Platt\u2013Trudgian 2021 (which is\nalready a named hypothesis `RHUpTo`) and zeta-23-lean's treatment of\npublished inputs (hEF/hRvM). Rationale:\n\n- Trudgian 2014 is refereed, published, with machine-checked constants;\n  it is *infrastructure*, not part of this paper's contribution. Our\n  contribution (R-004) is the ASSEMBLY \u2014 the S_\u221e lower bound, the margin\n  convexity, the bridge window, the traced R-bound \u2014 all of which are\n  either already Lean-proved (tier (i)) or Mathlib-tractable (L1\u2013L3).\n- Formalizing Trudgian from scratch is Backlund\u2013Rosser-class explicit\n  zero-counting: plausibly a larger project than everything formalized\n  so far combined (the notes' warning), with zero insight gained into\n  R-004's actual content.\n- Perimeters are honest when declared. The paper's Formal verification\n  appendix now declares exactly: Platt\u2013Trudgian (computational),\n  Misguich\u2013Voros/E-011/E-015 (computational), Trudgian 2014 (published\n  explicit bounds), M\u2080 (interval-arithmetic certificate, after E-023b).\n\n**Consequence for the tag when L0\u2013L3 are eventually discharged:**\nR-004 would read [Lean-verified modulo published explicit N(T)/S(T)\nbounds (Trudgian 2014) + computational certificates (Platt\u2013Trudgian\nRH-to-3\u00d710\u00b9\u00b2; Li verification to 5\u00d710\u2075; M\u2080 acb certificate)] \u2014 a fully\nhonest, fully declared endpoint. No further shrinkage is meaningful\nwithout formalizing published infrastructure.\n\n## 5. Step-2 discharge plan (base points) \u2014 VALIDATED NUMERICALLY\n\nhbase and hbase2 reduce to rational interval bounds on log/exp/\u221a at\nn = 8\u00d710\u2074 and n = 10\u2075. Certified constants and every link pre-verified\n(mpmath dps 40, session 012):\n\nPrimitives: e \u2208 [2.7182818283, 2.7182818286] (Mathlib d9), \u03c0 \u2208\n[3.1415926535, 3.1415926536] (d9), log 2 \u2208 [0.6931471803, 0.6931471808]\n(d9); exp lower bounds by partial sums (`Real.sum_le_exp_of_nonneg`),\nexp upper bounds by exp x = (exp(x/16))\u00b9\u2076 \u2264 (1/(1\u2212x/16))\u207b\u00b9\u2076\n(from `Real.add_one_le_exp` at \u2212x/16).\n\nVerified links (bound, target, margin):\n- e^11.263 \u2264 78056 < 80000 (2.4%) \u27f9 log 80000 \u2265 11.263\n- e^11.3 \u2265 80822 > 80000 (1.0%) \u27f9 log 80000 \u2264 11.3\n- e^11.5 \u2264 99507 < 100000 (0.5%) \u27f9 log 100000 \u2265 11.5\n- e^5.7 \u2265 298.9 > 286 (4.5%) \u27f9 log T, log(T+2) \u2264 5.7 (n = 8\u00d710\u2074)\n- e^5.8 \u2265 330.3 > 320 (3.2%) \u27f9 log T, log(T+2) \u2264 5.8 (n = 10\u2075)\n- e^1.75 \u2265 5.755 > 5.7 (1.0%) \u27f9 log log \u2264 1.75; e^1.77 \u2265 5.871 > 5.8\n  (1.2%) \u27f9 log log \u2264 1.77\n- e^5.6 \u2264 273.6 < 285 (4.0%) \u27f9 log 285 \u2265 5.6 (lower-bound side at 8\u00d710\u2074)\n- e^1.14 \u2264 3.1287 < \u03c0 (0.41%) \u27f9 log \u03c0 \u2265 1.14; e^1.1448 \u2265 3.14182 > \u03c0\n  (0.007% \u2014 tightest link; exact rational arithmetic, acceptable)\n  \u27f9 log \u03c0 \u2264 1.1448\n- e\u2074 \u2208 [54.5978, 54.6015] (exact pow of the d9 bounds)\n- \u221a80000 \u2264 283 (283\u00b2 = 80089 \u2265 80000), \u221a100000 \u2264 317 (317\u00b2 = 100489)\n- IIMaj \u2264 4.56(s+1)\u00b72 via e^{\u2212as}, e^{\u2212bs} \u2264 1 (crude, slack absorbs)\n\nResulting certified values (computed with the certified constants):\n- slower(8\u00d710\u2074) \u2265 336 998; Bn(8\u00d710\u2074) \u2264 327 038 \u27f9 margin \u2265 9 960 > 0 \u2713\n  (hbase)\n- slower(10\u2075) \u2265 433 098; Bn(10\u2075) \u2264 346 878 \u27f9 margin(10\u2075) \u2265 86 220\n- slower(8\u00d710\u2074) \u2264 338 671; Bn(8\u00d710\u2074) \u2265 274 683 \u27f9 margin(8\u00d710\u2074)\n  \u2264 63 989 < 86 220 \u2264 margin(10\u2075) \u2713 (hbase2)\n\n(True values: 15 764 and ~93 000 \u2014 the certified plan has \u2265 9 960 and\n\u2265 22 000 slack on the two comparisons respectively.) Estimated Lean\neffort: ~400\u2013600 lines of interval grind following the\n`block_range_bounds`/`iimaj_bracket_bound` patterns.\n\n## 6. Roadmap after step 2\n\n| Remaining obligation | Disposition |\n|---|---|\n| hbase, hbase2 | step 2 plan above (next sub-stage) |\n| SfBoundProp L0\u2013L3 | multi-session formalization (contour + residue machinery); the honest long pole |\n| SfBoundProp L4 | perimeter (decided, \u00a74) |\n| SfBoundProp L6 (M\u2080) | E-023b acb certificate \u2192 computational perimeter |\n| L5, hfinite, _hRH | already perimeter |\n"
}