Documentation

Complexitylib.Metacomplexity.MINCKT.Gap

Gap conditional MinKT #

For a canonical input (x, y, 1^t, 1^s), this module exposes the exact depth-adjusted promise used in Hirahara's 2022 route toward excluding Heuristica:

The ordinary depth machine and conditional oracle machine remain explicit. Malformed encodings and intermediate-gap instances lie outside the promise.

The identity transform is an admissible conditional MinKT clock.

@[simp]

The unary threshold has exactly the represented length.

@[simp]

Every canonical conditional gap instance decodes exactly.

Successful decoding characterizes canonical gap-instance encodings.

Decoding fails exactly on noncanonical strings.

Canonical conditional gap encoding is injective.

@[simp]

Exact nested-pair code length for (x, y, 1^t, 1^s).

theorem Complexity.GapMINCKT.Instance.laterTime_ge (parameters : Parameters) (hwidening : parameters.IsWidening) (inst : Instance) :
inst.time inst.laterTime parameters

Widening places the transformed clock after the source clock.

theorem Complexity.GapMINCKT.Instance.conditionDepth_add_later {ordinaryTapes : } (ordinaryMachine : TM ordinaryTapes) (parameters : Parameters) (hwidening : parameters.IsWidening) (inst : Instance) :
inst.conditionDepth ordinaryMachine parameters + ordinaryMachine.timeBoundedKolmogorovComplexity inst.condition (inst.laterTime parameters) = ordinaryMachine.timeBoundedKolmogorovComplexity inst.condition inst.time

Under widening, depth plus later-clock complexity reconstructs the source-clock complexity of the condition exactly.

theorem Complexity.GapMINCKT.Instance.isYes_iff_exists_adjustedWitness {ordinaryTapes conditionalTapes : } (inst : Instance) (ordinaryMachine : TM ordinaryTapes) (conditionalMachine : OracleTM conditionalTapes) (parameters : Parameters) :
inst.IsYes ordinaryMachine conditionalMachine parameters ∃ (program : List Bool), inst.IsAdjustedWitness ordinaryMachine conditionalMachine parameters program

The depth-adjusted yes inequality is equivalent to a concrete source-clock program obeying that same adjusted description budget.

theorem Complexity.GapMINCKT.Instance.isYes_implies_base_isAtMost {ordinaryTapes conditionalTapes : } (inst : Instance) (ordinaryMachine : TM ordinaryTapes) (conditionalMachine : OracleTM conditionalTapes) (parameters : Parameters) (hyes : inst.IsYes ordinaryMachine conditionalMachine parameters) :
inst.base.IsAtMost conditionalMachine inst.threshold

Every depth-adjusted yes-instance is, in particular, below its unadjusted source threshold.

theorem Complexity.GapMINCKT.Instance.isNo_iff_no_relaxedWitness {conditionalTapes : } (inst : Instance) (conditionalMachine : OracleTM conditionalTapes) (parameters : Parameters) :
inst.IsNo conditionalMachine parameters ¬∃ (program : List Bool), inst.IsRelaxedWitness conditionalMachine parameters program

The no condition says exactly that no program meets the transformed clock and logarithmically relaxed description budget.

theorem Complexity.GapMINCKT.Instance.IsYes.withThreshold_mono {ordinaryTapes conditionalTapes : } (inst : Instance) (ordinaryMachine : TM ordinaryTapes) (conditionalMachine : OracleTM conditionalTapes) (parameters : Parameters) {first second : } (hthreshold : first second) (hyes : (inst.withThreshold first).IsYes ordinaryMachine conditionalMachine parameters) :
(inst.withThreshold second).IsYes ordinaryMachine conditionalMachine parameters

Increasing the stored threshold preserves a yes-instance.

theorem Complexity.GapMINCKT.Instance.IsNo.withThreshold_anti {conditionalTapes : } (inst : Instance) (conditionalMachine : OracleTM conditionalTapes) (parameters : Parameters) {first second : } (hthreshold : first second) (hno : (inst.withThreshold second).IsNo conditionalMachine parameters) :
(inst.withThreshold first).IsNo conditionalMachine parameters

Decreasing the stored threshold preserves a no-instance.

theorem Complexity.GapMINCKT.Instance.not_isNo_of_isYes {ordinaryTapes conditionalTapes : } (inst : Instance) (ordinaryMachine : TM ordinaryTapes) (conditionalMachine : OracleTM conditionalTapes) (parameters : Parameters) (hwidening : parameters.IsWidening) (hyes : inst.IsYes ordinaryMachine conditionalMachine parameters) :
¬inst.IsNo conditionalMachine parameters

Widening the clock prevents a depth-adjusted yes-instance from also satisfying the logarithmic no condition.

theorem Complexity.GapMINCKT.Estimator.SatisfiesBounds.le_threshold_of_isYes {ordinaryTapes conditionalTapes : } {ordinaryMachine : TM ordinaryTapes} {conditionalMachine : OracleTM conditionalTapes} {parameters : Parameters} {estimate : Estimator} (hestimate : estimate.SatisfiesBounds ordinaryMachine conditionalMachine parameters) (inst : Instance) (hyes : inst.IsYes ordinaryMachine conditionalMachine parameters) :
estimate inst.base inst.threshold

The estimator's upper sandwich bound places it below the threshold of every depth-adjusted yes-instance.

theorem Complexity.GapMINCKT.Estimator.SatisfiesBounds.threshold_lt_of_isNo {ordinaryTapes conditionalTapes : } {ordinaryMachine : TM ordinaryTapes} {conditionalMachine : OracleTM conditionalTapes} {parameters : Parameters} {estimate : Estimator} (hestimate : estimate.SatisfiesBounds ordinaryMachine conditionalMachine parameters) (inst : Instance) (hno : inst.IsNo conditionalMachine parameters) :
inst.threshold < estimate inst.base

The estimator's lower sandwich bound places it strictly above the threshold of every logarithmic no-instance.

@[simp]
theorem Complexity.GapMINCKT.mem_yesLanguage_encode_iff {ordinaryTapes conditionalTapes : } (ordinaryMachine : TM ordinaryTapes) (conditionalMachine : OracleTM conditionalTapes) (parameters : Parameters) (inst : Instance) :
inst.encode yesLanguage ordinaryMachine conditionalMachine parameters inst.IsYes ordinaryMachine conditionalMachine parameters

Canonical yes-language membership is the depth-adjusted upper bound.

@[simp]
theorem Complexity.GapMINCKT.mem_noLanguage_encode_iff {conditionalTapes : } (conditionalMachine : OracleTM conditionalTapes) (parameters : Parameters) (inst : Instance) :
inst.encode noLanguage conditionalMachine parameters inst.IsNo conditionalMachine parameters

Canonical no-language membership is the transformed-clock lower bound.

theorem Complexity.GapMINCKT.disjoint_yesLanguage_noLanguage {ordinaryTapes conditionalTapes : } (ordinaryMachine : TM ordinaryTapes) (conditionalMachine : OracleTM conditionalTapes) (parameters : Parameters) (hwidening : parameters.IsWidening) :
Disjoint (yesLanguage ordinaryMachine conditionalMachine parameters) (noLanguage conditionalMachine parameters)

Under clock widening, the two encoded gap languages are disjoint.

@[simp]

On canonical codes, the estimator completion accepts exactly when its value is at most the stored threshold.

Executable estimator thresholding is the characteristic function of its completion language.

theorem Complexity.GapMINCKT.Estimator.SatisfiesBounds.yesLanguage_subset {ordinaryTapes conditionalTapes : } {ordinaryMachine : TM ordinaryTapes} {conditionalMachine : OracleTM conditionalTapes} {parameters : Parameters} {estimate : Estimator} (hestimate : estimate.SatisfiesBounds ordinaryMachine conditionalMachine parameters) :
yesLanguage ordinaryMachine conditionalMachine parametersestimatorLanguage estimate

A valid estimator's completion contains every promised yes-instance.

theorem Complexity.GapMINCKT.Estimator.SatisfiesBounds.disjoint_noLanguage {ordinaryTapes conditionalTapes : } {ordinaryMachine : TM ordinaryTapes} {conditionalMachine : OracleTM conditionalTapes} {parameters : Parameters} {estimate : Estimator} (hestimate : estimate.SatisfiesBounds ordinaryMachine conditionalMachine parameters) :
Disjoint (estimatorLanguage estimate) (noLanguage conditionalMachine parameters)

A valid estimator's completion excludes every promised no-instance.

theorem Complexity.GapMINCKT.Estimator.SatisfiesBounds.decision_eq_true_of_mem_yesLanguage {ordinaryTapes conditionalTapes : } {ordinaryMachine : TM ordinaryTapes} {conditionalMachine : OracleTM conditionalTapes} {parameters : Parameters} {estimate : Estimator} (hestimate : estimate.SatisfiesBounds ordinaryMachine conditionalMachine parameters) {bits : List Bool} (hyes : bits yesLanguage ordinaryMachine conditionalMachine parameters) :
decisionOfEstimator estimate bits = true

Thresholding a valid estimator accepts every promised yes-instance.

theorem Complexity.GapMINCKT.Estimator.SatisfiesBounds.decision_eq_false_of_mem_noLanguage {ordinaryTapes conditionalTapes : } {ordinaryMachine : TM ordinaryTapes} {conditionalMachine : OracleTM conditionalTapes} {parameters : Parameters} {estimate : Estimator} (hestimate : estimate.SatisfiesBounds ordinaryMachine conditionalMachine parameters) {bits : List Bool} (hno : bits noLanguage conditionalMachine parameters) :

Thresholding a valid estimator rejects every promised no-instance.

def Complexity.GapMINCKT {ordinaryTapes conditionalTapes : } (ordinaryMachine : TM ordinaryTapes) (conditionalMachine : OracleTM conditionalTapes) (parameters : GapMINCKT.Parameters) (hwidening : parameters.IsWidening) :

Hirahara's widening-certified depth-adjusted conditional MinKT promise.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem Complexity.GapMINCKT_yesInstances {ordinaryTapes conditionalTapes : } (ordinaryMachine : TM ordinaryTapes) (conditionalMachine : OracleTM conditionalTapes) (parameters : GapMINCKT.Parameters) (hwidening : parameters.IsWidening) :
    (GapMINCKT ordinaryMachine conditionalMachine parameters hwidening).yesInstances = GapMINCKT.yesLanguage ordinaryMachine conditionalMachine parameters

    The promise's yes side is definitionally the canonical depth-adjusted language.

    @[simp]
    theorem Complexity.GapMINCKT_noInstances {ordinaryTapes conditionalTapes : } (ordinaryMachine : TM ordinaryTapes) (conditionalMachine : OracleTM conditionalTapes) (parameters : GapMINCKT.Parameters) (hwidening : parameters.IsWidening) :
    (GapMINCKT ordinaryMachine conditionalMachine parameters hwidening).noInstances = GapMINCKT.noLanguage conditionalMachine parameters

    The promise's no side is definitionally the canonical transformed-clock language.

    theorem Complexity.GapMINCKT_solvedBy_decisionOfEstimator {ordinaryTapes conditionalTapes : } {ordinaryMachine : TM ordinaryTapes} {conditionalMachine : OracleTM conditionalTapes} {parameters : GapMINCKT.Parameters} (hwidening : parameters.IsWidening) {estimate : GapMINCKT.Estimator} (hestimate : estimate.SatisfiesBounds ordinaryMachine conditionalMachine parameters) :
    (GapMINCKT ordinaryMachine conditionalMachine parameters hwidening).SolvedBy (GapMINCKT.decisionOfEstimator estimate)

    Proposition 6.2's numerical core: thresholding any function satisfying the two-sided conditional-complexity sandwich solves the exact gap promise.

    theorem Complexity.GapMINCKT_mem_PromiseP_of_estimatorLanguage_mem_P {ordinaryTapes conditionalTapes : } {ordinaryMachine : TM ordinaryTapes} {conditionalMachine : OracleTM conditionalTapes} {parameters : GapMINCKT.Parameters} (hwidening : parameters.IsWidening) {estimate : GapMINCKT.Estimator} (hestimate : estimate.SatisfiesBounds ordinaryMachine conditionalMachine parameters) (hpolynomial : GapMINCKT.estimatorLanguage estimate P) :
    GapMINCKT ordinaryMachine conditionalMachine parameters hwidening PromiseP

    If a valid estimator's threshold language is in P, it is a deterministic polynomial-time completion of the conditional gap promise. This isolates the remaining algorithmic obligation in Proposition 6.2.