Noisy Moment Phase Boundary
Abstract
Assuming every nonconstant dual coefficient is nonzero, every feasible exterior mass satisfies the affine noisy-moment bound, whose equality case has a unique probability pair.
Theorem 1.1 (Affine bound and exact equality classification).
Proof. Machine-checked in Lean as D5/S3/Analytic/NoisyMomentPhaseBoundary.exact_noise_phase_classification (✓ std3). ∎
Source. Repository-derived.
Commentary.
For distinct real nodes and an off-node point, the Lagrange 0/1 dual polynomial determines P, the coefficient cost L, the signed perturbation r, and transition slopes A_i=Pr_i/c_i-L. Feas_epsilon(w,u,v) abbreviates exactly the normalized nonnegative weights and all-moment error bounds displayed in the theorem formula. Assuming every nonconstant dual coefficient is nonzero, every such feasible triple has a nonnegative dual gap 1+epsilonL-wP, equal to the sum of its nodal and nonconstant noisy-coordinate slacks; in particular, wP is at most 1+epsilonL. At w=(1+epsilonL)/P, feasibility holds exactly when every epsilon*A_i is at most one and the two probability weights are the computed positive and negative parts. The equality decomposition forces each nonconstant noisy moment to saturate and then forces every nodal weight, while the converse construction verifies normalization and all moments. Equality at a transition constraint is included. The result classifies attainment of this affine bound; it makes no assertion about later optimal phases or zero dual coefficients.