Nested finite-moment completion frontiers converge to the frontier determined by the full moment family.
Theorem 1.1 (Finite atomic frontiers decrease to the full frontier).
∀ C ∈ Real ( ) , c a p ∈ Real ( ) , l e v e lM a t c h ∈ Nat ( ) → ( Measure ( Real ( ) ) → P ro p ) , f u llM a t c h ∈ Measure ( Real ( ) ) → P ro p , reso l v e n tB u d g e t ∈ Measure ( Real ( ) ) → Real ( ) , w hi t e Fl oor ∈ Measure ( Real ( ) ) → Real ( ) , o pt imi zer ∈ Nat ( ) → Measure ( Real ( ) ) , c l u s t er ∈ Measure ( Real ( ) ) , se l ec t i o n ∈ Nat ( ) → Nat ( ) , ( ( ∀ n u ∈ Measure ( Real ( ) ) , apply ( w hi t e Fl oor , n u ) ≤ c a p ) ∧ ( ( ∀ N ∈ Nat ( ) , n u ∈ Measure ( Real ( ) ) , applyTwo ( l e v e lM a t c h , add ( N , 1 ) , n u ) ⇒ applyTwo ( l e v e lM a t c h , N , n u ) ) ∧ ( ( ∀ n u ∈ Measure ( Real ( ) ) , apply ( f u llM a t c h , n u ) ⇒ ( ∀ N ∈ Nat ( ) , applyTwo ( l e v e lM a t c h , N , n u ) ) ) ∧ ( ( ∀ n u ∈ Measure ( Real ( ) ) , ( ∀ N ∈ Nat ( ) , applyTwo ( l e v e lM a t c h , N , n u ) ) ⇒ apply ( f u llM a t c h , n u ) ) ∧ ( ( ∀ N ∈ Nat ( ) , applyTwo ( l e v e lM a t c h , N , apply ( o pt imi zer , N ) ) ) ∧ ( ( ∀ N ∈ Nat ( ) , apply ( reso l v e n tB u d g e t , apply ( o pt imi zer , N ) ) ≤ C ) ∧ ( ( ∀ N ∈ Nat ( ) , apply ( w hi t e Fl oor , apply ( o pt imi zer , N ) ) = sSup ( { ∃ n u ∈ Measure ( Real ( ) ) , applyTwo ( l e v e lM a t c h , N , n u ) ∧ ( apply ( reso l v e n tB u d g e t , n u ) ≤ C ∧ r = apply ( w hi t e Fl oor , n u ) ) ∣ r ∈ Real ( ) } ) ) ∧ ( ( ∀ N ∈ Nat ( ) , applyTwo ( l e v e lM a t c h , N , c l u s t er ) ) ∧ ( apply ( reso l v e n tB u d g e t , c l u s t er ) ≤ C ∧ ( StrictMono ( se l ec t i o n ) ∧ Tendsto ( ( k : Nat ( ) ↦ apply ( w hi t e Fl oor , apply ( o pt imi zer , apply ( se l ec t i o n , k ) ) ) ) , a tT o p , nhds ( apply ( w hi t e Fl oor , c l u s t er ) ) ) ) ) ) ) ) ) ) ) ) ) ⇒ let l e v e l Va l u es = N : Nat ( ) ↦ { ∃ n u ∈ Measure ( Real ( ) ) , applyTwo ( l e v e lM a t c h , N , n u ) ∧ ( apply ( reso l v e n tB u d g e t , n u ) ≤ C ∧ r = apply ( w hi t e Fl oor , n u ) ) ∣ r ∈ Real ( ) } , let f u ll Va l u es = { ∃ n u ∈ Measure ( Real ( ) ) , apply ( f u llM a t c h , n u ) ∧ ( apply ( reso l v e n tB u d g e t , n u ) ≤ C ∧ r = apply ( w hi t e Fl oor , n u ) ) ∣ r ∈ Real ( ) } , let hi er a rc h y = N : Nat ( ) ↦ sSup ( apply ( l e v e l Va l u es , N ) ) , let f u llF ro n t i er = sSup ( f u ll Va l u es ) , Antitone ( hi er a rc h y ) ∧ Tendsto ( hi er a rc h y , a tT o p , nhds ( f u llF ro n t i er ) )
Proof. Machine-checked in Lean as D5/S3/Weil/Budget/AtomicMomentHierarchyConvergence.atomic_moment_hierarchy_converges (✓ std3). ∎
Source. Repository-derived.
Commentary.
Nested moment constraints make the finite frontiers antitone. A strict optimizer subsequence whose cluster satisfies every determining constraint identifies its order limit with the full frontier.