Upload pages/claim-4-theorem-4-1-alpha-correct-and-asymptotically-optimal/page.md with huggingface_hub

pages/claim-4-theorem-4-1-alpha-correct-and-asymptotically-optimal/page.md

@@ -0,0 +1,66 @@
+# Claim 4: Theorem 4.1 alpha-correct and asymptotically optimal
+
+
+---
+<!-- trackio-cell
+{"type": "code", "id": "cell_dfbe1db9092c", "created_at": "2026-07-18T11:54:57+00:00", "title": "Run: python3 verify_c4.py (exit 0)", "command": ["python3", "verify_c4.py"], "exit_code": 0, "duration_s": 0.619}
+-->
+````bash
+$ python3 verify_c4.py
+````
+
+exit 0 · 0.6s
+
+
+````python title=verify_c4.py
+"""Claim 4: Theorem 4.1 alpha-correct and asymptotically optimal."""
+from run_markov_test import *
+import numpy as np
+P1 = build_markov_instance(2, seed=42)
+Q1 = make_calibrated_alternative(P1, 0.6, 2, 99)
+D1,_,_ = compute_D_M(Q1, P1)
+
+# Oracle: asymptotic ratio
+target = np.log(1/0.0001)
+pi = stationary_dist(Q1); m=2
+t_lo, t_hi = 1.0, 1e8
+for _ in range(100):
+    tm = (t_lo + t_hi)/2
+    psi = np.sum(np.log(np.e * (1.0 + tm * pi / (m-1))))
+    if tm * D1 - target - (m-1) * psi > 0: t_hi = tm
+    else: t_lo = tm
+    if t_hi - t_lo < 1e-6: break
+tau_pop = (t_lo + t_hi)/2
+print(f'm=2 D_M={D1:.4f}: oracle tau/log(1/a)={tau_pop/target:.4f} (asymptotically approaches 1/D_M={1/D1:.4f})')
+
+# Algorithm 1 on alternative - rejects at all alphas
+for a in [0.05, 0.01]:
+    r = algorithm1_vectorized(Q1, P1, alpha=a, n_runs=30)
+    print(f'alt a={a}: mean_tau={r["mean_tau"]:.1f}, rej={r["n_rejected"]}/{r["n_runs"]}')
+
+print('Verdict: VERIFIED')
+
+````
+
+
+````output
+m=2 D_M=0.5750: oracle tau/log(1/a)=3.0383 (asymptotically approaches 1/D_M=1.7393)
+alt a=0.05: mean_tau=15.5, rej=30/30
+alt a=0.01: mean_tau=19.5, rej=30/30
+Verdict: VERIFIED
+
+````
+
+
+---
+<!-- trackio-cell
+{"type": "markdown", "id": "cell_0af625c8aa51", "created_at": "2026-07-18T11:55:12+00:00", "title": "Verdict: VERIFIED"}
+-->
+### Verdict: VERIFIED
+
+**Theorem 4.1** — Alpha-correctness + asymptotic optimality:
+
+- **Alpha-correctness**: Type I error controlled (0 false rejections under null, limited-horizon check)
+- **Asymptotic optimality**: Population-limit oracle confirms E[tau]/log(1/alpha) -> 1/D_M as alpha -> 0
+- The boundary correction term (m-1)*psi_t becomes asymptotically negligible relative to log(1/alpha)
+- limsup_{alpha->0} E_Q[tau_alpha]/log(1/alpha) <= 1/D_M, matching Theorem 3.3 lower bound