← Session 3 — Project kickoff: RH blueprint, staged workflow + archive design
thinking (3140 chars)
Committed (f7af545). Now build E-006: positivity horizon numerics. Design per D-014 §4:
- Gabor-truncated Weil form G̃ vs bandwidth λ ∈ {0.5, 1.0, 1.5, 2.0} at T = 2000, using E-002 zeros.
- Construction: same as E-003 but with L_λ = λ·log(T/2π)... careful: in E-003, L = log(T/2π) ties support to X = T/2π (bandwidth 1). For bandwidth λ: test function support L_λ = λ·ℓ where ℓ = log(T/2π). Grid: critical density for the window: h = 2π/L_λ (per Lemma 2.1 no-aliasing), grid points α_k = T + k·h covering [T, 2T): d_λ = ⌊L_λ T/2π⌋ = λ·1834. At λ=2: d = 3668, matrix 3668² — fine.
- a = ‖ϕ‖²/L_λ.
- G̃_λ = (aL_λ²)⁻¹ Σ_{γ∈I′} v vᵀ, v = ϕ̂_λ(γ − α_k).
- Measure: full eigenvalue spectrum, esp. λ_min; also n₊/d; compare tr/d etc.
- Note: with all zeros on-line, G̃ ⪰ 0 always (PSD by construction up to tail). λ_min measures how close to singular.
- The Groskin budget comparison: B_T ~ (2N+1)ρ log T/(π²T) — his truncation parameters (prime cutoff c, band N, archimedean cutoff T) don't map 1-1 onto ours; I'll compute an analogous scale: our "tail" Ẽ norm bound was T^{−1/2} (Prop 4.3). Compare λ_min with T^{−1/2} scale.
- ALSO the interesting decay: λ_min vs λ — fit exponential/superexponential.
Implementation: reuse E-003's build_phi_hat (mollified window, xi_max_needed = 2T+√T). For λ = 2: L_λ = 2ℓ ≈ 11.5; M_needed = L_λ·(2T+√T)/π ≈ 11.5·4045/π ≈ 14800 → M = 16384; pad 8 → 131072 FFT — fine. d = 3668, zeros in I′ = 2044; V = 2044×3668 (60MB); V.T@V: 2044·3668² ≈ 2.7e10 — a few seconds; eigvalsh 3668² — ~20-40s. Total for 4 λ values: a couple of minutes. Good.
λ_min interpretation caveat: at λ=2, d=3668 > N(I′)=2044 — rank ≤ 2044 < d, so λ_min = 0 automatically (dimension deficit)! Hmm — that pollutes the horizon measurement: the matrix is singular for dimensional reasons when d > #zeros. At λ ≤ 1.1·...: d = λ·1834 vs zeros in I′ = 2044: crossover at λ ≈ 1.11. Above that, G̃ is structurally singular (more rows than vectors) — λ_min ≈ 0 (to numerical precision) regardless of math. The meaningful floor: the smallest POSITIVE eigenvalue (the (d−N′)-th smallest). Hmm — but the paper's truncation is at d ≈ N; the positivity question is about the form on the test-function space — the Gabor vectors at oversampled grid are linearly dependent... The Weil form on the span: the matrix represents the form in an overcomplete basis; rank deficiency = basis redundancy, not form degeneracy. For the horizon measurement I should look at the smallest POSITIVE eigenvalue relative to the bulk scale (e.g. λ_min₊/λ_max or λ_min₊/mean). Let me record: for each λ: d, N′, rank, λ_min₊ (smallest eigenvalue above a numerical-noise threshold), ratio λ_min₊/λ_mean, and log10(λ_min₊/λ_mean) — the "conditioning" of the truncation. Decay of that ratio vs λ is the horizon/complexity measure.
Noise threshold: entries accurate to ~1e-5 relative (frame self-test) — eigenvalue noise floor ~1e-4·λ_max·... use threshold 1e-8·λ_max·d? Estimate empirically: look at eigenvalue gap structure. Simple: report eigenvalues at percentiles and the count below several thresholds (1e-4, 1e-6, 1e-8 relative). Data will speak.
Write E-006 script.
Track C setup committed (`f7af545`). Now building **E-006 — the positivity horizon experiment**.
tool: Write ok
input
{
"file_path": "D:\\Python\\Quantum\\research\\numerics\\scripts\\E-006-positivity-horizon.py",
"content": "\"\"\"E-006 \u2014 Task 3.1 / Q-3.4b: positivity horizon of the truncated Weil form.\n\nFor bandwidth lambda in {0.5, 1, 1.5, 2} build the Gabor-truncated Weil\nform G_lambda on [T, 2T), T = 2000 (construction of E-003/D-002 \u00a73 with\nL_lambda = lambda * log(T/2pi), grid at critical density h = 2pi/L_lambda):\n\n phi_lambda(u) = chi(L/2+u) chi(L/2-u) * 1 (flat window, L = L_lambda)\n G = (a L^2)^-1 sum_{gamma in I'} v_gamma v_gamma^T, a = ||phi||^2/L\n\nAll zeros here are on the line, so G is PSD by construction; the\ninformative quantity is HOW CLOSE to singular the truncation gets as the\nsupport grows \u2014 the conditioning floor. NOTE: when d = lambda*d_1 exceeds\nthe number N' of zeros in I' (crossover lambda ~ 1.11 at this T), the\nmatrix is rank-deficient for dimensional reasons (overcomplete Gabor\nbasis); the meaningful floor is then the smallest POSITIVE eigenvalue.\n\nMetrics per lambda: d, N', numerical rank, eigenvalue percentiles,\nsmallest positive eigenvalue lambda_min+ and the ratios\nlambda_min+/lambda_max, lambda_min+/mean(eig>0); log10 of the ratio =\nconditioning exponent. A superexponential decay of the floor (cf. Kim et\nal. 2026 for Suzuki's operator) would be a complexity wall for positivity\ncertification (Groskin's B_T budget: resolving lambda_min needs precision\n1/lambda_min).\n\nOutputs: research/numerics/data/E-006-positivity-horizon.csv (+ .json)\n\"\"\"\nimport json\nimport sys\nimport time\nfrom datetime import datetime, timezone\nfrom pathlib import Path\n\nimport numpy as np\nfrom scipy.interpolate import CubicSpline\nfrom scipy.linalg import eigvalsh\n\nREPO = Path(__file__).resolve().parents[3]\nDATA = REPO / \"research\" / \"numerics\" / \"data\"\nZEROS_CSV = DATA / \"E-002-zeros-first-10000.csv\"\nCSV = DATA / \"E-006-positivity-horizon.csv\"\nJSON = DATA / \"E-006-positivity-horizon.json\"\n\nT = 2000.0\nLAMBDAS = (0.5, 1.0, 1.5, 2.0)\n\n\ndef chi(u: np.ndarray) -> np.ndarray:\n out = np.zeros_like(u)\n mid = (u > 0) & (u < 1)\n e1 = np.exp(-1.0 / u[mid])\n e2 = np.exp(-1.0 / (1.0 - u[mid]))\n out[mid] = e1 / (e1 + e2)\n out[u >= 1] = 1.0\n return out\n\n\ndef build_phi_hat(L: float, xi_max_needed: float, pad: int = 8, M0: int = 4096):\n M = int(2 ** np.ceil(np.log2(max(M0, L * xi_max_needed / np.pi))))\n du = L / M\n u = -L / 2 + du * np.arange(M)\n phi = chi(L / 2 + u) * chi(L / 2 - u) # flat window psi0\n a = np.sum(phi**2) * du / L\n full = np.zeros(pad * M)\n full[: M // 2] = phi[M // 2:]\n full[-M // 2:] = phi[: M // 2]\n F = np.fft.fft(full) * du\n xi = 2 * np.pi * np.fft.fftfreq(pad * M, d=du)\n order = np.argsort(xi)\n return CubicSpline(xi[order], F[order]), a\n\n\ndef main() -> int:\n if not ZEROS_CSV.exists():\n print(\"E-002 zeros not found\"); return 1\n if CSV.exists() and \"--force\" not in sys.argv:\n print(f\"cached: {CSV} exists (use --force to recompute)\"); return 0\n\n t0 = time.time()\n gam = np.loadtxt(ZEROS_CSV, delimiter=\",\", skiprows=1, usecols=1)\n ell = np.log(T / (2 * np.pi))\n sqT = np.sqrt(T)\n in_Ip = (gam >= T - sqT) & (gam < 2 * T + sqT)\n zeros_Ip = gam[in_Ip]\n Np = len(zeros_Ip)\n print(f\"T={T:.0f} ell={ell:.4f} zeros in I'={Np}\", flush=True)\n\n rows = []\n for lam in LAMBDAS:\n t1 = time.time()\n L = lam * ell\n h = 2 * np.pi / L\n d = int(L * T / (2 * np.pi))\n alpha = T + h * np.arange(d)\n phi_hat, a = build_phi_hat(L, xi_max_needed=2 * T + sqT)\n Z = zeros_Ip[:, None] - alpha[None, :]\n V = np.real(phi_hat(Z))\n G = (V.T @ V) / (a * L**2)\n ev = eigvalsh(G)\n lam_max = float(ev[-1])\n # numerical rank + smallest positive eigenvalue\n noise = 1e-10 * lam_max\n pos = ev[ev > noise]\n rank_num = int(len(pos))\n lam_min_pos = float(pos[0]) if len(pos) else 0.0\n mean_pos = float(pos.mean()) if len(pos) else 0.0\n ratio_max = lam_min_pos / lam_max if lam_max else 0.0\n ratio_mean = lam_min_pos / mean_pos if mean_pos else 0.0\n rows.append({\n \"lambda\": lam, \"d\": d, \"N_primes_zeros\": Np,\n \"dim_deficit\": max(0, d - Np),\n \"rank_numeric\": rank_num,\n \"lambda_max\": f\"{lam_max:.4e}\",\n \"lambda_min_pos\": f\"{lam_min_pos:.4e}\",\n \"minpos_over_max\": f\"{ratio_max:.3e}\",\n \"minpos_over_mean\": f\"{ratio_mean:.3e}\",\n \"log10_minpos_over_mean\": f\"{np.log10(ratio_mean) if ratio_mean>0 else float('-inf'):.2f}\",\n \"pct01_eig\": f\"{float(np.percentile(ev, 1)):.3e}\",\n \"pct10_eig\": f\"{float(np.percentile(ev, 10)):.3e}\",\n \"pct50_eig\": f\"{float(np.percentile(ev, 50)):.3e}\",\n })\n print(f\"lam={lam}: d={d} rank={rank_num} lam_max={lam_max:.3e} \"\n f\"lam_min+={lam_min_pos:.3e} min+/mean={ratio_mean:.2e} \"\n f\"({time.time()-t1:.0f}s)\", flush=True)\n del G, V, Z\n\n DATA.mkdir(parents=True, exist_ok=True)\n with CSV.open(\"w\", encoding=\"utf-8\", newline=\"\") as f:\n f.write(\",\".join(rows[0].keys()) + \"\\n\")\n for r in rows:\n f.write(\",\".join(str(v) for v in r.values()) + \"\\n\")\n meta = {\n \"experiment\": \"E-006\",\n \"task\": \"3.1 / Q-3.4b (positivity horizon)\",\n \"description\": \"Eigenvalue floor of Gabor-truncated Weil form vs \"\n \"bandwidth lambda; conditioning of positivity \"\n \"certification (cf. Groskin B_T budget, Kim et al. \"\n \"superexponential decay)\",\n \"script\": \"research/numerics/scripts/E-006-positivity-horizon.py\",\n \"parameters\": {\"T\": T, \"lambdas\": list(LAMBDAS), \"window\": \"psi0\",\n \"zeros_source\": \"E-002\", \"precision\": \"float64\"},\n \"caveats\": [\"all zeros on-line => PSD by construction; the floor \"\n \"measures conditioning, not failure\",\n \"d > N' => dimensional rank deficiency (overcomplete \"\n \"basis), not form degeneracy\"],\n \"elapsed_seconds\": round(time.time() - t0, 1),\n \"timestamp_utc\": datetime.now(timezone.utc).isoformat(),\n \"row_count\": len(rows),\n }\n JSON.write_text(json.dumps(meta, indent=2), encoding=\"utf-8\")\n print(f\"wrote {CSV.name}, {JSON.name}\")\n return 0\n\n\nif __name__ == \"__main__\":\n raise SystemExit(main())\n"
}
result 2026-08-17 22:20:35Z → 2026-08-22 06:17:53Z
{
"type": "create",
"filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiArchimedean.lean",
"content": "/-\nNguyenRH1/LiArchimedean.lean \u2014 tier ii\u2032 sub-stage ii\u2032-3a, piece (A)\n(D-066 \u00a74): the archimedean coefficients of the (4.10) split.\n\nTarget (D-066): the Taylor coefficients of s \u21a6 logDeriv Gamma\u211d (1+s) at 0:\n\n (1/j!)\u00b7iteratedDeriv j (fun s => logDeriv Gamma\u211d (1+s)) 0 = (\u22121)^{j+1} a_{j+1},\n\ni.e. `iteratedDeriv j ... 0 = (\u22121)^{j+1}\u00b7j!\u00b7lagariasA (j+1)`.\n\nPart 1 (this file, complete): the Gamma\u211d logDeriv split\n logDeriv Gamma\u211d (1+s) = \u2212(log \u03c0)/2 + (1/2)\u00b7digamma((1+s)/2)\n(`logDeriv_Gamma\u211d_one_add`) and the j = 0 evaluation\n logDeriv Gamma\u211d 1 = \u2212(log 4\u03c0 + \u03b3)/2 = \u2212lagariasA1\n(`logDeriv_Gamma\u211d_one`) \u2014 via Mathlib's `Complex.digamma_one_half`.\n\nPart 2 (next): the digamma series from BohrMollerup's logGammaSeq and the\nj \u2265 1 polygamma values at 1/2, then the odd-m reindexing to lagariasA.\n\nArchive references: D-066 (route \u03b24, piece A), journal-019/020.\n-/\nimport Mathlib\nimport NguyenRH1.LiSkeleton\n\nopen Zeta23 Complex Filter Topology\nopen scoped Nat\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. The Gamma\u211d logDeriv split -/\n\n/-- The cpow factor as an exponential: \u03c0^(\u2212w/2) = exp(\u2212(log \u03c0)/2\u00b7w). -/\nlemma pi_cpow_neg_half_eq_exp (w : \u2102) :\n (\u2191Real.pi : \u2102) ^ (-w / 2) = Complex.exp (-(Real.log \u03c0 : \u2102) / 2 * w) := by\n rw [Complex.cpow_def_of_ne_zero (by exact_mod_cast Real.pi_ne_zero)]\n congr 1\n rw [\u2190 Complex.ofReal_log Real.pi_nonneg]\n ring\n\n/-- The Gamma\u211d logDeriv split: for (1+s)/2 off the poles of \u0393,\n logDeriv Gamma\u211d (1+s) = \u2212(log \u03c0)/2 + (1/2)\u00b7\u03c8((1+s)/2). -/\nlemma logDeriv_Gamma\u211d_one_add {s : \u2102}\n (hs : Complex.Gamma ((1 + s) / 2) \u2260 0)\n (hs2 : \u2200 m : \u2115, ((1 + s) / 2) \u2260 -m) :\n logDeriv Complex.Gamma\u211d (1 + s) =\n -(Real.log \u03c0 : \u2102) / 2 + (1 / 2) * Complex.digamma ((1 + s) / 2) := by\n have hfun : Complex.Gamma\u211d = fun w : \u2102 =>\n Complex.exp (-(Real.log \u03c0 : \u2102) / 2 * w) * Complex.Gamma (w / 2) := by\n funext w\n show Complex.Gamma\u211d w = _\n rw [Complex.Gamma\u211d_def]\n congr 1\n exact pi_cpow_neg_half_eq_exp w\n rw [hfun, logDeriv_apply]\n have hdif1 : DifferentiableAt \u2102 (fun w : \u2102 => Complex.exp (-(Real.log \u03c0 : \u2102) / 2 * w))\n (1 + s) := by\n have h1 : DifferentiableAt \u2102 (fun w : \u2102 => -(Real.log \u03c0 : \u2102) / 2 * w) (1 + s) :=\n differentiableAt_const_mul _\n exact Complex.differentiableAt_exp.comp (1 + s) h1\n have hdif2 : DifferentiableAt \u2102 (fun w : \u2102 => Complex.Gamma (w / 2)) (1 + s) := by\n have h2 : DifferentiableAt \u2102 (fun w : \u2102 => w / 2) (1 + s) :=\n differentiableAt_id.div_const 2\n exact (Complex.differentiableAt_Gamma _ hs2).comp (1 + s) h2\n rw [logDeriv_mul (f := fun w : \u2102 => Complex.exp (-(Real.log \u03c0 : \u2102) / 2 * w))\n (g := fun w => Complex.Gamma (w / 2)) (1 + s) (Complex.exp_ne_zero _) hs hdif1 hdif2]\n have h1 : logDeriv (fun w : \u2102 => Complex.exp (-(Real.log \u03c0 : \u2102) / 2 * w)) (1 + s) =\n -(Real.log \u03c0 : \u2102) / 2 := by\n rw [logDeriv_apply]\n have hd : deriv (fun w : \u2102 => Complex.exp (-(Real.log \u03c0 : \u2102) / 2 * w)) (1 + s) =\n Complex.exp (-(Real.log \u03c0 : \u2102) / 2 * (1 + s)) * (-(Real.log \u03c0 : \u2102) / 2) := by\n have hh1 : HasDerivAt (fun w : \u2102 => -(Real.log \u03c0 : \u2102) / 2 * w)\n (-(Real.log \u03c0 : \u2102) / 2) (1 + s) := by\n simpa using (hasDerivAt_id (1 + s)).const_mul (-(Real.log \u03c0 : \u2102) / 2)\n have hh2 := (Complex.hasDerivAt_exp (-(Real.log \u03c0 : \u2102) / 2 * (1 + s))).comp (1 + s) hh1\n have heq : (Complex.exp \u2218 fun w : \u2102 => -(Real.log \u03c0 : \u2102) / 2 * w) =\n fun w : \u2102 => Complex.exp (-(Real.log \u03c0 : \u2102) / 2 * w) := rfl\n rw [heq] at hh2\n exact hh2.deriv\n rw [hd]\n field_simp [Complex.exp_ne_zero (-(Real.log \u03c0 : \u2102) / 2 * (1 + s))]\n have h2 : logDeriv (fun w : \u2102 => Complex.Gamma (w / 2)) (1 + s) =\n (1 / 2) * Complex.digamma ((1 + s) / 2) := by\n rw [logDeriv_apply]\n have hd : deriv (fun w : \u2102 => Complex.Gamma (w / 2)) (1 + s) =\n deriv Complex.Gamma ((1 + s) / 2) * (1 / 2) := by\n have hh1 : HasDerivAt (fun w : \u2102 => w / 2) (1 / 2) (1 + s) := by\n simpa using (hasDerivAt_id (1 + s)).div_const (2 : \u2102)\n have hh2 := ((Complex.differentiableAt_Gamma _ hs2).hasDerivAt).comp (1 + s) hh1\n have heq : (Complex.Gamma \u2218 fun w : \u2102 => w / 2) = fun w : \u2102 => Complex.Gamma (w / 2) := rfl\n rw [heq] at hh2\n exact hh2.deriv\n rw [hd, Complex.digamma_def, logDeriv_apply]\n field_simp [hs]\n ring\n rw [h1, h2]\n\n/-! ## 2. The j = 0 evaluation: \u03c4\u2080 = \u2212a\u2081 -/\n\n/-- log(4\u03c0) = 2\u00b7log 2 + log \u03c0. -/\nlemma log_four_pi : Real.log (4 * Real.pi) = 2 * Real.log 2 + Real.log Real.pi := by\n rw [Real.log_mul (by norm_num) (by positivity)]\n congr 1\n rw [show (4 : \u211d) = 2 ^ 2 from by norm_num, Real.log_pow]\n ring\n\n/-- **\u03c4\u2080** (D-066 \u00a74, j = 0): logDeriv Gamma\u211d 1 = \u2212(log 4\u03c0 + \u03b3)/2 = \u2212a\u2081. -/\ntheorem logDeriv_Gamma\u211d_one :\n logDeriv Complex.Gamma\u211d 1 = -(lagariasA1 : \u2102) := by\n have hs : Complex.Gamma ((1 + (0 : \u2102)) / 2) \u2260 0 := by\n have e : (1 + (0 : \u2102)) / 2 = 1 / 2 := by ring\n rw [e, Complex.Gamma_one_half_eq]\n intro hz\n rw [Complex.cpow_eq_zero_iff (by norm_num : ((1 : \u2102) / 2) \u2260 0)] at hz\n exact Real.pi_ne_zero (by exact_mod_cast hz.1)\n have hs2 : \u2200 m : \u2115, ((1 + (0 : \u2102)) / 2) \u2260 -m := by\n intro m hm\n have e : (1 + (0 : \u2102)) / 2 = 1 / 2 := by ring\n rw [e] at hm\n have hre : ((1 : \u2102) / 2).re = (-(m : \u2102)).re := by rw [hm]\n simp at hre\n have hm0 : (0 : \u211d) \u2264 (m : \u211d) := Nat.cast_nonneg m\n linarith\n have h := logDeriv_Gamma\u211d_one_add (s := 0) hs hs2\n rw [add_zero] at h\n rw [h]\n have e2 : (1 : \u2102) / 2 = ((1 / 2 : \u211d) : \u2102) := by push_cast; ring\n rw [e2, Complex.digamma_one_half]\n rw [lagariasA1, log_four_pi]\n push_cast\n ring\n",
"structuredPatch": [],
"originalFile": null
}
raw content_json (database row)
[{"type":"thinking","thinking":"Committed (f7af545). Now build E-006: positivity horizon numerics. Design per D-014 §4:\n\n- Gabor-truncated Weil form G̃ vs bandwidth λ ∈ {0.5, 1.0, 1.5, 2.0} at T = 2000, using E-002 zeros.\n- Construction: same as E-003 but with L_λ = λ·log(T/2π)... careful: in E-003, L = log(T/2π) ties support to X = T/2π (bandwidth 1). For bandwidth λ: test function support L_λ = λ·ℓ where ℓ = log(T/2π). Grid: critical density for the window: h = 2π/L_λ (per Lemma 2.1 no-aliasing), grid points α_k = T + k·h covering [T, 2T): d_λ = ⌊L_λ T/2π⌋ = λ·1834. At λ=2: d = 3668, matrix 3668² — fine.\n- a = ‖ϕ‖²/L_λ.\n- G̃_λ = (aL_λ²)⁻¹ Σ_{γ∈I′} v vᵀ, v = ϕ̂_λ(γ − α_k).\n- Measure: full eigenvalue spectrum, esp. λ_min; also n₊/d; compare tr/d etc.\n- Note: with all zeros on-line, G̃ ⪰ 0 always (PSD by construction up to tail). λ_min measures how close to singular.\n- The Groskin budget comparison: B_T ~ (2N+1)ρ log T/(π²T) — his truncation parameters (prime cutoff c, band N, archimedean cutoff T) don't map 1-1 onto ours; I'll compute an analogous scale: our \"tail\" Ẽ norm bound was T^{−1/2} (Prop 4.3). Compare λ_min with T^{−1/2} scale.\n- ALSO the interesting decay: λ_min vs λ — fit exponential/superexponential.\n\nImplementation: reuse E-003's build_phi_hat (mollified window, xi_max_needed = 2T+√T). For λ = 2: L_λ = 2ℓ ≈ 11.5; M_needed = L_λ·(2T+√T)/π ≈ 11.5·4045/π ≈ 14800 → M = 16384; pad 8 → 131072 FFT — fine. d = 3668, zeros in I′ = 2044; V = 2044×3668 (60MB); V.T@V: 2044·3668² ≈ 2.7e10 — a few seconds; eigvalsh 3668² — ~20-40s. Total for 4 λ values: a couple of minutes. Good.\n\nλ_min interpretation caveat: at λ=2, d=3668 > N(I′)=2044 — rank ≤ 2044 < d, so λ_min = 0 automatically (dimension deficit)! Hmm — that pollutes the horizon measurement: the matrix is singular for dimensional reasons when d > #zeros. At λ ≤ 1.1·...: d = λ·1834 vs zeros in I′ = 2044: crossover at λ ≈ 1.11. Above that, G̃ is structurally singular (more rows than vectors) — λ_min ≈ 0 (to numerical precision) regardless of math. The meaningful floor: the smallest POSITIVE eigenvalue (the (d−N′)-th smallest). Hmm — but the paper's truncation is at d ≈ N; the positivity question is about the form on the test-function space — the Gabor vectors at oversampled grid are linearly dependent... The Weil form on the span: the matrix represents the form in an overcomplete basis; rank deficiency = basis redundancy, not form degeneracy. For the horizon measurement I should look at the smallest POSITIVE eigenvalue relative to the bulk scale (e.g. λ_min₊/λ_max or λ_min₊/mean). Let me record: for each λ: d, N′, rank, λ_min₊ (smallest eigenvalue above a numerical-noise threshold), ratio λ_min₊/λ_mean, and log10(λ_min₊/λ_mean) — the \"conditioning\" of the truncation. Decay of that ratio vs λ is the horizon/complexity measure.\n\nNoise threshold: entries accurate to ~1e-5 relative (frame self-test) — eigenvalue noise floor ~1e-4·λ_max·... use threshold 1e-8·λ_max·d? Estimate empirically: look at eigenvalue gap structure. Simple: report eigenvalues at percentiles and the count below several thresholds (1e-4, 1e-6, 1e-8 relative). Data will speak.\n\nWrite E-006 script.","signature":""},{"type":"text","text":"Track C setup committed (`f7af545`). Now building **E-006 — the positivity horizon experiment**."},{"type":"tool_use","id":"Write_260","name":"Write","input":{"file_path":"D:\\Python\\Quantum\\research\\numerics\\scripts\\E-006-positivity-horizon.py","content":"\"\"\"E-006 — Task 3.1 / Q-3.4b: positivity horizon of the truncated Weil form.\n\nFor bandwidth lambda in {0.5, 1, 1.5, 2} build the Gabor-truncated Weil\nform G_lambda on [T, 2T), T = 2000 (construction of E-003/D-002 §3 with\nL_lambda = lambda * log(T/2pi), grid at critical density h = 2pi/L_lambda):\n\n phi_lambda(u) = chi(L/2+u) chi(L/2-u) * 1 (flat window, L = L_lambda)\n G = (a L^2)^-1 sum_{gamma in I'} v_gamma v_gamma^T, a = ||phi||^2/L\n\nAll zeros here are on the line, so G is PSD by construction; the\ninformative quantity is HOW CLOSE to singular the truncation gets as the\nsupport grows — the conditioning floor. NOTE: when d = lambda*d_1 exceeds\nthe number N' of zeros in I' (crossover lambda ~ 1.11 at this T), the\nmatrix is rank-deficient for dimensional reasons (overcomplete Gabor\nbasis); the meaningful floor is then the smallest POSITIVE eigenvalue.\n\nMetrics per lambda: d, N', numerical rank, eigenvalue percentiles,\nsmallest positive eigenvalue lambda_min+ and the ratios\nlambda_min+/lambda_max, lambda_min+/mean(eig>0); log10 of the ratio =\nconditioning exponent. A superexponential decay of the floor (cf. Kim et\nal. 2026 for Suzuki's operator) would be a complexity wall for positivity\ncertification (Groskin's B_T budget: resolving lambda_min needs precision\n1/lambda_min).\n\nOutputs: research/numerics/data/E-006-positivity-horizon.csv (+ .json)\n\"\"\"\nimport json\nimport sys\nimport time\nfrom datetime import datetime, timezone\nfrom pathlib import Path\n\nimport numpy as np\nfrom scipy.interpolate import CubicSpline\nfrom scipy.linalg import eigvalsh\n\nREPO = Path(__file__).resolve().parents[3]\nDATA = REPO / \"research\" / \"numerics\" / \"data\"\nZEROS_CSV = DATA / \"E-002-zeros-first-10000.csv\"\nCSV = DATA / \"E-006-positivity-horizon.csv\"\nJSON = DATA / \"E-006-positivity-horizon.json\"\n\nT = 2000.0\nLAMBDAS = (0.5, 1.0, 1.5, 2.0)\n\n\ndef chi(u: np.ndarray) -> np.ndarray:\n out = np.zeros_like(u)\n mid = (u > 0) & (u < 1)\n e1 = np.exp(-1.0 / u[mid])\n e2 = np.exp(-1.0 / (1.0 - u[mid]))\n out[mid] = e1 / (e1 + e2)\n out[u >= 1] = 1.0\n return out\n\n\ndef build_phi_hat(L: float, xi_max_needed: float, pad: int = 8, M0: int = 4096):\n M = int(2 ** np.ceil(np.log2(max(M0, L * xi_max_needed / np.pi))))\n du = L / M\n u = -L / 2 + du * np.arange(M)\n phi = chi(L / 2 + u) * chi(L / 2 - u) # flat window psi0\n a = np.sum(phi**2) * du / L\n full = np.zeros(pad * M)\n full[: M // 2] = phi[M // 2:]\n full[-M // 2:] = phi[: M // 2]\n F = np.fft.fft(full) * du\n xi = 2 * np.pi * np.fft.fftfreq(pad * M, d=du)\n order = np.argsort(xi)\n return CubicSpline(xi[order], F[order]), a\n\n\ndef main() -> int:\n if not ZEROS_CSV.exists():\n print(\"E-002 zeros not found\"); return 1\n if CSV.exists() and \"--force\" not in sys.argv:\n print(f\"cached: {CSV} exists (use --force to recompute)\"); return 0\n\n t0 = time.time()\n gam = np.loadtxt(ZEROS_CSV, delimiter=\",\", skiprows=1, usecols=1)\n ell = np.log(T / (2 * np.pi))\n sqT = np.sqrt(T)\n in_Ip = (gam >= T - sqT) & (gam < 2 * T + sqT)\n zeros_Ip = gam[in_Ip]\n Np = len(zeros_Ip)\n print(f\"T={T:.0f} ell={ell:.4f} zeros in I'={Np}\", flush=True)\n\n rows = []\n for lam in LAMBDAS:\n t1 = time.time()\n L = lam * ell\n h = 2 * np.pi / L\n d = int(L * T / (2 * np.pi))\n alpha = T + h * np.arange(d)\n phi_hat, a = build_phi_hat(L, xi_max_needed=2 * T + sqT)\n Z = zeros_Ip[:, None] - alpha[None, :]\n V = np.real(phi_hat(Z))\n G = (V.T @ V) / (a * L**2)\n ev = eigvalsh(G)\n lam_max = float(ev[-1])\n # numerical rank + smallest positive eigenvalue\n noise = 1e-10 * lam_max\n pos = ev[ev > noise]\n rank_num = int(len(pos))\n lam_min_pos = float(pos[0]) if len(pos) else 0.0\n mean_pos = float(pos.mean()) if len(pos) else 0.0\n ratio_max = lam_min_pos / lam_max if lam_max else 0.0\n ratio_mean = lam_min_pos / mean_pos if mean_pos else 0.0\n rows.append({\n \"lambda\": lam, \"d\": d, \"N_primes_zeros\": Np,\n \"dim_deficit\": max(0, d - Np),\n \"rank_numeric\": rank_num,\n \"lambda_max\": f\"{lam_max:.4e}\",\n \"lambda_min_pos\": f\"{lam_min_pos:.4e}\",\n \"minpos_over_max\": f\"{ratio_max:.3e}\",\n \"minpos_over_mean\": f\"{ratio_mean:.3e}\",\n \"log10_minpos_over_mean\": f\"{np.log10(ratio_mean) if ratio_mean>0 else float('-inf'):.2f}\",\n \"pct01_eig\": f\"{float(np.percentile(ev, 1)):.3e}\",\n \"pct10_eig\": f\"{float(np.percentile(ev, 10)):.3e}\",\n \"pct50_eig\": f\"{float(np.percentile(ev, 50)):.3e}\",\n })\n print(f\"lam={lam}: d={d} rank={rank_num} lam_max={lam_max:.3e} \"\n f\"lam_min+={lam_min_pos:.3e} min+/mean={ratio_mean:.2e} \"\n f\"({time.time()-t1:.0f}s)\", flush=True)\n del G, V, Z\n\n DATA.mkdir(parents=True, exist_ok=True)\n with CSV.open(\"w\", encoding=\"utf-8\", newline=\"\") as f:\n f.write(\",\".join(rows[0].keys()) + \"\\n\")\n for r in rows:\n f.write(\",\".join(str(v) for v in r.values()) + \"\\n\")\n meta = {\n \"experiment\": \"E-006\",\n \"task\": \"3.1 / Q-3.4b (positivity horizon)\",\n \"description\": \"Eigenvalue floor of Gabor-truncated Weil form vs \"\n \"bandwidth lambda; conditioning of positivity \"\n \"certification (cf. Groskin B_T budget, Kim et al. \"\n \"superexponential decay)\",\n \"script\": \"research/numerics/scripts/E-006-positivity-horizon.py\",\n \"parameters\": {\"T\": T, \"lambdas\": list(LAMBDAS), \"window\": \"psi0\",\n \"zeros_source\": \"E-002\", \"precision\": \"float64\"},\n \"caveats\": [\"all zeros on-line => PSD by construction; the floor \"\n \"measures conditioning, not failure\",\n \"d > N' => dimensional rank deficiency (overcomplete \"\n \"basis), not form degeneracy\"],\n \"elapsed_seconds\": round(time.time() - t0, 1),\n \"timestamp_utc\": datetime.now(timezone.utc).isoformat(),\n \"row_count\": len(rows),\n }\n JSON.write_text(json.dumps(meta, indent=2), encoding=\"utf-8\")\n print(f\"wrote {CSV.name}, {JSON.name}\")\n return 0\n\n\nif __name__ == \"__main__\":\n raise SystemExit(main())\n"},"extra_content":null}]