ScoreQuant

Result · DS-EXCHANGE-TERMINATES

Finite profiled exchange terminates

Proved herepublication: internal

Read the proof and evidence →

Meaning

Strictly improving feasible profiled moves terminate on a finite assignment space.

Statement

Accepting only exact positive Ds gains on a finite labeling set yields strict ascent and finite termination at a one-point exchange-stable state.

Relationships

Rests on

The full chain beneath it

Enables

Open next door

Local graph
Local map of Monotone exact Ds exchange terminates finitely1 prerequisites to the left, 1 results it enables or questions it raises to the right, 0 boundary cases below.Exact finite Ds one-point objective oracleExact finite Ds one-p…Exchange-stable Ds states span both margin regimes; ascent selects the funnel at scaleExchange-stable Ds st…Monotone exact Ds exchange terminates finitelyMonotone exact Ds exc…
Prerequisites to the left, what it enables or raises to the right, boundary cases below. Open in the map.

Proof

DS3. Exact finite one-point objective oracle

The same rank-two full-information update applies. The exact profiled gain is

ΔFs=Δlog⁡det⁡I−Δlog⁡det⁡Iλλ,\boxed{ \Delta F_s = \Delta\log\det I - \Delta\log\det I_{\lambda\lambda}, }

with each term evaluable by low-rank determinant algebra when blocks remain nonsingular. Exact positive-gain DsD_s exchange is therefore monotone and finitely terminating on a finite sample. The termination sentence is machine-checked generically, as ScoreQuantFormal.terminates with ascent_strict and no_cycle, in formal/ScoreQuantFormal/Termination.lean: the argument uses only that the objective is real-valued and the labeling set finite. DS-EXCHANGE-TERMINATES carries no formal_proof all the same, because FsF_s exists as no Lean object in that tree and no frozen conclusion instantiates it — see AUDITS/FORMALIZATION-D-EXCHANGE-TERMINATES-001.md.

From Profiled Ds-optimality · chapter contents