Gap conditional MinKT -- definitions

This is the machine-relative form of Hirahara's Gap_tau MINcKT promise from Definition 6.1 of Symmetry of Information from Meta-Complexity (CCC 2022). For an instance (x, y, 1^t, 1^s), write t' = tau(|x|, |y|, t). The promised sides are

• yes: C_cond^t(x | y) + cd^(t,t')(y) <= s;
• no: C_cond^t'(x | y) > s + log_2(t').

The sum on the yes side is the natural-number-safe form of the paper's C_cond^t(x | y) <= s - cd^(t,t')(y): if the depth exceeds s, the yes condition is false rather than relying on truncated subtraction.

The ordinary machine used for depth and the oracle machine used for conditional complexity are explicit and may differ. Relating them to one paper-specific universal evaluator is a later simulation theorem.

structure Complexity.GapMINCKT.Parameters : Type

The three-argument clock transformation tau(|x|, |y|, t).

• clock : ℕ → ℕ → ℕ → ℕ

  Later primitive clock from output length, condition length, and source clock.

def Complexity.GapMINCKT.Parameters.IsWidening (parameters : Parameters) : Prop

The transformed clock never gives less time than the source clock. This is the semantic condition needed to make the two promise sides disjoint.

Equations

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

def Complexity.GapMINCKT.Parameters.IsPolynomiallyBounded (parameters : Parameters) : Prop

One power of the total numeric input controls the clock transformation. This records the polynomial-growth part of the paper's quantification over tau; computability of the transform is a separate implementation property.

Equations

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

structure Complexity.GapMINCKT.Parameters.IsAdmissible (parameters : Parameters) : Prop

An admissible paper-level clock is widening and polynomially bounded.

• widening : parameters.IsWidening

  The transformed clock dominates the source clock.

• polynomiallyBounded : parameters.IsPolynomiallyBounded

  The transformed clock has uniform polynomial growth.

def Complexity.GapMINCKT.Parameters.identity : Parameters

The identity clock, useful as the zero-depth boundary case.

Equations

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

def Complexity.GapMINCKT.Parameters.transformedTime (parameters : Parameters) (inst : MINCKT.Instance) : ℕ

Apply the clock transformation to one threshold-free conditional MinKT instance.

Equations

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

def Complexity.GapMINCKT.Parameters.logarithmicSlack (parameters : Parameters) (inst : MINCKT.Instance) : ℕ

Base-two logarithmic error attached to the transformed clock.

Equations

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

@[reducible, inline]

abbrev Complexity.GapMINCKT.Estimator : Type

A threshold-free numerical estimator for conditional bounded complexity.

Equations

• Complexity.GapMINCKT.Estimator = (Complexity.MINCKT.Instance → ℕ)

def Complexity.GapMINCKT.Estimator.SatisfiesBounds {ordinaryTapes conditionalTapes : ℕ} (estimate : Estimator) (ordinaryMachine : TM ordinaryTapes) (conditionalMachine : OracleTM conditionalTapes) (parameters : Parameters) : Prop

The two-sided estimator sandwich used in Proposition 6.2:

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

Both inequalities use WithTop so a claimed estimator also certifies the relevant descriptions are finite.

Equations

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

structure Complexity.GapMINCKT.Instance : Type

A decoded conditional gap instance (x, y, 1^t, 1^s).

• output : List Bool

  String whose conditional complexity is measured.

• condition : List Bool

  Finite random-access condition.

• time : ℕ

  Source primitive clock.

• threshold : ℕ

  Source description threshold.

def Complexity.GapMINCKT.Instance.base (inst : Instance) : MINCKT.Instance

Forget the decision threshold, retaining the conditional MinKT instance.

Equations

• inst.base = { output := inst.output, condition := inst.condition, time := inst.time }

def Complexity.GapMINCKT.Instance.unaryThreshold (inst : Instance) : List Bool

Unary encoding of the decision threshold.

Equations

• inst.unaryThreshold = List.replicate inst.threshold true

def Complexity.GapMINCKT.Instance.encode (inst : Instance) : List Bool

Canonical nested-pair encoding of (x, y, 1^t, 1^s).

Equations

• inst.encode = Complexity.pair inst.base.encode inst.unaryThreshold

def Complexity.GapMINCKT.Instance.decode? (bits : List Bool) : Option Instance

Decode one canonical gap instance, rejecting malformed conditional MinKT codes and every non-unary threshold field.

Equations

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

def Complexity.GapMINCKT.Instance.withThreshold (inst : Instance) (threshold : ℕ) : Instance

Replace only the source description threshold.

Equations

• inst.withThreshold threshold = { output := inst.output, condition := inst.condition, time := inst.time, threshold := threshold }

def Complexity.GapMINCKT.Instance.laterTime (inst : Instance) (parameters : Parameters) : ℕ

The transformed clock tau(|x|, |y|, t).

Equations

• inst.laterTime parameters = parameters.transformedTime inst.base

def Complexity.GapMINCKT.Instance.logSlack (inst : Instance) (parameters : Parameters) : ℕ

The base-two logarithmic slack on the no side.

Equations

• inst.logSlack parameters = parameters.logarithmicSlack inst.base

noncomputable def Complexity.GapMINCKT.Instance.conditionDepth {tapes : ℕ} (inst : Instance) (ordinaryMachine : TM tapes) (parameters : Parameters) : WithTop ℕ

The condition's two-clock computational depth C^t(y) - C^tau(y).

Equations

• inst.conditionDepth ordinaryMachine parameters = ordinaryMachine.computationalDepthBetween inst.condition inst.time (inst.laterTime parameters)

def Complexity.GapMINCKT.Instance.IsYes {ordinaryTapes conditionalTapes : ℕ} (inst : Instance) (ordinaryMachine : TM ordinaryTapes) (conditionalMachine : OracleTM conditionalTapes) (parameters : Parameters) : Prop

Promised yes condition C_cond^t(x | y) + cd^(t,tau)(y) <= s.

Equations

• inst.IsYes ordinaryMachine conditionalMachine parameters = (inst.base.complexity conditionalMachine + inst.conditionDepth ordinaryMachine parameters ≤ ↑inst.threshold)

def Complexity.GapMINCKT.Instance.IsNo {conditionalTapes : ℕ} (inst : Instance) (conditionalMachine : OracleTM conditionalTapes) (parameters : Parameters) : Prop

Promised no condition C_cond^tau(x | y) > s + log_2(tau).

Equations

• inst.IsNo conditionalMachine parameters = (↑(inst.threshold + inst.logSlack parameters) < (inst.base.withTime (inst.laterTime parameters)).complexity conditionalMachine)

def Complexity.GapMINCKT.Instance.IsAdjustedWitness {ordinaryTapes conditionalTapes : ℕ} (inst : Instance) (ordinaryMachine : TM ordinaryTapes) (conditionalMachine : OracleTM conditionalTapes) (parameters : Parameters) (program : List Bool) : Prop

A concrete program witnessing the depth-adjusted yes budget.

Equations

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

def Complexity.GapMINCKT.Instance.IsRelaxedWitness {conditionalTapes : ℕ} (inst : Instance) (conditionalMachine : OracleTM conditionalTapes) (parameters : Parameters) (program : List Bool) : Prop

A concrete program forbidden by the promised no condition.

Equations

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

def Complexity.GapMINCKT.yesLanguage {ordinaryTapes conditionalTapes : ℕ} (ordinaryMachine : TM ordinaryTapes) (conditionalMachine : OracleTM conditionalTapes) (parameters : Parameters) : Language

Canonically encoded depth-adjusted yes language. Malformed codes are outside the promise.

Equations

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

def Complexity.GapMINCKT.noLanguage {conditionalTapes : ℕ} (conditionalMachine : OracleTM conditionalTapes) (parameters : Parameters) : Language

Canonically encoded logarithmic-slack no language.

Equations

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

def Complexity.GapMINCKT.estimatorLanguage (estimate : Estimator) : Language

Total completion obtained by accepting exactly when the estimator value is at most the encoded threshold. Malformed codes are rejected.

Equations

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

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

Executable thresholding of a numerical estimator.

Equations

• Complexity.GapMINCKT.decisionOfEstimator estimate bits = match Complexity.GapMINCKT.Instance.decode? bits with | some inst => decide (estimate inst.base ≤ inst.threshold) | none => false