ScoreQuant

Result · DS-EXACT-MOVE-ORACLE

Profiled moves have an exact gain

Proved herepublication: internal

Read the proof and evidence →

Meaning

An exact one-point objective oracle compares feasible finite assignments with nuisance profiling.

Statement

The full information has the universal rank-two update and exact profiled gain is Δlogdet I-Δlogdet I_λλ, giving an exact low-rank finite move oracle when blocks stay nonsingular.

Relationships

Rests on

Enables

Raises

Open next door

Local graph
Local map of Exact finite Ds one-point objective oracle2 prerequisites to the left, 5 results it enables or questions it raises to the right, 0 boundary cases below.Exact weighted rank-two relocationExact weighted rank-t…Ds objective is the logdet of efficient/profiled Schur informationDs objective is the l…Monotone exact Ds exchange terminates finitelyMonotone exact Ds exc…Approximate finite Ds efficient-Voronoi necessity boundApproximate finite Ds…Best practical Ds solver with theorem-backed certificateBest practical Ds sol…Exact profiled leverage stability boundExact profiled levera…Stronger local neighborhoodsStronger local neighb…Exact finite Ds one-point objective oracleExact finite Ds one-p…
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