ScoreQuant

Result · D-EXCHANGE-TERMINATES

Finite D exchange terminates

Proved heremachine-checked statementpublication: internal

Read the proof and evidence →

Meaning

Accepting only strictly positive exact gains yields monotone search on finitely many assignments.

Statement

Accepting only exact positive D gains strictly increases the objective, cannot cycle, and terminates finitely at a one-point exchange-stable state.

Assumptions

  • finite labeling set

  • only exact positive gains accepted, at zero tolerance

  • one-point relocations preserving nonempty source cells

  • the determinant objective det I, matching ExchangeStable's convention; the log det run is a different run

Closest prior work

Nearest prior work

Relationships

Rests on

The full chain beneath it

Enables

Open next door

Machine-checked statement

The statement is proved in Lean 4.33.1 + Mathlib 4.33.1 as ScoreQuantFormal.d_exchange_terminates. Its hypotheses and conclusion are frozen in a specification file that was audited against this page's statement before the proof was written (verdict: fixes verified with residue). A Lean build certifies the theorem, not the Python and JAX code that implements it.

In the library

Carried by DExchangeConfig. Reference.

Every object and refusal

Local graph
Local map of Monotone exact D one-point exchange1 prerequisites to the left, 1 results it enables or questions it raises to the right, 0 boundary cases below.Exact finite D log-determinant gainExact finite D log-de…Exact finite inductive closure / compilerExact finite inductiv…Monotone exact D one-point exchangeMonotone exact D one-…
Prerequisites to the left, what it enables or raises to the right, boundary cases below. Open in the map.

Proof

D8. Monotone exact one-point exchange

Accepting only exact positive D gains gives:

  • strict objective ascent;
  • no cycles;
  • finite termination because the labeling set is finite;
  • a terminal one-point exchange-stable solution;
  • by D5/D6, a canonical deployable D quantizer.

Machine-checked. All three clauses are now frozen in formal/ScoreQuantFormal/TerminationSpec.lean and discharged by ScoreQuantFormal.d_exchange_terminates, audited in AUDITS/FORMALIZATION-D-EXCHANGE-TERMINATES-001.md. The argument is generic in the objective, so ScoreQuantFormal.terminates, ascent_strict and no_cycle also cover the termination sentences of DS3 and A1 — but neither FsF_s nor FAF_A exists as a Lean object in that tree, so those two claims carry no formal_proof and this note is their record.

Two cautions. The det⁡\det and log⁡det⁡\log\det runs are different runs: a det⁡\det-stable state can still admit a log⁡det⁡\log\det-improving move, so both instances are stated and proved separately. And nothing formal chains a terminal stable state back to D5 — the fifth bullet above is prose, not a machine-checked consequence. ScoreQuantFormal.no_infinite_strict_ascent and exists_exchangeStable in Corollaries.lean remain as the earlier, weaker fragments.

From D-optimality · chapter contents