Angle form of the sequential recovery bound, conditional on Hypothesis (U) (vacuous: (U) is refuted)

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-angle-form-under-u

Statement

UNDER Hypothesis (U) (card hypothesis-u-natural-cone-fidelity, which is REFUTED): in the setting of card sequential-recovery-bound-type-iii, the Bures angles A = arccos F add along the chain, A(omega|N_m, omega|N_1 o R) <= sum_k A(omega|N_{k+1}, omega|N_k o R_k) (Thm 12.5, thm:w6), and Phi_tot <= -log cos(sum_k arccos e^{-Phi_k}) whenever sum_k arccos e^{-Phi_k} < pi/2 (Cor 12.7(1), eq:w6-master). (U) enters only at thm:w6 <1>4 (l. 1846): all mu_j get natural-cone representatives in one Hilbert space whose inner products are the fidelities, so the spherical triangle inequality (lem:spherical) applies. Since (U) is false, this proof establishes nothing; the implication is recorded so that the knowledge base shows it as vacuous. The unconditional angle inequality is expected to hold (Uhlmann's supremum formula F = sup |<xi, u' eta>|, a sequential choice of vector representatives and lem:spherical), 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.

Angle form of the sequential recovery bound, conditional on Hypothesis (U) (vacuous: (U) is refuted).

UNDER Hypothesis (U) (card hypothesis-u-natural-cone-fidelity, which is REFUTED): in the setting of card sequential-recovery-bound-type-iii, the Bures angles A = arccos F add along the chain, A(omega|N_m, omega|N_1 o R) <= sum_k A(omega|N_{k+1}, omega|N_k o R_k) (Thm 12.5, thm:w6), and Phi_tot <= -log cos(sum_k arccos e^{-Phi_k}) whenever sum_k arccos e^{-Phi_k} < pi/2 (Cor 12.7(1), eq:w6-master).

(U) enters only at thm:w6 <1>4 (l. 1846): all mu_j get natural-cone representatives in one Hilbert space whose inner products are the fidelities, so the spherical triangle inequality (lem:spherical) applies.

Since (U) is false, this proof establishes nothing; the implication is recorded so that the knowledge base shows it as vacuous.

How to verify

rigor/network_corner_calculus.tex Thm 12.5 (thm:w6, l. 1816-1855): only step <1>4 (l. 1846-1850) invokes hyp:U; Cor 12.7(1) (cor:w6-second, <1>2).

Evidence

• rigor/network_corner_calculus.tex — document, at thm:w6
• rigor/network_corner_calculus.tex — document, at cor:w6-second
• rigor/network_corner_calculus.tex — document, at hyp:U

Related claims

• Type-III sequential recovery bound: Bures distances add along a chain of von Neumann inclusions (chordal and second-order forms, no Hypothesis (U)) — proved

Review

Review record: passed 2026-09-23 by REF-DEP-CFT-B4.

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