Efficient threshold search for logarithmic-gap MINKT #
This module proves the algorithmic reverse direction of Hirahara's Fact 3.4.
If the one-bit characteristic string of a logarithmic-gap solver is in FP, an
explicit t+1-step unary sweep computes the corresponding numerical estimator
in FP. On canonical (x,1^t) inputs its output length is exactly the semantic
least-accepted-threshold estimator.
On canonical MINKT inputs, the threshold sweep returns the semantic least-accepted threshold in exact unary form.
On canonical MINKT inputs, the unary sweep output has exactly the semantic least-accepted threshold as its length.
The estimator represented by the executable unary sweep is extensionally the semantic time-capped search estimator.
The numerical estimator represented by the threshold sweep satisfies the Fact 3.4 sandwich at every finite source instance.
The executable estimator satisfies Fact 3.4 on any explicit domain where the source-clock complexity is finite.
Algorithmic reverse Fact 3.4 on the paper's exact |x| <= t domain.
The first conjunct is the concrete FP unary estimator implementation; the
second is its numerical sandwich on every eligible input.
Generic efficient universality discharges source finiteness on a uniform
polynomial printer-clock domain. The returned coefficients depend only on the
universal machine: they are chosen before the clock parameters and the solver,
and for every widening clock and every FP solver of logarithmic GapMINKT,
every eligible (x,1^t) with the printer clock below t receives both the
executable FP estimator and the Fact 3.4 sandwich.
Under global source finiteness, the executable estimator satisfies the global Fact 3.4 sandwich.