mpmath at 60-80 digits: dist((1-Pi)M, Ext) = 0 exactly

Status: numerical — measured, with an error bar and a convergence order; not a theorem.

Area: Optimality of recovery channels (O8, Phases 3 and 3b) · Card type: result · Knowledge-base id: e2-mpmath-distance-exactly-zero

Statement

R := ||M||^2 - ||Pi M||^2 - ||Proj_Ext M||^2 = dist((1-Pi)M, Ext)^2, recomputed in mpmath from the closed forms P_jk = (1/L) sum_{n<L/2} w^{n(j-k)} and d_jk = (1/L) sum_n i nu_n s_n w^{n(j-k)}: R = -6.5e-60 (L=32, 60 dps), -2.5e-56 (L=48, 60 dps), +6.7e-72 (L=64, 80 dps), against ||(1-Pi)M||^2 = 4.4e-2, 3.0e-2, 2.6e-2. The residue tracks the working precision (12 orders smaller when dps goes 60 -> 80) and not the smallest denominator d^c (1e-16 at L=48, 1e-21 at L=64), so dist = 0 exactly. Leak of eta onto the d=0 modes <= 4e-118, leak of K identically 0. This closes the only precision caveat on the double-precision distances of e2_dist_ub.py.

How to verify

run numerics/optimality_all/e2_mp.py 32 60 (then 48 60, 64 80); read the line 'R = dist((1-Pi)M,Ext)^2'

Evidence

• numerics/optimality_all/e2_mp.py — numerics
• rigor/exterior_extension_numerics.tex — document, at sec:dist

Related claims

• Optimised exterior extension: UB_c = (1/2)s^2|u|^2 exactly and UB_rot/UB_c = 1-theta — numerical
• NS-circle model: Ext = N^perp exactly, with the dimension identity (L-|I|)^2 — numerical

Review

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

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