Logarithmic-gap MINKT -- definitions

This is the exact machine-relative form of Hirahara's Gap_tau MINKT promise from Definition 3.3 of Symmetry of Information from Meta-Complexity (CCC 2022). It reuses the canonical (x, 1^t, 1^s) codec from GapMINKT, but fixes the promised sides to

• yes: C^t(x) <= s;
• no: C^tau(x) > s + log_2(tau).

The existing general GapMINKT.Parameters remains useful for optimization search with an arbitrary description transformation sigma(n,s). This module is separate because the paper's exact logarithmic loss depends on the source clock through tau(n,t).

structure Complexity.GapMINKT.Logarithmic.Parameters : Type

The paper's two-argument clock transformation tau(|x|,t).

• clock : ℕ → ℕ → ℕ

  Later primitive clock from output length and source clock.

def Complexity.GapMINKT.Logarithmic.Parameters.IsWidening (parameters : Parameters) : Prop

The transformed clock never gives less time than the source clock.

Equations

• parameters.IsWidening = ∀ (outputLength time : ℕ), time ≤ parameters.clock outputLength time

def Complexity.GapMINKT.Logarithmic.Parameters.IsPolynomiallyBounded (parameters : Parameters) : Prop

One power of the total numeric input controls the clock transformation.

Equations

• parameters.IsPolynomiallyBounded = ∃ (coefficient : ℕ) (exponent : ℕ), ∀ (outputLength time : ℕ), parameters.clock outputLength time ≤ coefficient * (outputLength + time + 1) ^ exponent

structure Complexity.GapMINKT.Logarithmic.Parameters.IsAdmissible (parameters : Parameters) : Prop

A paper-level clock is admissible when it is widening and polynomially bounded. Computability remains a separate implementation property.

• widening : parameters.IsWidening

  The target clock dominates the source clock.

• polynomiallyBounded : parameters.IsPolynomiallyBounded

  The target clock has uniform polynomial growth.

def Complexity.GapMINKT.Logarithmic.Parameters.identity : Parameters

The identity transformation, giving the zero-blow-up boundary case.

Equations

• Complexity.GapMINKT.Logarithmic.Parameters.identity = { clock := fun (_outputLength time : ℕ) => time }

def Complexity.GapMINKT.Logarithmic.Parameters.transformedTime (parameters : Parameters) (inst : MINKT.Instance) : ℕ

Apply the clock transformation to a threshold-free MINKT instance.

Equations

• parameters.transformedTime inst = parameters.clock inst.output.length inst.time

def Complexity.GapMINKT.Logarithmic.Parameters.logarithmicSlack (parameters : Parameters) (inst : MINKT.Instance) : ℕ

Base-two logarithmic slack at the transformed clock.

Equations

• parameters.logarithmicSlack inst = Nat.log 2 (parameters.transformedTime inst)

@[reducible, inline]

abbrev Complexity.GapMINKT.Logarithmic.Estimator : Type

A threshold-free numerical estimator for ordinary bounded complexity.

Equations

• Complexity.GapMINKT.Logarithmic.Estimator = (Complexity.MINKT.Instance → ℕ)

def Complexity.GapMINKT.Logarithmic.Estimator.SatisfiesBounds {tapes : ℕ} (estimate : Estimator) (machine : TM tapes) (parameters : Parameters) : Prop

Fact 3.4's subtraction-free estimator sandwich:

B(x,1^t) <= C^t(x) and C^tau(x) <= B(x,1^t) + log_2(tau).

Equations

• One or more equations did not get rendered due to their size.

def Complexity.GapMINKT.Logarithmic.Estimator.SatisfiesBoundsOn {tapes : ℕ} (estimate : Estimator) (machine : TM tapes) (parameters : Parameters) (eligible : MINKT.Instance → Prop) : Prop

The estimator sandwich restricted to an explicit set of inputs.

Hirahara's Fact 3.4 uses the domain |x| <= t. Keeping the domain explicit lets the machine-relative library state that version without pretending that an arbitrary machine can print every output at every tiny clock.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.GapMINKT.Logarithmic.IsLengthWithinTime (inst : MINKT.Instance) : Prop

The input domain |x| <= t used in Fact 3.4.

Equations

• Complexity.GapMINKT.Logarithmic.IsLengthWithinTime inst = (inst.output.length ≤ inst.time)

def Complexity.GapMINKT.Logarithmic.IsNo {tapes : ℕ} (inst : Instance) (machine : TM tapes) (parameters : Parameters) : Prop

Exact logarithmic no condition C^tau(x) > s + log_2(tau).

Equations

• One or more equations did not get rendered due to their size.

def Complexity.GapMINKT.Logarithmic.IsRelaxedWitness {tapes : ℕ} (inst : Instance) (machine : TM tapes) (parameters : Parameters) (program : List Bool) : Prop

A concrete program forbidden by the exact logarithmic no condition.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.GapMINKT.Logarithmic.yesLanguage {tapes : ℕ} (machine : TM tapes) : Language

The yes language is exactly the existing source-threshold language.

Equations

• Complexity.GapMINKT.Logarithmic.yesLanguage machine = Complexity.GapMINKT.yesLanguage machine

def Complexity.GapMINKT.Logarithmic.noLanguage {tapes : ℕ} (machine : TM tapes) (parameters : Parameters) : Language

Canonically encoded exact logarithmic no language.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.GapMINKT.Logarithmic.estimatorLanguage (estimate : Estimator) : Language

Total completion obtained by thresholding a numerical estimator.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.GapMINKT.Logarithmic.decisionOfEstimator (estimate : Estimator) : List Bool → Bool

Executable thresholding of an ordinary bounded-complexity estimator.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.GapMINKT.Logarithmic.thresholdInstance (inst : MINKT.Instance) (threshold : ℕ) : Instance

Add a description threshold to a threshold-free MINKT instance.

Equations

• Complexity.GapMINKT.Logarithmic.thresholdInstance inst threshold = { output := inst.output, time := inst.time, threshold := threshold }

def Complexity.GapMINKT.Logarithmic.firstAcceptedThreshold (decide : List Bool → Bool) (inst : MINKT.Instance) (cap : ℕ) : ℕ

Search the finite interval [0,cap] for the first threshold accepted by a Boolean promise solver. If the solver accepts none of them, return cap.

The fallback makes the operation total. Correctness theorems use an accepted upper bound, so the fallback branch is then unreachable.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.GapMINKT.Logarithmic.estimatorOfSolver (decide : List Bool → Bool) (cap : MINKT.Instance → ℕ) : Estimator

Turn a gap solver into a numerical estimator by bounded threshold search.

Equations

• Complexity.GapMINKT.Logarithmic.estimatorOfSolver decide cap inst = Complexity.GapMINKT.Logarithmic.firstAcceptedThreshold decide inst (cap inst)

def Complexity.GapMINKT.Logarithmic.timeSearchEstimator (decide : List Bool → Bool) : Estimator

The canonical Fact 3.4 search uses the unary source clock as its threshold cap. Every finite source complexity is at most this value by input locality.

Equations

• Complexity.GapMINKT.Logarithmic.timeSearchEstimator decide = Complexity.GapMINKT.Logarithmic.estimatorOfSolver decide fun (inst : Complexity.MINKT.Instance) => inst.time