Finite Moment Infeasibility Certificate

Abstract

Infeasibility of the finite interval-constrained positive-semidefinite moment problem excludes every compatible real-axis even positive completion.

Theorem 1.1 (Finite SDP infeasibility is a strict completion certificate).

$$\begin{gathered} \forall N:\mathbb{N},Rlower,Rupper:\mathbb{R}, \\ target:\mathbb{R}\to \mathrm{Fin}\left(N+1\right)\to \mathbb{R},tau:\mathrm{Fin}\left(N+1\right)\to \mathbb{R}, \\ T:(\mathrm{Fin}\left(N+1\right)\to \mathbb{R})\to \mathrm{Matrix}\left(\mathrm{Fin}\left(N+1\right),\mathrm{Fin}\left(N+1\right),\mathbb{R}\right),C:\mathrm{Type}, \\ RealAxis,Even,Positive,LocalSource,CayleyCompact:C\to \mathrm{Prop}, \\ B:C\to \mathbb{R},m:C\to \mathrm{Fin}\left(N+1\right)\to \mathbb{R}, \\ (\forall c:C,m(c)(0)=B(c))\Rightarrow \\ (\forall c:C,RealAxis(c)\wedge Even(c)\wedge Positive(c)\wedge LocalSource(c)\wedge CayleyCompact(c)\Rightarrow \forall i:\mathrm{Fin}\left(N+1\right),\mathrm{abs}\left(m(c)(i)-target(B(c))(i)\right)\le B(c)\cdot tau(i))\Rightarrow \\ (\forall c:C,RealAxis(c)\wedge Even(c)\wedge Positive(c)\wedge CayleyCompact(c)\Rightarrow \mathrm{PosSemidef}\left(T(m(c))\right))\Rightarrow \\ (\neg \exists R:\mathbb{R},v:\mathrm{Fin}\left(N+1\right)\to \mathbb{R},Rlower\le R\wedge R\le Rupper\wedge v(0)=R\wedge \\ (\forall i:\mathrm{Fin}\left(N+1\right),\mathrm{abs}\left(v(i)-target(R)(i)\right)\le R\cdot tau(i))\wedge \mathrm{PosSemidef}\left(T(v)\right))\Rightarrow \\ \neg \exists c:C,RealAxis(c)\wedge Even(c)\wedge Positive(c)\wedge LocalSource(c)\wedge Rlower\le B(c)\wedge B(c)\le Rupper\wedge CayleyCompact(c). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Weil/Budget/FiniteMomentInfeasibilityCertificate.finite_moment_infeasibility_certificate (✓ std3). ∎

Source. Repository-derived.

Commentary.

The hypotheses expose the completion-to-moment construction, its zero moment, every source interval, and the Toeplitz positivity law.

A putative real-axis even positive completion with local-source consistency, an in-range resolvent budget, and a Cayley compactification would therefore construct the forbidden SDP witness.

References

• Truth anchor: D5/S3/Weil/Budget/FiniteMomentInfeasibilityCertificate.finite_moment_infeasibility_certificate