{
  "file_path": "D:\\Python\\Quantum\\research\\derivations\\D-006-sharpness-ceiling-lean.md",
  "content": "# D-006 \u2014 \u00a77 sharpness/ceiling + conditional extensions + Lean (App. A)\nDate: 2026-08-17 | Session: 001 | Task: 0.2e | Status: complete\nSource: fulltext pp. 12\u201317. This completes the 0.2 sub-stage series.\n\n---\n\n## 1. \u00a77.1 \u2014 Position vs. prior work (map)\n- [Ary22]/[BGSTB24]: unconditional Fej\u00e9r-kernel sum over zero differences\n  = (4/3+o(1))(T/2\u03c0)log T \u2014 the zero-side reading of our \u2016G\u0303\u2016\u00b2_HS.\n- [GS25 Thm 2]: unconditional bound on the diagonal (\u03b3=\u03b3\u2032) sum with\n  constant C < 2 would give \u2265 2\u2212C simple/on-line; C = 4/3 needs discarding\n  \u03b3\u2260\u03b3\u2032 terms = termwise positivity that FAILS off the line. [BGSTB25,\n  GS26] achieve it under \"all zeros within o(1/log T) of the line\".\n- Theorem A = unconditional substitute reaching their 2\u2212C = 2/3: instead\n  of isolating the horizontal diagonal termwise, Lemma 3.2 bounds the rank\n  from tr, \u2016\u00b7\u2016_HS, and positive index. 5/6 = (3\u2212C)/2 = average of simple\n  and critical proportions [GS25 Thm 3(ii)] = RH-conditional [CGG98,(1.2)].\n- Bombieri [Bom00]: negative index of truncated Weil form = #off-line\n  pairs seen. Yoshida [Yos92]: positivity of W on small support.\n  **No prior use of positive index/rank + second moment together.**\n\n## 2. \u00a77.2 \u2014 Sharpness and limits (THE ceiling analysis)\n\n**(a) Dimension.** rank P, n\u208a(G\u0303) \u2264 d = N(1+o(1)): trivial ceiling 100%.\nX \u2264 T restriction is from Prop 5.4 (off-diagonal primes). X \u226b T needs\nHardy\u2013Littlewood prime-pair info \u27fa Montgomery pair correlation for\nsupport > 1 [Mon73, GM87].\nExtreme configuration test: all zeros off-line pairs \u27f9 rank P = 0,\nn\u208a(Q) \u2264 N/2, Lemma 3.2 forces \u2016G\u0303\u2016\u00b2 \u2265 2N > (4/3)N \u2014 contradiction with\n(P) only shows \u2265 2/3 are not of this kind. **Nothing in the method\ndistinguishes \"two thirds\" from \"all\".** [This is the precise statement of\nthe wall.]\n\n**(b) Sharpness of the three counts.** Given only tr, \u2016\u00b7\u2016\u00b2_HS, block\nstructure, tr P\u2081 \u2264 s\u2081: \u00a76 inequalities are SHARP. Extremal: (2/3)N\nmutually orthogonal simple on-line + (1/6)N on-line doubles realizes\ntr = N, \u2016\u00b7\u2016\u00b2 = (4/3)N, s\u2081 = (2/3)N, N_d = (5/6)N \u2014 Montgomery's RH\nextremal. Off-line pairs of depth \u2192 0 are spectrally identical; there\nThm A(i) is exact (2/3) and A(ii) is not sharp (N_d = N). \u27f9 **Improving\nthe constants with this exact data set is impossible** (formal sense).\n\n**(c) Two levels of integrality.** (P,Q) decomposition recovers\n(m\u22121)\u00b2 \u2265 0; (P\u2081,Q\u2032) regrouping recovers (m\u22121)(m\u22122) \u2265 0. Interacting\nsimple zeros (eigenvalues in (0,2)) are harmless on the rank side;\nmultiple on-line points and off-line pairs sit on the index side at flat\ncharge 4. = [CGG98,(1.2)] made unconditional.\n\n**(d) CMS connection.** Lemma 3.2 is the m=1 case of the one-sided\nChebyshev\u2013Markov\u2013Stieltjes bound: knowing moments d\u207b\u00b9tr G\u0303\u1d4f for k \u2264 2m,\nthe sharp lower bound for n\u208a(G\u0303)/d is 1 \u2212 \u039b_m(0), \u039b_m = Christoffel\nfunction of the moment sequence at 0. \u27f9 The natural upgrade path is\nMOMENTS, and the upgrade is quantified by Christoffel functions.\n\n**(e) Rudnick\u2013Sarnak wall.** Prime-side evaluation of tr G\u0303\u1d4f by the\ndiagonal method works exactly when X\u1d4f \u2264 T^{2\u2212\u03b5} [RS96]. At X \u224d T: only\nk = 1,2 (tr G\u0303 and \u2016G\u0303\u2016\u00b2 = tr G\u0303\u00b2). **Unconditionally, higher moments add\nnothing.** [Confirmed: this is why the certificate is a 2-moment object.]\n\n**(f) Conditional ladder HL*(k\u2080).** Hypothesis: tr G\u0303\u1d4f = d\u00b7m_k(1)(1+o(1))\nfor k \u2264 k\u2080, where m_k(1) = k-th moment of the limiting spectral\ndistribution of the sine-kernel Gram matrix over the sine process.\n(k=4 encodes Hardy\u2013Littlewood-type additive correlations\n\u03a3_m(\u039b\u2217\u039b)(m)(\u039b\u2217\u039b)(m+h), |h| \u2264 X\u00b2/T.)\nComputed: m_k(1) = 1, 4/3, 2, 13/4 (k \u2264 4); \u039b\u2082(0;1) = 5/36.\nHL*(4) \u27f9 N^s_0/N \u2265 13/18 = 0.7222. HL*(\u221e) \u27f9 100% simple on line \u2014 the\nceiling of (a). **RH itself is out of reach of the mechanism.**\nComplementary to [GLSS25]: full-support pair correlation conjecture \u27f9\n100% simple zeros on the line.\n[Verify later (Phase 1): m_k sequence and 13/18 computation \u2014 reproduction\ntarget 1.3; the moment sequence 1, 4/3, 2, 13/4 looks like it comes from a\nspecific density \u2014 identify it: candidate \u03c1(x) = (2/\u03c0)\u221a... or Mar\u010denko\u2013\nPastur-like. NUMERICALLY CHECKABLE. \u2192 logged as open thread.]\n\n**The bandwidth-one ceiling (\u2248 0.682, partially Lean-verified).**\nDefinition: a bandwidth-one certificate p depends on the zero\nconfiguration only through its first two trace moments against test\nfunctions of Fourier support in [\u22121,1] + the on-line/off-line partition,\nand satisfies p \u2264 N^s_0/N configuration-wise. Thm A(i)'s certificate is of\nthis kind.\nLean theorem `Zeta23.PairCeiling.ceiling_law256`: for any such p and any\nwindow r of Fourier support in [\u22121,1],\n  c\u2080 + \u222b\u2080\u00b9 r(x)x dx \u2264 p + 0.824|r(1)| + 2.55\u00d710\u207b\u2076(|r\u2032(1)| + \u222b\u2080\u00b9|r\u2033|)\nunder hypotheses h_valid (sampled form factor S_j of the explicit\n256-periodic law, `Zeta23/PairCeiling/LawN256.lean` \u2014 optimum of the\nfinite program) and EnclOK (form-factor enclosures).\np\u2080 := 1 \u2212 a_N \u2264 0.6818287 (exact rational, rounded up).\nBand-limited windows have r(\u00b11) = 0 \u27f9 0.824-term vanishes \u27f9 bound\np\u2080 + 2.55\u00d710\u207b\u2076(|r\u2032(1)| + \u222b|r\u2033|) < 0.6819 for |r\u2032(1)| + \u222b|r\u2033| < 8.2\n(both windows (2.6) qualify).\n**Audit caveat:** at tag v1.0 the enclosures EnclOK are certified by\nINTERVAL ARITHMETIC, not the Lean kernel. Kernel-checked (given EnclOK):\n255 near-CUE row inequalities |256S(j) \u2212 j| \u2264 3\u00d710\u207b\u2074\u2070, edge bound\n|D(1)| \u2264 0.82395317 and its sign, analytic stability inequality. This is\nthe ONLY numerical certification in the paper; Theorems A/B are\nindependent of it (3 standard axioms only).\n\u27f9 **Theorem A is within 0.016 of the ceiling of its own method class.**\nBeating 0.682 provably requires leaving bandwidth one (support > 1\nform-factor input) or using \u2265 3 moments.\n\n## 3. \u00a77.3 \u2014 Conditional extensions (roadmap material)\nUnder RH, tr G\u0303\u00b3 available [Hej94, RS96]. Cubic weight\n\u03c9(m) = \u00bdm + (1/18)(2m\u00b2 \u2212 m\u00b3) + (4/9)\u00b71_{m=1} (tight at m = 1,2,3;\nSchur\u2013Horn + convex minorant of \u2212x\u00b2/9 + x\u00b3/18); window cos(8s/5)1_{|s|\u22641/2}\n+ [BHB13] N^s/N \u2265 19/27 (RH) \u27f9 N_d/N \u2265 0.85082 (cf. 0.8477 [CGdL20] RH).\nIf Montgomery's form factor were known on support (\u2212\u03bb\u2080,\u03bb\u2080) for ALL \u03bb\u2080:\nmethod certifies 100% simple zeros on the line.\n\n## 4. Remark 7.1 \u2014 Zeros of \u03be\u2032 (unconditional, new)\nSame argument applied to \u03be\u2032: N^s_{0,\u03be\u2032}/N_{\u03be\u2032} \u2265 0.85838 (flat window);\n0.86864 with quartic window v(s) = 1 \u2212 (7/100)(2s)\u00b2 \u2212 (51/200)(2s)\u2074;\ndistinct: 0.92919 / 0.93432.\nComparators: Conrey 79.874% (uncond.); FGL14 85.84% (RH); CGdL20\n0.8825/0.9412 (RH). Wu [Wu15] 0.86957 on-line (not simple, uncond.) \u2014\nNOT exceeded; the new content is SIMPLICITY. Flat-window 85.838% =\nFGL's RH-constant with RH removed. Lean: `Zeta23.XiPrime.*`.\n\n## 5. Appendix A \u2014 Lean formalisation (facts for task 0.5)\nToolchain v4.33.0-rc2; Mathlib 51e6992efd06; repo tag v1.0;\ngithub.com/anthropics/zeta-23-lean.\nCounting functions defined directly against Mathlib's riemannZeta\n(Zeta23/Statement.lean). Main theorems carry NO hypotheses:\n`two_thirds_on_critical_line`, `thmB_0_mult` (2/3 simple on-line),\n`thmC_0_mult` (5/6 distinct), Montgomery\u2013Taylor variants with\ncMT := \u221a2 tan(1/\u221a2)/(1 + (1/\u221a2)tan(1/\u221a2)), Theorem B analogues,\ncomparator/ directory restating against Mathlib alone.\nAudit: no axiom declarations beyond Mathlib's; #print axioms on all main\ndeclarations \u27f9 only propext, Classical.choice, Quot.sound; no sorry.\nContributed to Mathlib: von Neumann trace inequality (Hermitian), both\ndirections of Sylvester's law of inertia (Hermitian forms).\nAnalytic inputs (\u00a72) appear as theorems in their own right; several ported\nwith attribution from PrimeNumberTheoremAnd [PNT+].\n\n## 6. SYNTHESIS \u2014 the obstruction map, now mechanistic (Phase 1 input)\n| Wall | Precise mechanism | Escape requires |\n|---|---|---|\n| 2/3 certificate | Lemma 3.2 tight at eigenvalues {1}_P,{2}_Q (D-005) | data breaking simultaneous tightness |\n| 0.682 bandwidth-one | 2-moment + support-[\u22121,1] certificates: finite program optimum p\u2080 \u2264 0.6818287 (Lean + interval arith.) | support > 1 OR \u2265 3 moments |\n| X \u2264 T (bandwidth) | Prop 5.4 off-diagonal O(L\u00b2X) vs main TL\u00b3 (D-004) | Hardy\u2013Littlewood prime-pair input |\n| moments k \u2264 2 | Rudnick\u2013Sarnak X\u1d4f \u2264 T^{2\u2212\u03b5} (\u00a77.2e) | new unconditional moment input |\n| RH itself | sine-process moments give 100% simple but not RH (\u00a77.2f) | DIFFERENT mechanism entirely |\n\n**Open threads logged to STATE.md:**\n- T1: reproduce m_k(1) = 1,4/3,2,13/4 + \u039b\u2082(0;1) = 5/36 numerically\n  (identify the limiting density) \u2014 feeds Phase 1 task 1.3.\n- T2: Christoffel/CMS formulation (\u00a77.2d) \u2014 is there a weighted/variant\n  CMS bound using tr G\u0303\u00b2 differently? (task 1.1 material)\n- T3: the 0.824 edge constant / finite program LawN256 \u2014 understand the\n  256-periodic law construction before attempting to beat 0.682.\n- T4: \u03be\u2032-analogue (Remark 7.1) \u2014 the method is stronger on \u03be\u2032; do our\n  Track A ideas also transfer there? (cheap secondary target)\n"
}

{
  "type": "create",
  "filePath": "D:\\Python\\Quantum\\research\\journal\\session-008.md",
  "content": "# Session 008 \u2014 2026-08-19\n## Regroup + R7 registration; task 3.8 COMPLETE (R-004 finite-height Li theorem)\n\n### Part 1 \u2014 Regroup (user-requested) and resources registration\n- User asked for a regroup + formal registration of the resources folder.\n- Created research/resources/index.md: all 43 notes cataloged in 4 groups\n  (Foundations / Zeros & explicit formulas / RH equivalences / RMT\n  statistics), each mapped to the track/task it feeds.\n- NGUYEN.md \u00a72: R7 row added. D-001 Part III: pointer entry.\n- Found: research/paper/Detailed_Derivations_...txt is an OLDER DRAFT\n  duplicate (54,034 vs 54,367 bytes, missing intro) of the resources\n  compendium \u2014 untracked, flagged to user for deletion (not deleted).\n- Committed as session-008 opening (e7b72ad).\n\n### Part 2 \u2014 Task 3.8 (D-037 \u2192 R-004) COMPLETE\nAssembled the explicit finite-height Li theorem. Full chain in D-037:\n1. Read inputs: D-032/D-033 (design), D-036 (constants), E-021 data,\n   Lagarias math/0404394 PDF \u00a71 (Thm 1.1, bridge (1.16)) and \u00a76\n   (Thm 6.1 proof, read in full).\n2. **Coordinate-system audit** of D-036 (variant A kernel-plane vs\n   variant B w-plane): resolved \u2014 D-036/E-021 consistent in variant B\n   (contour in the \u03b6\u2032/\u03b6 argument plane, \u03c3\u2080 = \u22125/2, trivial zero \u22122\n   inside, residue \u2264 1). No bug.\n3. **Real gap found**: D-036's uniform |\u03b6\u2032/\u03b6| bound on segment (III)\n   rests on the R-bound verified only for |t| \u2265 10; the line passes\n   within 1/2 of the trivial pole at w = \u22122. Closed by E-023 S1:\n   M\u2080 = max_{|t|\u226410} |\u03b6\u2032/\u03b6(\u22125/2+it)| = 1.3352 (grid + Lipschitz \u00d72).\n   Contribution 40\u00b7M\u2080 = 53.4 \u2014 negligible.\n4. **S_\u221e elementary lower bound derived** (new, D-037 \u00a73): from\n   Lagarias (4.11) via finite differences:\n   S_\u221e(n) = (1\u2212a\u2081)n \u2212 1 + \u03a3_{m odd\u22653} [(1\u22121/m)\u207f \u2212 1 + n/m]\n   \u27f9 S_\u221e(n) \u2265 \u00bdn log n + (C\u2081\u2212\u03b3/2)n \u2212 4 (n \u2265 20), fully explicit\n   (harmonic bounds). Validated vs E-021 exact values (E-023 V1).\n   Avoids tracing Lagarias \u00a75's O(1) lemmas entirely.\n5. Margin assembly (E-023): margin convex for n \u2265 20; crossover\n   32 871 (traced A=2/B\u2080=2) / 30 217 (measured 0.9/1.0); adopted\n   N\u2080 = 5\u00d710\u2074 (margin 67 705). Finite verification contiguous:\n   ours to 3000 (ledger #3) + Misguich\u2013Voros to 5\u00d710\u2075 (10\u00d7 overlap).\n6. Bridge: n \u2264 (T\u2080\u22121)\u00b2 from the proof's actual requirement\n   (\u221an+1 \u2264 T\u2080); Lagarias's printed (1.16) window T\u00b2/(4log\u00b2T) is\n   conservative slack \u2014 fallback N\u2081* = 2.726\u00d710\u00b2\u00b9 documented.\n\n**THEOREM (R-004, ledger #6):** \u03bb_n > 0 for all\n1 \u2264 n \u2264 N\u2081 = (T\u2080\u22121)\u00b2 = 8 999 999 999 994 000 000 000 001 \u2248 9.0\u00d710\u00b2\u2074,\nT\u2080 = 3\u00d710\u00b9\u00b2 (Platt\u2013Trudgian). Tag [PROVED-CONDITIONAL(computational\nRH-to-T\u2080; finite verification; one numeric sub-bound)]. Criterion-3\ndeliverable; the maximal content of the Li route short of RH (Voros).\n\n### Adversarial review highlights (D-037 \u00a77)\n- P1\u2013P6 proved/elementary; H1\u2013H5 computational/heuristic, each with\n  sensitivity analysis (theorem insensitive to H2/H3 links) and upgrade\n  paths: D-039 (Binet-form digamma sub-bound proof), E-023b (acb box\n  cover for M\u2080).\n- Sanity gates pass: no claim beyond N\u2081; no D-H/Epstein analogue.\n\n### State of the plan\n- Track C (Phase 3): 3.1\u20133.8 ALL CLOSED. The Li/front-A line has\n  delivered its maximal deliverable.\n- Next per plan: 2.10 (E-022 spectral-measure numerics), 2.9-D1 (Krein\n  frame), 2.11 (D-038 transition scale). Optional: D-039, E-023b.\n\n### Handoff notes\n- E-023 script: research/numerics/scripts/E-023-finite-height-assembly.py;\n  data E-023-assembly.csv/.json; db registered (session 8).\n- Platt\u2013Trudgian exact height: \"3\u00d710\u00b9\u00b2\" per title/abstract\n  (arXiv:2004.09765); confirm exact certified height at paper write-up\n  (N\u2081 insensitive at <1% level).\n- N\u2080 could be pushed under 3000 (fully self-contained verification) only\n  with a fundamentally sharper horizontal-segment treatment (I_II/IV\n  dominate B(n) below n ~ 10\u2075: 2(e\u2074+1)\u00b77H(T), H = 3C\u2080\u00b2 ~ zero-avoidance\n  d_min); not needed for the theorem \u2014 literature bridge suffices.\n- E-021 n=10\u2074 rerun still available cheaply via caches (unchanged).\n",
  "structuredPatch": [],
  "originalFile": null
}