ScoreQuant

Result · A-EXACT-MOVE-ORACLE

Finite A moves have an exact gain

Proved herepublication: internal

Read the proof and evidence →

Meaning

Relocation updates give an exact objective comparison for the A criterion under its feasibility conditions.

Statement

For F_A(I)=-tr(I^{-1}), the universal rank-two information move plus Woodbury gives an exact O(d^2)-type move oracle.

Relationships

Rests on

Enables

Raises

Open next door

Local graph
Local map of Exact finite A move oracle1 prerequisites to the left, 2 results it enables or questions it raises to the right, 0 boundary cases below.Exact weighted rank-two relocationExact weighted rank-t…Monotone exact A exchange terminates finitelyMonotone exact A exch…Quantitative A finite-geometry necessity boundQuantitative A finite…Exact finite A move oracleExact finite A move o…
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