← Session 3 — Project kickoff: RH blueprint, staged workflow + archive design
thinking (3441 chars)
0.2c committed. Continue to 0.2d (linear algebra §3 + chain §6 = includes task 0.3). I've already read §3 (lines 400-452) and §6 (lines 1173-1207). Write D-005 reproducing Lemma 3.1, 3.2, Remark 3.3, Lemma 3.4, and the chain.
Lemma 3.2 independent reproduction (task 0.3): Let me re-derive carefully.
Statement: P,Q Hermitian d×d, P ⪰ 0, rank P ≤ r, n₊(Q) ≤ b. Then r ≥ 2tr P + 4tr Q − 4b − ‖P+Q‖²_HS.
Proof structure: Q = Q⁺ − Q⁻ (Jordan decomposition), Q± ⪰ 0, Q⁺Q⁻ = 0, rank Q⁺ = n₊(Q) ≤ b.
‖P+Q‖²_HS = tr(P + Q⁺ − Q⁻)² = ‖P‖² + ‖Q⁺‖² + ‖Q⁻‖² + 2tr(PQ⁺) − 2tr(PQ⁻) − 2tr(Q⁺Q⁻).
tr(PQ⁺) ≥ 0 (product of PSD has nonnegative trace ✔), tr(Q⁺Q⁻) = 0 ✔.
So ‖P+Q‖² ≤ ... wait we need lower bound on r, so need upper bound on ‖P+Q‖²? No: r ≥ 2trP + 4trQ − 4b − ‖P+Q‖² ⟺ ‖P+Q‖² ≥ 2trP + 4trQ − 4b − r. So need LOWER bound on ‖P+Q‖²_HS.
‖P+Q‖² ≥ ‖P‖² − 2tr(PQ⁻) + ‖Q⁻‖² + ‖Q⁺‖² (dropping 2tr(PQ⁺) ≥ 0).
Von Neumann trace inequality: tr(PQ⁻) ≤ Σᵢ pᵢnᵢ (eigenvalues in decreasing order, both ⪰0).
⟹ ‖P‖² − 2tr(PQ⁻) + ‖Q⁻‖² ≥ Σpᵢ² − 2Σpᵢnᵢ + Σnᵢ² = Σ(pᵢ − nᵢ)².
Now Σᵢ(pᵢ−nᵢ)² ≥ Σ_{i≤r}(pᵢ−nᵢ)² + Σ_{i>r}nᵢ² (pᵢ=0 for i>r since rank P ≤ r ✔).
For i≤r: (p−n)² = p² −2pn + n²... the paper uses x² ≥ 2x−1: (pᵢ−nᵢ)² ≥ 2(pᵢ−nᵢ) − 1. ✔
Σ_{i≤r} [2(pᵢ−nᵢ)−1] = 2tr P − r − 2Σ_{i≤r}nᵢ.
Then −2Σ_{i≤r}nᵢ ≥ −4Σ_{i≤r}nᵢ (since nᵢ ≥ 0). And Σ_{i>r}nᵢ² ≥ 0 ≥ −4Σ_{i>r}nᵢ. Hmm the paper writes:
Σ_{i≤r}(2(pᵢ−nᵢ)−1) + Σ_{i>r}nᵢ² ≥ 2tr P − r − 4tr Q⁻.
Check: 2trP − r − 2Σ_{i≤r}nᵢ + Σ_{i>r}nᵢ² ≥ 2trP − r − 4Σ_{i≤r}nᵢ − 4Σ_{i>r}nᵢ? Need −2Σ_{i≤r}nᵢ ≥ −4Σ_{i≤r}nᵢ ✔ (n≥0) and Σ_{i>r}nᵢ² ≥ −4Σ_{i>r}nᵢ ✔ (n² ≥ 0 ≥ −4n). ✔ So ‖P‖²−2tr(PQ⁻)+‖Q⁻‖² ≥ 2trP − r − 4trQ⁻.
‖Q⁺‖² = Σqⱼ² over ≤ b positive eigenvalues: q² ≥ 4q − 4 (x²≥4x−4 ⟺ (x−2)²≥0 ✔) ⟹ ‖Q⁺‖² ≥ 4trQ⁺ − 4b. ✔
Total: ‖P+Q‖² ≥ 2trP − r − 4trQ⁻ + 4trQ⁺ − 4b = 2trP − r + 4trQ − 4b. Rearranged: r ≥ 2trP + 4trQ − 4b − ‖P+Q‖². ✔ Equality case: P = Π₁, Q = 2Π₂, Π₁⊥Π₂ projections ranks r, b: tr P = r, tr Q = 2b, ‖P+Q‖² = r + 4b. RHS: 2r + 8b − 4b − r − 4b = r ✔ equality.
Remark 3.3: alternative variational proof; also Q=0 recovers rank P ≥ (tr P)²/‖P‖² (Cauchy–Schwarz rank bound) — check: with Q = 0, b=0: r ≥ 2trP − ‖P‖²... hmm that's weaker than (trP)²/‖P‖² in general; the remark says "setting Q=0 and optimising the coefficient 2 recovers rank P ≥ (trP)²/‖P‖²" — i.e., using x² ≥ 2λx − λ²... with optimal λ = ... scalar inequality (p−n)² ≥ 2λ(p−n) − λ², optimize λ: get r ≥ 2λtrP − λ²... hmm rank P ≥ 2λ tr P − λ²... wait Σ(pᵢ−nᵢ)² ≥ Σ_{i≤r}(2λpᵢ − λ²) − ... gives rλ² ≥ 2λtrP − ‖P+Q‖²... at λ = trP/r... optimize over λ: r ≥ 2λtrP − ‖P‖² over λ²: max at λ = trP/r gives r ≥ (trP)²/‖P‖²... circular but recoverable. Fine, note it.
Lemma 3.1: Q₀ Hermitian on ℂᵐ, A: ℂᵈ→ℂᵐ linear. n₊(A*Q₀A) ≤ n₊(Q₀). Proof: if A*Q₀A positive definite on U ⊂ ℂᵈ, A|U injective (x∈U, Ax=0 ⟹ x*A*Q₀Ax = 0 ⟹ x=0), Q₀ positive definite on A(U), dim U = dim A(U) ≤ n₊(Q₀). ✔ This is Sylvester inertia for congruence — standard.
Lemma 3.4 (Weyl): A, E Hermitian, ‖E‖ ≤ θ ⟹ n₊(A) ≥ #{i : λᵢ(A+E) > θ}. Via Courant–Fischer λᵢ(A+E) ≤ λᵢ(A) + ‖E‖. Wait direction: λᵢ(A) ≥ λᵢ(A+E) − ‖E‖ ≥ λᵢ(A+E) − θ > 0 for those i ⟹ n₊(A) ≥ count ✔.
Where is Lemma 3.4 used? Probably in §6 or for handling Ẽ tail in inertia. Not critical for chain; note it.
Chain (1.2) full assembly — already verified in D-004 §9. D-005 will consolidate: Lemma 3.2 reproduction (task 0.3) + chain assembly verification + equality/sharpness cases.
Write D-005.
0.2c committed (`67fd4c8`). Proceeding to **0.2d — linear algebra + chain assembly** (this also fulfills task 0.3, the independent Lemma 3.2 reproduction).
tool: Write ok
input
{
"file_path": "D:\\Python\\Quantum\\research\\derivations\\D-005-linear-algebra-and-chain.md",
"content": "# D-005 \u2014 Linear algebra (\u00a73) + chain assembly (\u00a76); task 0.3 fulfilled\nDate: 2026-08-17 | Session: 001 | Tasks: 0.2d + 0.3 | Status: complete\nSource: fulltext pp. 5\u20136 (\u00a73), p. 11 (\u00a76). Re-derived independently.\n\n---\n\n## Lemma 3.1 (Inertia under pull-back). [VERIFIED]\nQ\u2080 Hermitian on \u2102\u1d50, A : \u2102\u1d48 \u2192 \u2102\u1d50 linear \u27f9 n\u208a(A*Q\u2080A) \u2264 n\u208a(Q\u2080).\nProof re-derived: if A*Q\u2080A is positive definite on U \u2282 \u2102\u1d48, then A|_U is\ninjective (Ax = 0, x \u2208 U \u27f9 x*A*Q\u2080Ax = 0 \u27f9 x = 0) and Q\u2080 is positive\ndefinite on A(U); hence dim U = dim A(U) \u2264 n\u208a(Q\u2080). Taking U maximal:\nn\u208a(A*Q\u2080A) \u2264 n\u208a(Q\u2080). \u2714 (This is Sylvester's law of inertia for\ncongruence; A need not be invertible \u2014 injectivity on U suffices.)\n\n## Lemma 3.2 (Rank\u2013trace inequality) \u2014 TASK 0.3 INDEPENDENT REPRODUCTION\n**Statement.** P, Q Hermitian d\u00d7d, P \u2ab0 0, rank P \u2264 r, n\u208a(Q) \u2264 b \u27f9\n r \u2265 2 tr P + 4 tr Q \u2212 4b \u2212 \u2016P+Q\u2016\u00b2_HS. (3.1)\n\n**My reproduction.** Jordan decomposition Q = Q\u207a \u2212 Q\u207b, Q\u00b1 \u2ab0 0, Q\u207aQ\u207b = 0,\nrank Q\u207a = n\u208a(Q) \u2264 b. Expand:\n \u2016P+Q\u2016\u00b2_HS = \u2016P\u2016\u00b2 + \u2016Q\u207a\u2016\u00b2 + \u2016Q\u207b\u2016\u00b2 + 2tr(PQ\u207a) \u2212 2tr(PQ\u207b) \u2212 2tr(Q\u207aQ\u207b).\ntr(PQ\u207a) \u2265 0 (trace of product of two PSD matrices: tr(PQ\u207a) =\ntr(P^{1/2}Q\u207aP^{1/2}) \u2265 0 \u2714); tr(Q\u207aQ\u207b) = 0 \u2714. Drop the \u22650 term:\n \u2016P+Q\u2016\u00b2 \u2265 \u2016P\u2016\u00b2 \u2212 2tr(PQ\u207b) + \u2016Q\u207b\u2016\u00b2 + \u2016Q\u207a\u2016\u00b2. (*)\nVon Neumann trace inequality: tr(PQ\u207b) \u2264 \u03a3\u1d62 p\u1d62n\u1d62 (p\u2081\u2265\u22ef\u2265p_d \u22650 eigenvalues\nof P, n\u2081\u2265\u22ef\u2265n_d\u22650 of Q\u207b). \u27f9 first three terms of (*) satisfy\n \u2016P\u2016\u00b2 \u2212 2tr(PQ\u207b) + \u2016Q\u207b\u2016\u00b2 \u2265 \u03a3\u1d62(p\u1d62 \u2212 n\u1d62)\u00b2. (**)\nSplit at r (p\u1d62 = 0 for i > r since rank P \u2264 r):\n \u03a3\u1d62(p\u1d62\u2212n\u1d62)\u00b2 \u2265 \u03a3_{i\u2264r}(p\u1d62\u2212n\u1d62)\u00b2 + \u03a3_{i>r} n\u1d62\u00b2.\nScalar inequality x\u00b2 \u2265 2x \u2212 1 at x = p\u1d62\u2212n\u1d62 (i\u2264r):\n \u03a3_{i\u2264r}(p\u1d62\u2212n\u1d62)\u00b2 \u2265 2\u03a3_{i\u2264r}(p\u1d62\u2212n\u1d62) \u2212 r = 2tr P \u2212 r \u2212 2\u03a3_{i\u2264r}n\u1d62\n \u2265 2tr P \u2212 r \u2212 4\u03a3_{i\u2264r}n\u1d62 (n\u1d62 \u2265 0).\nAnd \u03a3_{i>r}n\u1d62\u00b2 \u2265 0 \u2265 \u22124\u03a3_{i>r}n\u1d62. Since tr Q\u207b = \u03a3_{all i} n\u1d62:\n (**) \u2265 2tr P \u2212 r \u2212 4tr Q\u207b. (***)\nFor Q\u207a: positive eigenvalues q\u2081..q_{b\u2032}, b\u2032 \u2264 b; scalar (x\u22122)\u00b2 \u2265 0, i.e.\nx\u00b2 \u2265 4x \u2212 4:\n \u2016Q\u207a\u2016\u00b2 = \u03a3 q\u2c7c\u00b2 \u2265 \u03a3(4q\u2c7c \u2212 4) = 4tr Q\u207a \u2212 4b\u2032 \u2265 4tr Q\u207a \u2212 4b. (****)\nInsert (***),(****) into (*):\n \u2016P+Q\u2016\u00b2 \u2265 2tr P \u2212 r \u2212 4tr Q\u207b + 4tr Q\u207a \u2212 4b\n = 2tr P \u2212 r + 4tr Q \u2212 4b (tr Q = tr Q\u207a \u2212 tr Q\u207b).\nRearranged: r \u2265 2tr P + 4tr Q \u2212 4b \u2212 \u2016P+Q\u2016\u00b2. \u220e [VERIFIED \u2014 every\ninequality step independently justified]\n\n**Equality case (checked):** P = \u03a0\u2081, Q = 2\u03a0\u2082, orthogonal projections\n\u03a0\u2081 \u22a5 \u03a0\u2082, ranks r, b: tr P = r, tr Q = 2b, \u2016P+Q\u2016\u00b2 = tr \u03a0\u2081 + 4tr \u03a0\u2082 =\nr + 4b. RHS = 2r + 8b \u2212 4b \u2212 (r + 4b) = r \u2714 equality.\n**Tightness map (where the proof can lose):** (i) dropping 2tr(PQ\u207a) \u2265 0 \u2014\nlossy unless P \u22a5 Q\u207a; (ii) von Neumann \u2014 lossy unless P, Q\u207b simultaneously\ndiagonalizable with aligned order; (iii) x\u00b2 \u2265 2x\u22121 \u2014 tight only at\np\u1d62\u2212n\u1d62 = 1; (iv) x\u00b2 \u2265 4x\u22124 \u2014 tight only at q\u2c7c = 2. \u27f9 The certificate is\ntight exactly for eigenvalue pattern {1}_P, {2}_Q: this is why simple\nzeros (charge 1) and off-line pairs (charge... matching v-norms \u2248 1, pairs\nat signature (1,1) scaled by 2) saturate it. Any improvement must exploit\na regime where these four inequalities are NOT simultaneously tight \u2014\nkey input for task 1.1.\n\n**Remark 3.3 (variational view, checked):** minimize U \u21a6 \u2016P+UQU*\u2016\u00b2_HS\nover the (compact) unitary group; first-order condition tr([P,UQU*]H) = 0\n\u2200 Hermitian H \u27f9 [P, UQU*] = 0 \u27f9 simultaneous diagonalization \u27f9 (3.1)\nreduces to scalar (x\u22121)\u00b2 \u2265 0, x\u00b2 \u2265 0, (x\u22122)\u00b2 \u2265 0 in the three sign cases.\nSetting Q = 0 and optimizing the scalar parameter recovers the\nCauchy\u2013Schwarz rank bound rank P \u2265 (tr P)\u00b2/\u2016P\u2016\u00b2_HS. \u2714\n[Note: Lemma 3.2 with Q\u22600 is NOT implied by C\u2013S; the 4tr Q \u2212 4b term is\nthe genuinely new content \u2014 it charges off-line mass at rate 4 instead of\nlosing it entirely.]\n\n**Genealogy (checked against \u00a71.2):** (3.1) is the matrix form of\nm\u00b2 \u2265 2m \u2212 1 (per-zero: multiplicity m costs m\u00b2 in \u2016G\u0303\u2016\u00b2, earns 2m\u22121...\ni.e. m\u00b2 \u2212 (2m\u22121) = (m\u22121)\u00b2 \u2265 0); with simple zeros on the rank side and\nmultiple ones at flat charge 4 it recovers m\u00b2 \u2265 3m \u2212 2\n(m\u00b2 \u2212 (3m\u22122) = (m\u22121)(m\u22122) \u2265 0 \u2714). The flat charge 4 for Q-eigenvalues\nis what treats off-line pairs and multiple zeros uniformly.\n\n## Lemma 3.4 (Weyl). [VERIFIED]\nA, E Hermitian, \u2016E\u2016 \u2264 \u03b8 \u27f9 n\u208a(A) \u2265 #{i : \u03bb\u1d62(A+E) > \u03b8}.\nCourant\u2013Fischer: \u03bb\u1d62(A) \u2265 \u03bb\u1d62(A+E) \u2212 \u2016E\u2016 > \u03b8 \u2212 \u03b8 = 0 for each counted i. \u2714\n(Role: lets inertia statements survive the o(1) tail \u1ebc; insurance for the\nchain, used implicitly when passing from G\u0303+\u1ebc to G\u0303.)\n\n## Chain assembly (\u00a76) \u2014 full verification\nSetup: P\u2081 := (aL\u00b2)\u207b\u00b9 \u03a3_{\u03c1\u2208on, m_\u03c1=1} v_\u03c1v_\u03c1\u1d40 (simple on-line), Q\u2032 := G\u0303 \u2212 P\u2081.\n- P\u2081 \u2ab0 0, rank P\u2081 \u2264 s\u2081, tr P\u2081 \u2264 s\u2081 (Lemma 2.1, m_\u03c1=1: each \u2016v_\u03c1\u2016\u00b2 \u2264 aL\u00b2). \u2714\n- Q\u2032 = pull-back of \u2295_{on, m\u22652} m_\u03c1|x|\u00b2 \u2295 \u2295_pairs [[0,m_\u03c1],[m_\u03c1,0]] \u2014\n the pair block [[0,m],[m,0]] has eigenvalues \u00b1m \u2714 (one positive per pair);\n on-line multiple zeros contribute one positive direction each \u27f9\n n\u208a(Q\u2032) \u2264 s\u2082 + p (Lemma 3.1). \u2714\n- Apply Lemma 3.2 with r = s\u2081, b = s\u2082 + p, tr Q\u2032 = tr G\u0303 \u2212 tr P\u2081:\n rank P\u2081 \u2265 2tr P\u2081 + 4(tr G\u0303 \u2212 tr P\u2081) \u2212 4(s\u2082+p) \u2212 \u2016G\u0303\u2016\u00b2\n = 4tr G\u0303 \u2212 2tr P\u2081 \u2212 4(s\u2082+p) \u2212 \u2016G\u0303\u2016\u00b2.\n- Key inequality: tr P\u2081 + 2(s\u2082+p) \u2264 s\u2081 + 2s\u2082 + 2p \u2264 N(I\u2032)\n (tr P\u2081 \u2264 s\u2081; m_\u03c1 \u2265 2 per multiple on-line point; m \u2265 1 per off-line zero,\n 2 zeros per pair). \u2714 \u27f9 \u22122tr P\u2081 \u2212 4(s\u2082+p) \u2265 \u22122N(I\u2032).\n- \u27f9 rank P\u2081 \u2265 4tr G\u0303 \u2212 2N(I\u2032) \u2212 \u2016G\u0303\u2016\u00b2_HS\n = 4N(I\u2032) \u2212 2N(I\u2032) \u2212 R(\u03c8)N + o(N) = (2 \u2212 R(\u03c8) \u2212 o(1))N\n (Prop 4.2 + Thm 5.7 + N(I\u2032) = N(I) + O(\u221aT L)). \u2714\n- Rank side: N^s_0(I) = s\u2081 \u2212 O(\u221aT L) \u2265 rank P\u2081 \u2212 O(\u221aT L) (Cor 4.5). \u2714\n\u27f9 (1.2): N^s_0 \u2265 (2 \u2212 R(\u03c8) \u2212 o(1))N. \u03c8\u2080: 2 \u2212 4/3 = 2/3 \u220e (i).\n(ii): from the display before the key inequality:\n 3tr P\u2081... rearranged form: 3s\u2081 + 4(s\u2082+p) \u2265 4tr G\u0303 \u2212 \u2016G\u0303\u2016\u00b2 (using\n tr P\u2081 \u2264 s\u2081 to go from \u22122tr P\u2081 to \u2265 \u22122s\u2081: check \u2014 rank P\u2081 \u2265 4tr G\u0303 \u2212\n 2tr P\u2081 \u2212 4(s\u2082+p) \u2212 \u2016G\u0303\u2016\u00b2 and rank P\u2081 \u2264 s\u2081, tr P\u2081 \u2264 s\u2081 \u27f9\n s\u2081 \u2265 4tr G\u0303 \u2212 2s\u2081 \u2212 4(s\u2082+p) \u2212 \u2016G\u0303\u2016\u00b2 \u27f9 3s\u2081 + 4(s\u2082+p) \u2265 4tr G\u0303 \u2212 \u2016G\u0303\u2016\u00b2 \u2714);\n subtract s\u2081 + 2s\u2082 + 2p \u2264 N(I\u2032):\n 2(s\u2081+s\u2082+p) \u2265 (3 \u2212 R(\u03c8) \u2212 o(1))N; N_d(I\u2032) \u2265 s\u2081+s\u2082+2p \u2265 s\u2081+s\u2082+p \u27f9\n N_d \u2265 \u00bd(3 \u2212 R(\u03c8) \u2212 o(1))N. \u03c8\u2080: \u00bd(3\u22124/3) = 5/6 \u220e (ii). [VERIFIED]\nCumulative (0,T): dyadic summation, rate O(log log T/log T) (Remark 6.1). \u2714\nTheorem B: \u03c7-twisted inputs, no poles for \u03c7\u2260\u03c7\u2080, chain unchanged. \u2714\n\n## TASK 0.3 SIGN-OFF\nLemma 3.2 reproduced independently with all four loss-points mapped and\nthe equality case confirmed. The inequality is elementary (von Neumann +\ntwo scalar inequalities) but the STRUCTURE \u2014 charging Q at rate 4 with\ncap 4b \u2014 is the paper's load-bearing idea.\n\n## OBSERVATIONS FOR THE ATTACK\n1. **The four tightness conditions are the blueprint for improvement.**\n Beating 2/3 requires either (i) data that makes tr(PQ\u207a) > 0 usable\n (correlation between simple-zero vectors and off-line/multiple mass),\n (ii) eigenvalue distributions of P, Q\u207b that break von Neumann alignment,\n or (iii)/(iv) non-saturating eigenvalues \u2014 i.e. moments beyond the\n second. All three need NEW prime-side input (support > 1 or higher\n moments) \u2014 consistent with \u00a77.2, now understood mechanistically.\n2. The chain uses rank P\u2081 \u2264 s\u2081 AND tr P\u2081 \u2264 s\u2081 (both saturated by simple\n zeros). Multiple on-line zeros waste (m_\u03c1\u22121) trace AND occupy Q\u2032-budget\n at rate... a double zero on the line costs 2 in N but returns 0 rank:\n the worst case for the certificate. Bounding multiple-zero density by\n OTHER means (e.g. derivatives of \u03be, Levinson-style) would tighten\n tr P\u2081 + 2(s\u2082+p) \u2264 N \u2014 a cross-track hook (Track A \u2194 classical\n mollifier methods).\n"
}
result 2026-08-17 18:40:44Z → 2026-08-22 02:54:59Z
{
"type": "create",
"filePath": "D:\\Python\\Quantum\\research\\journal\\session-017.md",
"content": "# Session 017 \u2014 2026-08-21 \u2014 Tier ii\u2032 sub-stage ii\u2032-1b(iii) COMPLETE (ii\u2032-1b now fully done)\n\n## Directive\nContinue tier ii\u2032 per D-064: finish ii\u2032-1b \u2014 (iii) the rectangle residue\ntheorem for the Lagarias-kernel integrand J (STATE.md NEXT ACTION).\n\n## Work done\n**ii\u2032-1b(iii) COMPLETE (commit f3d7244)** \u2014 LiSides.lean (~460 lines, 19\nnew declarations, single-file check clean, full `lake build` GREEN 8745\njobs \u2014 first build covering LiResidue/LiPrincipal, which session 016 had\nleft out of the package root; root NguyenRH1.lean now imports all three):\n\n* `kFun n w = (w/(w\u22121))\u207f\u22121`, `Jlag n w = kFun n w\u00b7(\u2212\u03b6\u2032/\u03b6(w))`,\n `Rfun n = Jlag n \u2212 ppart n` + differentiability/continuity kits\n (`kFun_differentiableAt`, `ppart_differentiableAt`,\n `Jlag_differentiableAt`, `Rfun_differentiableAt`, `ppart_continuousAt`).\n* `zeta_order_ne_top_of_ne` : analyticOrderAt \u03b6 \u03c1 \u2260 \u22a4 for all \u03c1 \u2260 1 \u2014\n identity principle through the ENTIRE zetaA (avoids punctured-plane\n connectedness): analyticOrderAt_ne_top_of_isPreconnected on univ with\n zetaA 1 = 1 \u2260 0, then order(zetaA) = order((w\u22121)\u00b7\u03b6) = 0 + order(\u03b6)\n via `analyticOrderAt_congr` + `analyticOrderAt_mul`. NOTE: zetaA's\n value-1-at-1 also makes `riemannZeta 1`'s junk value irrelevant\n everywhere \u2014 no `\u03b6(1) \u2260 0` lemma needed.\n* `rectangle_mem_nhds_of_mem_not_border` \u2014 interior from border avoidance\n (extracted from the vendored hZint argument).\n* **Removable singularity at 1** (`Rfun_bounded_near_one`): on \ud835\udcdd[\u2260] 1,\n R = (Ffun n \u2212 TaylP n)/(w\u22121)^{n+1} (`Rfun_eq_sub_div_near_one`, from\n `Jlag_mul_pow` + `ppart_mul_pow`); `Ffun_sub_TaylP_order`: order \u2265 n+1\n via `natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero` \u2014\n `iteratedDeriv_TaylP` (the i-th deriv of the Taylor poly matches Ffun's:\n descFactorial/0^{j\u2212i} split, `Finset.sum_eq_single`); then\n `Rfun_tendsto_one` by cases on order = \u22a4 (R \u2192 0) or factorization\n g = (w\u22121)^m\u00b7h with m \u2265 n+1 (R \u2192 0^{m\u2212n\u22121}\u00b7h(1)). Residue at 1 is 0\n for R \u2014 exactly what `residueTheorem_finset` needs with 1 \u2208 S.\n* **Residue at a zero** (`Rfun_residue_at`): for ANY \u03c1 \u2260 1,\n R \u2212 mult(\u03c1)\u00b7(1\u2212(\u03c1/(\u03c1\u22121))\u207f)/(w\u2212\u03c1) is bounded on \ud835\udcdd[\u2260] \u03c1 \u2014 logDeriv normal\n form \u03b6 = (w\u2212\u03c1)^m\u00b7h, h(\u03c1) \u2260 0 (from `zeta_order_ne_top_of_ne` +\n `AnalyticAt.analyticOrderAt_ne_top`), so \u2212\u03b6\u2032/\u03b6 = \u2212m/(w\u2212\u03c1) \u2212 h\u2032/h; the\n kFun slope \u2192 kFun\u2032(\u03c1), h\u2032/h and ppart continuous. Multiple zeros OK\n (logDeriv poles are simple). Sign check: residue = \u2212m\u00b7kFun n \u03c1\n = m\u00b7(1\u2212(\u03c1/(\u03c1\u22121))\u207f) \u2713 matches D-064.\n* **`rectInt'_Jlag`** (the deliverable): rectangle with 1 interior, no\n zeros of \u03b6 on the border, Sz any finset with\n `s \u2208 Sz \u2194 s \u2208 Rectangle \u2227 zetaA s = 0` (supplied form, like the\n vendored `rectangleIntegral'_mul_logDeriv`; downstream produces Sz from\n `finite_zeros_rectangle` \u2014 zetaA is entire so it applies across w = 1):\n RectangleIntegral' (Jlag n) z w\n = ResW1 n + \u03a3_{\u03c1 \u2208 Sz} (zeroMult \u03c1)\u00b7(1 \u2212 (\u03c1/(\u03c1\u22121))\u207f).\n Proof: residueTheorem_finset on R with S = insert 1 Sz, A 1 = 0,\n A \u03c1 = mult\u00b7(1\u2212(\u03c1/(\u03c1\u22121))\u207f); then Jlag = Rfun + ppart,\n `RectangleIntegral'_add`, `rectInt'_ppart` (session 016).\n\nAxiom audit (PrintAxioms.lean): all 19 declarations \u2014 propext,\nClassical.choice, Quot.sound ONLY. No sorryAx.\n\n**Deferred (documented in file header):** zeroMult(\u22122) = 1 (trivial-zero\nsimplicity \u2014 not in Mathlib/Zeta23; would need the functional-equation\nderiv computation). The sum keeps zeroMult symbolic; the\nSz = {nontrivial} \u222a {\u22122} split on the D-064 rectangle is ii\u2032-4 territory.\n\n## Lean notes (hard-won this session, additions to the handoff list)\n- `analyticOrderAt_ne_top_of_isPreconnected` is **AnalyticOnNhd-namespaced**\n (`AnalyticOnNhd.analyticOrderAt_ne_top_of_isPreconnected`).\n- `mul_div_cancel_left\u2080 (b) (ha : a \u2260 0) : a * b / a = b` \u2014 the EXPLICIT\n arg is b (the kept factor); pass `_`.\n- `Tendsto.congr'` needs an `EventuallyEq` \u2014 a raw `\u2200\u1da0 s, f s = c` has no\n `.symm`; ascribe the have as `f =\u1da0[l] g` explicitly.\n- `mem_nhdsWithin_of_mem_nhds` yields the raw set-membership form\n ({x | p x} \u2208 \ud835\udcdd s); coerce to `f =\u1da0[\ud835\udcdd s] g` by type ascription before\n `.deriv_eq` / `.self_of_nhds` dot-projection works.\n- `analyticOrderAt_mul` in a `rw` needs `(f := ...) (g := ...)` named \u2014\n `analyticAt_id.sub analyticAt_const` elaborates to `id \u2212 const`, not\n the `fun w => w \u2212 1` lambda; `show`-bridge for the defeq.\n- `field_simp` sometimes closes the cleared goal itself \u2014 a trailing\n `ring` then errors \"no goals\". Remove on recompile error.\n- `Nat.cast_analyticOrderNatAt (h : order \u2260 \u22a4) : \u2191orderNat = order` \u2014\n rewrite direction `\u2190 ... at h` to turn an order bound into a nat bound\n (`ENat.natCast_le_natCast.mp`).\n- `riemannZeta 1 = (\u03b3 \u2212 log 4\u03c0)/2` (Mathlib ZetaAsymp) \u2014 junk value but\n nonzero; routing everything through zetaA avoids needing it.\n\n## State at stop\nii\u2032-1b (R1 residue machinery) FULLY COMPLETE: (i) ResW1_eq_sum, (ii)\nrectInt'_ppart, (iii) rectInt'_Jlag. The sides identity\nsides(T) = ResW1 n + \u03a3_{\u03c1 \u2208 Sz} mult\u00b7(1\u2212(\u03c1/(\u03c1\u22121))\u207f) is now a Lean theorem.\nNext: **ii\u2032-2** \u2014 R2(i)/(ii) elementary swaps: \u03bb_n = \u03a3_j (\u22121)^{j+1}C(n,j)\u03c3_j\n(binomial + paired swap) and S_\u221e = \u03a3_j C(n,j)\u03c4_{j\u22121} (D-064 \u00a74 R2).\n",
"structuredPatch": [],
"originalFile": null
}
raw content_json (database row)
[{"type":"thinking","thinking":"0.2c committed. Continue to 0.2d (linear algebra §3 + chain §6 = includes task 0.3). I've already read §3 (lines 400-452) and §6 (lines 1173-1207). Write D-005 reproducing Lemma 3.1, 3.2, Remark 3.3, Lemma 3.4, and the chain.\n\nLemma 3.2 independent reproduction (task 0.3): Let me re-derive carefully.\n\nStatement: P,Q Hermitian d×d, P ⪰ 0, rank P ≤ r, n₊(Q) ≤ b. Then r ≥ 2tr P + 4tr Q − 4b − ‖P+Q‖²_HS.\n\nProof structure: Q = Q⁺ − Q⁻ (Jordan decomposition), Q± ⪰ 0, Q⁺Q⁻ = 0, rank Q⁺ = n₊(Q) ≤ b.\n‖P+Q‖²_HS = tr(P + Q⁺ − Q⁻)² = ‖P‖² + ‖Q⁺‖² + ‖Q⁻‖² + 2tr(PQ⁺) − 2tr(PQ⁻) − 2tr(Q⁺Q⁻).\ntr(PQ⁺) ≥ 0 (product of PSD has nonnegative trace ✔), tr(Q⁺Q⁻) = 0 ✔.\nSo ‖P+Q‖² ≤ ... wait we need lower bound on r, so need upper bound on ‖P+Q‖²? No: r ≥ 2trP + 4trQ − 4b − ‖P+Q‖² ⟺ ‖P+Q‖² ≥ 2trP + 4trQ − 4b − r. So need LOWER bound on ‖P+Q‖²_HS.\n‖P+Q‖² ≥ ‖P‖² − 2tr(PQ⁻) + ‖Q⁻‖² + ‖Q⁺‖² (dropping 2tr(PQ⁺) ≥ 0).\nVon Neumann trace inequality: tr(PQ⁻) ≤ Σᵢ pᵢnᵢ (eigenvalues in decreasing order, both ⪰0).\n⟹ ‖P‖² − 2tr(PQ⁻) + ‖Q⁻‖² ≥ Σpᵢ² − 2Σpᵢnᵢ + Σnᵢ² = Σ(pᵢ − nᵢ)².\nNow Σᵢ(pᵢ−nᵢ)² ≥ Σ_{i≤r}(pᵢ−nᵢ)² + Σ_{i>r}nᵢ² (pᵢ=0 for i>r since rank P ≤ r ✔).\nFor i≤r: (p−n)² = p² −2pn + n²... the paper uses x² ≥ 2x−1: (pᵢ−nᵢ)² ≥ 2(pᵢ−nᵢ) − 1. ✔\nΣ_{i≤r} [2(pᵢ−nᵢ)−1] = 2tr P − r − 2Σ_{i≤r}nᵢ.\nThen −2Σ_{i≤r}nᵢ ≥ −4Σ_{i≤r}nᵢ (since nᵢ ≥ 0). And Σ_{i>r}nᵢ² ≥ 0 ≥ −4Σ_{i>r}nᵢ. Hmm the paper writes:\nΣ_{i≤r}(2(pᵢ−nᵢ)−1) + Σ_{i>r}nᵢ² ≥ 2tr P − r − 4tr Q⁻.\nCheck: 2trP − r − 2Σ_{i≤r}nᵢ + Σ_{i>r}nᵢ² ≥ 2trP − r − 4Σ_{i≤r}nᵢ − 4Σ_{i>r}nᵢ? Need −2Σ_{i≤r}nᵢ ≥ −4Σ_{i≤r}nᵢ ✔ (n≥0) and Σ_{i>r}nᵢ² ≥ −4Σ_{i>r}nᵢ ✔ (n² ≥ 0 ≥ −4n). ✔ So ‖P‖²−2tr(PQ⁻)+‖Q⁻‖² ≥ 2trP − r − 4trQ⁻.\n‖Q⁺‖² = Σqⱼ² over ≤ b positive eigenvalues: q² ≥ 4q − 4 (x²≥4x−4 ⟺ (x−2)²≥0 ✔) ⟹ ‖Q⁺‖² ≥ 4trQ⁺ − 4b. ✔\nTotal: ‖P+Q‖² ≥ 2trP − r − 4trQ⁻ + 4trQ⁺ − 4b = 2trP − r + 4trQ − 4b. Rearranged: r ≥ 2trP + 4trQ − 4b − ‖P+Q‖². ✔ Equality case: P = Π₁, Q = 2Π₂, Π₁⊥Π₂ projections ranks r, b: tr P = r, tr Q = 2b, ‖P+Q‖² = r + 4b. RHS: 2r + 8b − 4b − r − 4b = r ✔ equality.\n\nRemark 3.3: alternative variational proof; also Q=0 recovers rank P ≥ (tr P)²/‖P‖² (Cauchy–Schwarz rank bound) — check: with Q = 0, b=0: r ≥ 2trP − ‖P‖²... hmm that's weaker than (trP)²/‖P‖² in general; the remark says \"setting Q=0 and optimising the coefficient 2 recovers rank P ≥ (trP)²/‖P‖²\" — i.e., using x² ≥ 2λx − λ²... with optimal λ = ... scalar inequality (p−n)² ≥ 2λ(p−n) − λ², optimize λ: get r ≥ 2λtrP − λ²... hmm rank P ≥ 2λ tr P − λ²... wait Σ(pᵢ−nᵢ)² ≥ Σ_{i≤r}(2λpᵢ − λ²) − ... gives rλ² ≥ 2λtrP − ‖P+Q‖²... at λ = trP/r... optimize over λ: r ≥ 2λtrP − ‖P‖² over λ²: max at λ = trP/r gives r ≥ (trP)²/‖P‖²... circular but recoverable. Fine, note it.\n\nLemma 3.1: Q₀ Hermitian on ℂᵐ, A: ℂᵈ→ℂᵐ linear. n₊(A*Q₀A) ≤ n₊(Q₀). Proof: if A*Q₀A positive definite on U ⊂ ℂᵈ, A|U injective (x∈U, Ax=0 ⟹ x*A*Q₀Ax = 0 ⟹ x=0), Q₀ positive definite on A(U), dim U = dim A(U) ≤ n₊(Q₀). ✔ This is Sylvester inertia for congruence — standard.\n\nLemma 3.4 (Weyl): A, E Hermitian, ‖E‖ ≤ θ ⟹ n₊(A) ≥ #{i : λᵢ(A+E) > θ}. Via Courant–Fischer λᵢ(A+E) ≤ λᵢ(A) + ‖E‖. Wait direction: λᵢ(A) ≥ λᵢ(A+E) − ‖E‖ ≥ λᵢ(A+E) − θ > 0 for those i ⟹ n₊(A) ≥ count ✔.\n\nWhere is Lemma 3.4 used? Probably in §6 or for handling Ẽ tail in inertia. Not critical for chain; note it.\n\nChain (1.2) full assembly — already verified in D-004 §9. D-005 will consolidate: Lemma 3.2 reproduction (task 0.3) + chain assembly verification + equality/sharpness cases.\n\nWrite D-005.","signature":""},{"type":"text","text":"0.2c committed (`67fd4c8`). Proceeding to **0.2d — linear algebra + chain assembly** (this also fulfills task 0.3, the independent Lemma 3.2 reproduction)."},{"type":"tool_use","id":"Write_60","name":"Write","input":{"file_path":"D:\\Python\\Quantum\\research\\derivations\\D-005-linear-algebra-and-chain.md","content":"# D-005 — Linear algebra (§3) + chain assembly (§6); task 0.3 fulfilled\nDate: 2026-08-17 | Session: 001 | Tasks: 0.2d + 0.3 | Status: complete\nSource: fulltext pp. 5–6 (§3), p. 11 (§6). Re-derived independently.\n\n---\n\n## Lemma 3.1 (Inertia under pull-back). [VERIFIED]\nQ₀ Hermitian on ℂᵐ, A : ℂᵈ → ℂᵐ linear ⟹ n₊(A*Q₀A) ≤ n₊(Q₀).\nProof re-derived: if A*Q₀A is positive definite on U ⊂ ℂᵈ, then A|_U is\ninjective (Ax = 0, x ∈ U ⟹ x*A*Q₀Ax = 0 ⟹ x = 0) and Q₀ is positive\ndefinite on A(U); hence dim U = dim A(U) ≤ n₊(Q₀). Taking U maximal:\nn₊(A*Q₀A) ≤ n₊(Q₀). ✔ (This is Sylvester's law of inertia for\ncongruence; A need not be invertible — injectivity on U suffices.)\n\n## Lemma 3.2 (Rank–trace inequality) — TASK 0.3 INDEPENDENT REPRODUCTION\n**Statement.** P, Q Hermitian d×d, P ⪰ 0, rank P ≤ r, n₊(Q) ≤ b ⟹\n r ≥ 2 tr P + 4 tr Q − 4b − ‖P+Q‖²_HS. (3.1)\n\n**My reproduction.** Jordan decomposition Q = Q⁺ − Q⁻, Q± ⪰ 0, Q⁺Q⁻ = 0,\nrank Q⁺ = n₊(Q) ≤ b. Expand:\n ‖P+Q‖²_HS = ‖P‖² + ‖Q⁺‖² + ‖Q⁻‖² + 2tr(PQ⁺) − 2tr(PQ⁻) − 2tr(Q⁺Q⁻).\ntr(PQ⁺) ≥ 0 (trace of product of two PSD matrices: tr(PQ⁺) =\ntr(P^{1/2}Q⁺P^{1/2}) ≥ 0 ✔); tr(Q⁺Q⁻) = 0 ✔. Drop the ≥0 term:\n ‖P+Q‖² ≥ ‖P‖² − 2tr(PQ⁻) + ‖Q⁻‖² + ‖Q⁺‖². (*)\nVon Neumann trace inequality: tr(PQ⁻) ≤ Σᵢ pᵢnᵢ (p₁≥⋯≥p_d ≥0 eigenvalues\nof P, n₁≥⋯≥n_d≥0 of Q⁻). ⟹ first three terms of (*) satisfy\n ‖P‖² − 2tr(PQ⁻) + ‖Q⁻‖² ≥ Σᵢ(pᵢ − nᵢ)². (**)\nSplit at r (pᵢ = 0 for i > r since rank P ≤ r):\n Σᵢ(pᵢ−nᵢ)² ≥ Σ_{i≤r}(pᵢ−nᵢ)² + Σ_{i>r} nᵢ².\nScalar inequality x² ≥ 2x − 1 at x = pᵢ−nᵢ (i≤r):\n Σ_{i≤r}(pᵢ−nᵢ)² ≥ 2Σ_{i≤r}(pᵢ−nᵢ) − r = 2tr P − r − 2Σ_{i≤r}nᵢ\n ≥ 2tr P − r − 4Σ_{i≤r}nᵢ (nᵢ ≥ 0).\nAnd Σ_{i>r}nᵢ² ≥ 0 ≥ −4Σ_{i>r}nᵢ. Since tr Q⁻ = Σ_{all i} nᵢ:\n (**) ≥ 2tr P − r − 4tr Q⁻. (***)\nFor Q⁺: positive eigenvalues q₁..q_{b′}, b′ ≤ b; scalar (x−2)² ≥ 0, i.e.\nx² ≥ 4x − 4:\n ‖Q⁺‖² = Σ qⱼ² ≥ Σ(4qⱼ − 4) = 4tr Q⁺ − 4b′ ≥ 4tr Q⁺ − 4b. (****)\nInsert (***),(****) into (*):\n ‖P+Q‖² ≥ 2tr P − r − 4tr Q⁻ + 4tr Q⁺ − 4b\n = 2tr P − r + 4tr Q − 4b (tr Q = tr Q⁺ − tr Q⁻).\nRearranged: r ≥ 2tr P + 4tr Q − 4b − ‖P+Q‖². ∎ [VERIFIED — every\ninequality step independently justified]\n\n**Equality case (checked):** P = Π₁, Q = 2Π₂, orthogonal projections\nΠ₁ ⊥ Π₂, ranks r, b: tr P = r, tr Q = 2b, ‖P+Q‖² = tr Π₁ + 4tr Π₂ =\nr + 4b. RHS = 2r + 8b − 4b − (r + 4b) = r ✔ equality.\n**Tightness map (where the proof can lose):** (i) dropping 2tr(PQ⁺) ≥ 0 —\nlossy unless P ⊥ Q⁺; (ii) von Neumann — lossy unless P, Q⁻ simultaneously\ndiagonalizable with aligned order; (iii) x² ≥ 2x−1 — tight only at\npᵢ−nᵢ = 1; (iv) x² ≥ 4x−4 — tight only at qⱼ = 2. ⟹ The certificate is\ntight exactly for eigenvalue pattern {1}_P, {2}_Q: this is why simple\nzeros (charge 1) and off-line pairs (charge... matching v-norms ≈ 1, pairs\nat signature (1,1) scaled by 2) saturate it. Any improvement must exploit\na regime where these four inequalities are NOT simultaneously tight —\nkey input for task 1.1.\n\n**Remark 3.3 (variational view, checked):** minimize U ↦ ‖P+UQU*‖²_HS\nover the (compact) unitary group; first-order condition tr([P,UQU*]H) = 0\n∀ Hermitian H ⟹ [P, UQU*] = 0 ⟹ simultaneous diagonalization ⟹ (3.1)\nreduces to scalar (x−1)² ≥ 0, x² ≥ 0, (x−2)² ≥ 0 in the three sign cases.\nSetting Q = 0 and optimizing the scalar parameter recovers the\nCauchy–Schwarz rank bound rank P ≥ (tr P)²/‖P‖²_HS. ✔\n[Note: Lemma 3.2 with Q≠0 is NOT implied by C–S; the 4tr Q − 4b term is\nthe genuinely new content — it charges off-line mass at rate 4 instead of\nlosing it entirely.]\n\n**Genealogy (checked against §1.2):** (3.1) is the matrix form of\nm² ≥ 2m − 1 (per-zero: multiplicity m costs m² in ‖G̃‖², earns 2m−1...\ni.e. m² − (2m−1) = (m−1)² ≥ 0); with simple zeros on the rank side and\nmultiple ones at flat charge 4 it recovers m² ≥ 3m − 2\n(m² − (3m−2) = (m−1)(m−2) ≥ 0 ✔). The flat charge 4 for Q-eigenvalues\nis what treats off-line pairs and multiple zeros uniformly.\n\n## Lemma 3.4 (Weyl). [VERIFIED]\nA, E Hermitian, ‖E‖ ≤ θ ⟹ n₊(A) ≥ #{i : λᵢ(A+E) > θ}.\nCourant–Fischer: λᵢ(A) ≥ λᵢ(A+E) − ‖E‖ > θ − θ = 0 for each counted i. ✔\n(Role: lets inertia statements survive the o(1) tail Ẽ; insurance for the\nchain, used implicitly when passing from G̃+Ẽ to G̃.)\n\n## Chain assembly (§6) — full verification\nSetup: P₁ := (aL²)⁻¹ Σ_{ρ∈on, m_ρ=1} v_ρv_ρᵀ (simple on-line), Q′ := G̃ − P₁.\n- P₁ ⪰ 0, rank P₁ ≤ s₁, tr P₁ ≤ s₁ (Lemma 2.1, m_ρ=1: each ‖v_ρ‖² ≤ aL²). ✔\n- Q′ = pull-back of ⊕_{on, m≥2} m_ρ|x|² ⊕ ⊕_pairs [[0,m_ρ],[m_ρ,0]] —\n the pair block [[0,m],[m,0]] has eigenvalues ±m ✔ (one positive per pair);\n on-line multiple zeros contribute one positive direction each ⟹\n n₊(Q′) ≤ s₂ + p (Lemma 3.1). ✔\n- Apply Lemma 3.2 with r = s₁, b = s₂ + p, tr Q′ = tr G̃ − tr P₁:\n rank P₁ ≥ 2tr P₁ + 4(tr G̃ − tr P₁) − 4(s₂+p) − ‖G̃‖²\n = 4tr G̃ − 2tr P₁ − 4(s₂+p) − ‖G̃‖².\n- Key inequality: tr P₁ + 2(s₂+p) ≤ s₁ + 2s₂ + 2p ≤ N(I′)\n (tr P₁ ≤ s₁; m_ρ ≥ 2 per multiple on-line point; m ≥ 1 per off-line zero,\n 2 zeros per pair). ✔ ⟹ −2tr P₁ − 4(s₂+p) ≥ −2N(I′).\n- ⟹ rank P₁ ≥ 4tr G̃ − 2N(I′) − ‖G̃‖²_HS\n = 4N(I′) − 2N(I′) − R(ψ)N + o(N) = (2 − R(ψ) − o(1))N\n (Prop 4.2 + Thm 5.7 + N(I′) = N(I) + O(√T L)). ✔\n- Rank side: N^s_0(I) = s₁ − O(√T L) ≥ rank P₁ − O(√T L) (Cor 4.5). ✔\n⟹ (1.2): N^s_0 ≥ (2 − R(ψ) − o(1))N. ψ₀: 2 − 4/3 = 2/3 ∎ (i).\n(ii): from the display before the key inequality:\n 3tr P₁... rearranged form: 3s₁ + 4(s₂+p) ≥ 4tr G̃ − ‖G̃‖² (using\n tr P₁ ≤ s₁ to go from −2tr P₁ to ≥ −2s₁: check — rank P₁ ≥ 4tr G̃ −\n 2tr P₁ − 4(s₂+p) − ‖G̃‖² and rank P₁ ≤ s₁, tr P₁ ≤ s₁ ⟹\n s₁ ≥ 4tr G̃ − 2s₁ − 4(s₂+p) − ‖G̃‖² ⟹ 3s₁ + 4(s₂+p) ≥ 4tr G̃ − ‖G̃‖² ✔);\n subtract s₁ + 2s₂ + 2p ≤ N(I′):\n 2(s₁+s₂+p) ≥ (3 − R(ψ) − o(1))N; N_d(I′) ≥ s₁+s₂+2p ≥ s₁+s₂+p ⟹\n N_d ≥ ½(3 − R(ψ) − o(1))N. ψ₀: ½(3−4/3) = 5/6 ∎ (ii). [VERIFIED]\nCumulative (0,T): dyadic summation, rate O(log log T/log T) (Remark 6.1). ✔\nTheorem B: χ-twisted inputs, no poles for χ≠χ₀, chain unchanged. ✔\n\n## TASK 0.3 SIGN-OFF\nLemma 3.2 reproduced independently with all four loss-points mapped and\nthe equality case confirmed. The inequality is elementary (von Neumann +\ntwo scalar inequalities) but the STRUCTURE — charging Q at rate 4 with\ncap 4b — is the paper's load-bearing idea.\n\n## OBSERVATIONS FOR THE ATTACK\n1. **The four tightness conditions are the blueprint for improvement.**\n Beating 2/3 requires either (i) data that makes tr(PQ⁺) > 0 usable\n (correlation between simple-zero vectors and off-line/multiple mass),\n (ii) eigenvalue distributions of P, Q⁻ that break von Neumann alignment,\n or (iii)/(iv) non-saturating eigenvalues — i.e. moments beyond the\n second. All three need NEW prime-side input (support > 1 or higher\n moments) — consistent with §7.2, now understood mechanistically.\n2. The chain uses rank P₁ ≤ s₁ AND tr P₁ ≤ s₁ (both saturated by simple\n zeros). Multiple on-line zeros waste (m_ρ−1) trace AND occupy Q′-budget\n at rate... a double zero on the line costs 2 in N but returns 0 rank:\n the worst case for the certificate. Bounding multiple-zero density by\n OTHER means (e.g. derivatives of ξ, Levinson-style) would tighten\n tr P₁ + 2(s₂+p) ≤ N — a cross-track hook (Track A ↔ classical\n mollifier methods).\n"},"extra_content":null}]