Logarithmic-gap MINKT #
This module exposes the exact Gap_tau MINKT promise from Hirahara's 2022
Definition 3.3. For (x,1^t,1^s), it distinguishes C^t(x) <= s from
C^tau(x) > s + log_2(tau). It also packages Fact 3.4's numerical estimator
sandwich and proves that thresholding any such estimator solves the promise.
The identity transformation is admissible.
Widening places the transformed clock after the source clock.
The logarithmic no condition excludes exactly the programs meeting its relaxed description budget and transformed clock.
A widening clock prevents a source yes-instance from also satisfying the exact logarithmic no condition.
Canonical yes membership is the source bounded-complexity inequality.
Canonical no membership is the exact transformed-clock lower bound.
Widening makes the exact logarithmic promise sides disjoint.
The estimator's upper bound places it below every yes threshold.
The estimator's lower bound places it above every no threshold.
Executable thresholding characterizes the estimator completion.
Adding a threshold and then forgetting it recovers the original MINKT instance.
If some threshold up to the cap is accepted, bounded search returns an accepted threshold no larger than that witness.
A valid estimator completion contains the yes language.
A valid estimator completion excludes the logarithmic no language.
Thresholding a valid estimator accepts every promised yes-instance.
Thresholding a valid estimator rejects every promised no-instance.
The widening-certified exact logarithmic GapMINKT promise.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The reverse numerical direction of Fact 3.4 at one finite source instance.
Bounded threshold search against any solver for logarithmic GapMINKT returns a value between the later-clock complexity minus logarithmic slack and the exact source-clock complexity.
A gap solver yields the Fact 3.4 estimator sandwich on every explicitly eligible input whose source-clock complexity is finite.
Exact domain-restricted reverse Fact 3.4: on inputs with |x| <= t, it is
enough that the source complexity be finite on that same domain.
If source-clock complexity is finite on every input, bounded threshold search converts a logarithmic-gap solver into a global Fact 3.4 estimator.
Thresholding a valid estimator solves the exact logarithmic promise.
If a valid estimator's threshold language is in P, it completes the exact
logarithmic promise in deterministic polynomial time.