cft-cmi

A-C restriction bound: (Tcond) implies E_AC = 0 exactly; applied on the hopping chain (4,8,2), (4,12,2), (4,16,2)

Status: proved — a complete structured proof.

Area: Optimality of recovery channels (O8, Phases 3 and 3b) · Card type: result · Knowledge-base id: ac-lower-bound-zero

Statement

Proved, as an implication (Prop. prop:AC-zero, rigor/optimality_second_order.tex:408-434): if some T: h_C -> h_B satisfies (eq:Tcond) Q_AB T = Q_AC, T*T <= 1, T* Q_BB T <= Q_CC <= 1 - T*(1 - Q_BB) T, then X* := (0 T) and Z := (1/2) 1_B (+) Q_CC give (X, Z) in F whose recovered symbol on h_A (+) h_C is the vacuum one, so a gauge-invariant quasi-free channel beta in C reproduces omega exactly on A(A) v A(C): E_AC = 0 and the restriction bound (eq:AC-bound) of Lemma lem:restriction gives nothing. Application: the hypothesis is established only numerically, on the half-filled hopping chain for (L_A,L_B,L_C) = (4,8,2), (4,12,2), (4,16,2), where T = Q_AB^+ Q_AC satisfies (Tcond) (card ac-intertwiner-exists-hopping-chain); on these three chains E_AC = 0 exactly, consistent with the direct convex minimisation of numerics/optimality/lower_bound.py (lb.log: E_AC = 1.53e-9, 9.83e-10, 6.99e-9, solver floor, against -log F(omega_AC, omega_A (x) omega_C) = 3.17e-3, 1.66e-3, 1.03e-3). Nothing is claimed for the continuum or for other geometries: lb.log's third row (6,12,3) gives E_AC = 2.27e-5 (E_AC/z^2 = 0.0045), and at (6,12,3) and (8,16,4) the Moore-Penrose T violates (Tcond) (margins -0.133, -0.464; numerics/kb-checks-2026-09-23/tcond_check_extra.out). Until 2026-09-24 the tex concluded that the O8 route ('bound the Bures distance of the vacuum A-C state to the B-mediated ones') yields no bound at all (:450-457), an extrapolation from these three chains by a heuristic mechanism. It now draws that conclusion only for the three chains and calls 'no bound at all' (continuum, other geometries) an extrapolation that is not shown, and the mechanism heuristic (:452-453; likewise the Q4 verdict :741-745 and the list of results proved, :769; Correction C2); its summary (:28-31) no longer claims a nonzero lower bound of order z^2: on these chains the restriction bound is exactly zero, and only E_opt >= 0 is proved (Correction C3). The extrapolation is not part of this card.

How to verify

rigor/optimality_second_order.tex Prop. 4.2 (prop:AC-zero) with proof steps <1>1-<1>4 (:419-434: X* = (0 T), Z = 1/2 1 (+) Q_CC; Lemma lem:rec-symbol; Prop. prop:cp), verdict box :436-457; the section Corrections of 2026-09-24 (Sec. 7), items C2 and C3 (l. 820-864). Hypothesis on the three chains, from the cft_cmi root: python3 numerics/kb-checks-2026-09-23/tcond_check.py (needs numpy); expected output as in tcond_check.out: residual 3.6e-17, 1.8e-17, 1.8e-17, ||T|| = 0.5524, 0.3779, 0.2894, both margins 0.1216, 0.1510, 0.1630. Direct minimisation: numerics/optimality/lb.log (E_AC and the norm of the Powell-optimised T, 0.5503, 0.3776, 0.2851; lb.log contains no residual). Other geometries: tcond_check_extra.py / .out in the same folder.

Evidence

Related claims

None recorded.

Review

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

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