Type-III sequential recovery bound: Bures distances add along a chain of von Neumann inclusions (chordal and second-order forms, no Hypothesis (U))
Status: proved — a complete structured proof. Conditional. The statement is not unconditional: it rests on U, quoted below. Read the badge only together with them.
Area: Lattice, thermal, massive and gapped geometries (O7, O9, O10) · Card type: theorem · Knowledge-base id: sequential-recovery-bound-type-iii
Statement
Let omega be a normal state on a von Neumann algebra M, N_1 subset N_2 subset ... subset N_m subset M von Neumann subalgebras with the same unit, R_k: N_{k+1} -> N_k normal unital 2-positive (Heisenberg-picture) recovery maps, R = R_1 o ... o R_{m-1}. CHORDAL FORM (Thm 12.6, thm:w6chord), no Hypothesis (U): with d_B = sqrt(2 - 2F), d_B(omega|N_m, omega|N_1 o R) <= sum_k d_B(omega|N_{k+1}, omega|N_k o R_k). Proof: telescoping through the states mu_j = omega|N_{m-j} o R_{m-j} o S_j, S_j = R_{m-j+1} o ... o R_{m-1} (steps <1>1-<1>3 of Thm 12.5, which do not use (U)), monotonicity of F under the channel S_j (Lemma 12.3, from Choi's inequality T(a^{-1}) >= T(a)^{-1} for unital 2-positive T, Lemma 12.2, via the Schur complement, and Alberti-Uhlmann 2002 Thm 2(1), p. 6, and Cor 2(5), p. 8), and the triangle inequality of d_B (Alberti-Uhlmann 2002 Prop. 1(1), p. 3, stated there without proof and attributed to Bures 1969, which is NOT OBTAINED). SECOND-ORDER FORM (Cor 12.7(2), cor:w6-second), no (U): with Phi_tot = -log F(omega|N_m, omega|N_1 o R) and Phi_k = -log F(omega|N_{k+1}, omega|N_k o R_k), Phi_tot <= (sum_k sqrt(Phi_k))^2 (1 + o(1)) as all Phi_k -> 0; if each step extends to a normal unital 2-positive map on F(I) with error check-Phi_k, then Phi_k <= check-Phi_k and the same bound holds with check-Phi_k. SATURATION, 'if' direction only (Rem 12.8, rem:w6-sat): when all corners of the protocol coincide at one point (e.g. VWZ 1(B), Protocol 3), Thm 8.5 (thm:prot3, card corner-calculus) and Theorem A give Phi_tot = Phi_A(sum_k zeta_k) = f2 (sum_k zeta_k)^2 + o and check-Phi_k = f2 zeta_k^2 + o, so the second-order bound is saturated at second order. NOT claimed: the converse (non-saturation for corners at distinct points); the document compares with the conjectural network law W2 only 'as a target, not used' (l. 1962), and W2 would at best concern the extended errors check-Phi_k. NOT claimed: the ANGLE FORM (arccos F adds along the chain; Thm 12.5, thm:w6) and its exact form Phi_tot <= -log cos(sum_k arccos e^{-Phi_k}) (Cor 12.7(1), eq:w6-master). The document proves them only under Hypothesis (U), which is refuted (card hypothesis-u-natural-cone-fidelity), so they are vacuous as proved; the conditional statement is card sequential-recovery-angle-form-under-u. The angle inequality is expected to hold without (U), but no project document proves it and no card uses it.
Hypotheses
This result is conditional: at least part of the statement holds only where the hypotheses below hold. The sentences are quoted from the statement above; read the status badge only together with them.
Hypothesis labels used: U.
Type-III sequential recovery bound: Bures distances add along a chain of von Neumann inclusions (chordal and second-order forms, no Hypothesis (U)).
CHORDAL FORM (Thm 12.6, thm:w6chord), no Hypothesis (U): with d_B = sqrt(2 - 2F), d_B(omega|N_m, omega|N_1 o R) <= sum_k d_B(omega|N_{k+1}, omega|N_k o R_k).
Proof: telescoping through the states mu_j = omega|N_{m-j} o R_{m-j} o S_j, S_j = R_{m-j+1} o ... o R_{m-1} (steps <1>1-<1>3 of Thm 12.5, which do not use (U)), monotonicity of F under the channel S_j (Lemma 12.3, from Choi's inequality T(a^{-1}) >= T(a)^{-1} for unital 2-positive T, Lemma 12.2, via the Schur complement, and Alberti-Uhlmann 2002 Thm 2(1), p. 6, and Cor 2(5), p. 8), and the triangle inequality of d_B (Alberti-Uhlmann 2002 Prop. 1(1), p. 3, stated there without proof and attributed to Bures 1969, which is NOT OBTAINED).
SECOND-ORDER FORM (Cor 12.7(2), cor:w6-second), no (U): with Phi_tot = -log F(omega|N_m, omega|N_1 o R) and Phi_k = -log F(omega|N_{k+1}, omega|N_k o R_k), Phi_tot <= (sum_k sqrt(Phi_k))^2 (1 + o(1)) as all Phi_k -> 0; if each step extends to a normal unital 2-positive map on F(I) with error check-Phi_k, then Phi_k <= check-Phi_k and the same bound holds with check-Phi_k.
The document proves them only under Hypothesis (U), which is refuted (card hypothesis-u-natural-cone-fidelity), so they are vacuous as proved; the conditional statement is card sequential-recovery-angle-form-under-u.
The angle inequality is expected to hold without (U), but no project document proves it and no card uses it.
How to verify
No numerics needed. Chordal form: rigor/network_corner_calculus.tex Thm 12.6 (thm:w6chord, l. 1879) with Box [G7] and Thm 12.5 <1>1-<1>3; second-order form: Cor 12.7(2), step <1>3a (l. 1908ff); saturation 'if': Rem 12.8 (rem:w6-sat, l. 1954-1962) with Thm 8.5 (card corner-calculus) and Theorem A (card thm-a-quadratic-law); numerical cross-check of the two second-order routes: rigor/ref_p6_3_separation.out (d).
Evidence
- rigor/network_corner_calculus.tex — document, at
thm:w6 - rigor/network_corner_calculus.tex — document, at
thm:w6chord - rigor/network_corner_calculus.tex — document, at
cor:w6-second refs/AlbertiUhlmann02_math-ph-0202038.pdf— source; held privately, not redistributedrefs/Uhlmann76.pdf— source; held privately, not redistributed- rigor/ref_p6_3_separation.py — numerics
- rigor/network_corner_calculus.tex — document, at
rem:w6-sat
Related claims
- Corner calculus: sequential one-sided recovery = Schwarzian point masses at the junctions —
proved - Second-order network law: Phi_tot = sum zeta_j zeta_k G(y_j - y_k), G = c Ghat universal —
conjectural phase6-plan—active, no page of its own- Theorem A: lim Phi/zeta^2 = c/(12 pi^2) —
refereed - Angle form of the sequential recovery bound, conditional on Hypothesis (U) (vacuous: (U) is refuted) —
proved hypothesis-u-natural-cone-fidelity—refuted, no page of its own
Review
Review record: passed 2026-09-23 by REF-DEP-CFT-B5.
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