Remainder bound in the settled range: Phi(zeta) <= -1/2 log(1 - 2 f2 zeta^2) for 0 <= zeta < (4 f2)^{-1/2} = pi sqrt(3)

Status: proved — a complete structured proof.

Area: Theorem A: exact recovery error of the free fermion · Card type: result · Knowledge-base id: rrr-bound-small-zeta

Statement

For the zero-collar compression of the free chiral fermion (one chiral component; Phi as in rate_of_remainder.tex l. 66-67), Phi(zeta) <= -1/2 log(1 - 2 f2 zeta^2) for 0 <= zeta < (4 f2)^{-1/2} = pi sqrt(3) = 5.4414, f2 = 1/(12 pi^2) (rigor/rate_of_remainder.tex prop:rrr, restricted to the range that its Correction C3 settles). In this range the h' of prop:rrr <1>4 with 4 f2^K zeta^2 < 1 still have infimum f2^K = f2, because inf f2^K = f2 < 1/(4 zeta^2). For each of them U_zeta = e^{zeta K} has ||G_zeta||_2 <= zeta ||[P_-, K]||_2 = (4 f2^K zeta^2)^{1/2} < 1 (lem:groupbound <1>2, <1>3). So both off-diagonal blocks of U_zeta have norm < 1, being blocks of [P_+, U_zeta] = -U_zeta G_zeta, and P_+ U_zeta P_+ is invertible on P_+ H (PA Thm 4.1 <1>1), hence of index zero. Therefore the two blocks have the same singular values (C3, l. 1034-1040), which gives lem:groupbound's ||V_zeta||_2^2 <= 2 f2^K zeta^2 and PA Thm 4.1's hypothesis ||P_+ U_zeta P_-|| < 1 (C3 (ii), l. 1069-1075). The printed range up to (2 f2)^{-1/2} = pi sqrt(6) is the card rate-of-remainder, which rests beyond pi sqrt(3) on group-index-zero-large-s. Split off rate-of-remainder on 2026-09-24 so that cards using the bound only at small zeta do not inherit the index gap.

How to verify

rigor/rate_of_remainder.tex prop:rrr (and its <1>3, <1>4), lem:groupbound <1>2, Correction C3 'Status of the uses' (ii) (l. 1069-1075; mechanism l. 1034-1040); PA = rigor/uhlmann_upper_bound.tex Thm 4.1 <1>1. Range: (4 f2)^{-1/2} = pi sqrt(3) for f2 = 1/(12 pi^2).

Evidence

• rigor/rate_of_remainder.tex — document, at prop:rrr
• rigor/rate_of_remainder.tex — document, at lem:groupbound
• rigor/rate_of_remainder.tex — document, at corr0924:C3

Related claims

• Remainder of Theorem A: global upper bound Phi <= -(1/2) log(1 - 2 f2 zeta^2); c3 <= 0 as a limsup; no positive log^-2 term — proved
• Index zero for e^{sK} beyond ||G_s||_2 < 1: for a unitary group e^{sK} with [P_-, K] Hilbert-Schmidt the two off-diagonal blocks have the same singular values also where |s| ||[P_-, K]||_2 >= 1 (open; no document contains an argument) — conjectural
• Weak link: Phi(zeta) <= 0.0085 zeta^2 on (0, 1] (rigorous on (0, 0.8868], numerical on [0.8868, 1]) — numerical

Review

Review record: passed 2026-09-24 by REF-CARD-ROR.

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