Ultraviolet tail bound for the windowed fidelity (shape proved; explicit constants 0.173, 0.88 rest on numerical inputs)
Status: proved — a complete structured proof.
Area: Theorem A: exact recovery error of the free fermion · Card type: theorem · Knowledge-base id: tail-bound
Statement
For the free chiral fermion, with Phi_W the window (sub-compressed) recovery error at modular cutoff kappa_c (rigor/tail_bound.tex). (a) PROVED, the shape, as thm:main now states and proves it (corrected 2026-09-24, tail_bound.tex Correction C1): 0 <= Phi - Phi_W <= Phi_d + Y/(1-Y), with Phi_d := T/(2(1-T)), y = 2 e^{2 Phi_d} sqrt(Phi Phi_d) and Y := e^{Phi_W} y <= e^{Phi} y, provided T < 1 and Y < 1 (the hypotheses of thm:main, tail_bound.tex:458-470). Both hold on the admissible region of cor:rate with the inputs of (b), where T <= 1.75 zeta^2/kappa_c^2 <= 0.0175 and Y <= 0.02; the document checks both in cor:rate <1>2 (l. 524, added 2026-09-24, Correction C3). Until 2026-09-24 the document printed this bound, and its hypothesis, with y in place of Y; that form does not follow from the proof's ingredients (DOCUMENT ERROR note on step <1>5). The Y-form is what it now states and proves (Thm 5.1, thm:main, eq:Psi: Bures-angle triangle inequality through the product state rho'' and the purification lower bound lem:purif), with T = 5 tau + nu <= 2 zeta^2/(3 kappa_c^2) + 10 C_2 zeta^2/kappa_c^3 + (12 + 10 C_1 zeta (1 + kappa_c)) e^{-kappa_c}, where C_2 = 4 pi A_3, C_1 = A_1/(4 pi^2) and A_1, A_3 are finite suprema of explicit one-dimensional integrals of the closed-form occupation (Thm 4.2, thm:tau), and |Sigma - zeta^2/(15 kappa_c^2)| <= C_2 zeta^2 kappa_c^-3 + C_1 zeta (1 + kappa_c) e^{-kappa_c}; hence, whenever Phi <= f zeta^2, Phi - Phi_W <= C zeta^2/kappa_c + C' zeta^2/kappa_c^2 on kappa_c >= max{10, 2 log(1/zeta) + 2 log(1 + kappa_c) + 3} with finite C, C'. (b) EXPLICIT CONSTANTS, via numerical inputs: A_1 <= 2.0 and A_3 <= 0.0374, i.e. C_1 <= 0.051 and C_2 <= 0.47 (card tail-constants-numerical: uncertified double-precision and finite-difference evaluations; A_3 <= 0.036 and C_2 <= 0.46 until 2026-09-24, corrected in tail_bound.tex Correction C10, since the supremum A_3 is the zeta -> 0 limit, about 0.0372), and f = 0.0085 (card phi-below-0085-zeta2-numerical) give 0 <= Phi - Phi_W <= 0.173 zeta^2/kappa_c + 0.88 zeta^2/kappa_c^2 (Cor. 5.2, cor:rate, eq:final). eq:final holds given these inputs, and the document now says so: cor:rate states that eq:final rests on these numerical inputs and on a double-precision evaluation of the corrected chain over the admissible region, not on an analytic argument (l. 510-512, 527), and its step <1>1 is repaired, with s(10) = 1.707 <= 1.75 (corrected 2026-09-24, Corrections C2, C3 and C10; until 2026-09-24 the printed proof used a false step at l. 521 and obtained eq:final by dropping the factors 1 + O(zeta^2), DOCUMENT ERROR note of 2026-09-23). With eq:taunu's T (C_2 <= 0.47) the corrected chain of display (a) (Y in place of y) stays <= 0.9841 of the claimed bound on the admissible region, with supremum 0.98405 at the corner (zeta, kappa_c) = (11 e^{-3.5}, 10) = (0.33217, 10), where kappa_c = kappa_dagger = 10 (refb10_tail_sup_c2.py; 0.98019 with C_2 <= 0.46 before 2026-09-24, refb10_tail_sup.py). The grid of tailcheck_ext.py and refb6_tailcheck_corrected.py (zeta step 5e-4) reaches only zeta = 0.3325 there and gives 0.98365 (refb10_tail_sup_c2.py, grid scan; 0.97979 with C_2 <= 0.46, refb6_tailcheck_corrected.py). The pre-correction chain (y in place of Y, as printed until 2026-09-24) gives 0.98343 at the corner (refb10_tail_sup_c2.py); with C_2 <= 0.46 it gave 0.97957 at the corner (refb10_tail_sup.py) and 0.97917 on the grid (tailcheck.py, tailcheck_ext.py). The input f = 0.0085 could be replaced by the proved f <= 0.008516 of rate-of-remainder prop:rrr (2 sqrt(0.875 x 0.008516) = 0.1726 <= 0.173; corrected chain <= 0.9847 of the bound, 0.98467 at the corner, refb10_tail_sup_c2.py; 0.98080 with C_2 <= 0.46). tail_bound.tex now cites prop:rrr, in Correction C3 (l. 935-940, 964-967): as the rigorous basis of f = 0.0085 on (0, 0.8868], the rest of (0, 1] being numerical as on card phi-below-0085-zeta2-numerical, and as a possible replacement of f; cor:rate itself still takes f = 0.0085 (l. 510). Until 2026-09-24 tail_bound.tex did not cite prop:rrr. Supersedes the heuristic tail of Note 5 Prop. 4.1; the zeta^2 log^-2 remainder claimed there was refuted (card rate-of-remainder).
How to verify
rigor/tail_bound.tex Thm 5.1 (thm:main, l. 458-500) for (a); Thm 4.2 (thm:tau, l. 314-340) for T and Sigma; Cor. 5.2 (cor:rate, l. 502-529) for eq:final; the corrections of 2026-09-24 are in its section 'Corrections of 2026-09-24' (l. 849-1112): C1 thm:main, C2 and C3 cor:rate, C4 the status of the constants, C10 A_3 and C_2. A_1 <= 2.0 is evaluated by numerics/pt_checks.py, and A_3 <= 0.0374 by numerics/kb-checks-2026-09-24/a3_refined.py, which evaluates the supremum, the zeta -> 0 limit, that the finite-zeta samples of rigor/pt_tailconst.py miss (A_3 <= 0.036 until 2026-09-24, Correction C10); both in double precision, not certified (card tail-constants-numerical) -- NOT by numerics/certified/cert_tail*.py, which evaluate a different bound (Phi - Phi_W <= Phi_22 + Phi_off, certified_numerics.tex Thm 3.2, thm:nocross). eq:final given the inputs, with C_2 <= 0.47: from the cft_cmi root run python3 numerics/kb-checks-2026-09-24/refb10_tail_sup_c2.py (standard library, about 20 s) and compare with refb10_tail_sup_c2.out. It is refb10_tail_sup.py with 10 C_2 = 4.7 in place of 4.6 in T, plus a scan of the corrected chain over the admissible grid of tailcheck_ext.py (5.25e6 admissible points, zeta down to 1e-8, kappa_c up to 200, f = 0.0085 and 0.008516). The earlier scripts are in numerics/kb-checks-2026-09-23/ (tailcheck.py is REF-DEP-CFT-B2's): tailcheck.py, tailcheck_ext.py, refb6_tailcheck_corrected.py and refb10_tail_sup.py hard-code 4.6 (C_2 <= 0.46), so their ratios are the values before 2026-09-24; refb6_psi_check3.py (the saturating example of Correction C1) does not involve C_2. Grid maxima with C_2 <= 0.47 (zeta step 5e-4, first point 0.3325 at kappa_c = 10): corrected chain of display (a) 0.98365 (f = 0.0085) and 0.98427 (f = 0.008516), both at (0.3325, 10), where the pre-correction chain (y in place of Y) gives 0.98303 and 0.98365 (refb10_tail_sup_c2.py). With C_2 <= 0.46 (before 2026-09-24): pre-correction chain 0.97917 and 0.97979 (tailcheck.py, tailcheck_ext.py), corrected chain 0.97979 and 0.98041 (refb6_tailcheck_corrected.py). The supremum over the admissible region is at the corner (11 e^{-3.5}, 10) = (0.33217, 10): corrected 0.98405 (f = 0.0085) and 0.98467 (f = 0.008516), pre-correction 0.98343 and 0.98405, T kappa_c^2/zeta^2 = 1.7071 (refb10_tail_sup_c2.py); max T kappa_c^2/zeta^2 = 1.707 at the corner (1.706 on the grid) <= 1.75, in agreement with s(10) = 2/3 + 0.47 + 0.494 + 0.077 = 1.707 of cor:rate <1>1 (l. 522). With C_2 <= 0.46 (before 2026-09-24): corrected 0.98019 and 0.98080, pre-correction 0.97957 and 0.98019, T kappa_c^2/zeta^2 = 1.697 at the corner (1.696 on the grid) (refb10_tail_sup.py).
Evidence
- rigor/tail_bound.tex — document, at
cor:rate - rigor/tail_bound.tex — document, at
thm:main - rigor/tail_bound.tex — document, at
thm:tau - numerics/pt_checks.py — numerics
- rigor/pt_tailconst.py — numerics
- numerics/kb-checks-2026-09-23/tailcheck.py — numerics
- numerics/kb-checks-2026-09-23/tailcheck.out — numerics
- numerics/kb-checks-2026-09-23/tailcheck_ext.py — numerics
- numerics/kb-checks-2026-09-23/tailcheck_ext.out — numerics
- numerics/kb-checks-2026-09-23/refb6_psi_check3.py — numerics
- numerics/kb-checks-2026-09-23/refb6_psi_check3.out — numerics
- numerics/kb-checks-2026-09-23/refb6_tailcheck_corrected.py — numerics
- numerics/kb-checks-2026-09-23/refb6_tailcheck_corrected.out — numerics
- numerics/kb-checks-2026-09-23/refb10_tail_sup.py — numerics
- numerics/kb-checks-2026-09-23/refb10_tail_sup.out — numerics
- numerics/kb-checks-2026-09-24/refb10_tail_sup_c2.py — numerics
- numerics/kb-checks-2026-09-24/refb10_tail_sup_c2.out — numerics
Related claims
None recorded.
Review
Review record: passed 2026-09-24 by REF-CARD-TAIL.
The referee's report and the card's event log stay in the private knowledge base; only the verdict, the date and the referee are published here.
Documentation map · All claims by area · What is open · Symbols · Definitions