ScoreQuant

Result · A-EXCHANGE-TERMINATES

Finite A exchange terminates

Proved herepublication: internal

Read the proof and evidence →

Meaning

Strictly improving feasible moves cannot cycle through the finite set of assignments.

Statement

Accepting only exact positive A gains gives strict ascent and finite termination on a finite labeling set.

Relationships

Rests on

The full chain beneath it

Open next door

Local graph
Local map of Monotone exact A exchange terminates finitely1 prerequisites to the left, 0 results it enables or questions it raises to the right, 0 boundary cases below.Exact finite A move oracleExact finite A move o…Monotone exact A exchange terminates finitelyMonotone exact A exch…
Prerequisites to the left, what it enables or raises to the right, boundary cases below. Open in the map.

Proof

A1. Exact finite move oracle

The universal rank-two ΔI\Delta I plus Woodbury gives an exact O(d2)O(d^2)-type A move oracle; exact positive-gain exchange is monotone and finitely terminating. 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. A-EXCHANGE-TERMINATES carries no formal_proof all the same, because FAF_A exists as no Lean object in that tree and no frozen conclusion instantiates it — see AUDITS/FORMALIZATION-D-EXCHANGE-TERMINATES-001.md.

From A-optimality · chapter contents