Multiplicative-gap conditional MinKT

This module formalizes Definition 6.5's multiplicative no threshold, its exact program semantics, factor monotonicity, disjoint promise, and relation to the additive GapMINCKT problem. A larger factor narrows the no side; therefore the resulting multiplicative promise side-preservingly reduces to the additive factor-one promise by the identity map.

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

The multiplicative no condition exactly forbids descriptions meeting its relaxed length and transformed-time bounds.

theorem Complexity.GapMINCKT.Multiplicative.IsNo.implies_additive {conditionalTapes : ℕ} {inst : Instance} {conditionalMachine : OracleTM conditionalTapes} {parameters : Parameters} {factor : ℕ → ℕ} (hfactor : 1 ≤ factor inst.output.length) (hno : IsNo inst conditionalMachine parameters factor) : inst.IsNo conditionalMachine parameters

Any multiplicative no-instance with factor at least one is an additive no-instance.

theorem Complexity.GapMINCKT.Multiplicative.IsNo.factor_anti {conditionalTapes : ℕ} {inst : Instance} {conditionalMachine : OracleTM conditionalTapes} {parameters : Parameters} {first second : ℕ → ℕ} (hfactor : first inst.output.length ≤ second inst.output.length) (hno : IsNo inst conditionalMachine parameters second) : IsNo inst conditionalMachine parameters first

Increasing the approximation factor can only narrow the no side.

theorem Complexity.GapMINCKT.Multiplicative.not_isNo_of_isYes {ordinaryTapes conditionalTapes : ℕ} (inst : Instance) (ordinaryMachine : TM ordinaryTapes) (conditionalMachine : OracleTM conditionalTapes) (parameters : Parameters) (factor : ℕ → ℕ) (hwidening : parameters.IsWidening) (hfactor : 1 ≤ factor inst.output.length) (hyes : inst.IsYes ordinaryMachine conditionalMachine parameters) : ¬IsNo inst conditionalMachine parameters factor

Widening and a factor of at least one prevent overlap with the depth-adjusted yes side.

@[simp]

theorem Complexity.GapMINCKT.Multiplicative.mem_noLanguage_encode_iff {conditionalTapes : ℕ} (conditionalMachine : OracleTM conditionalTapes) (parameters : Parameters) (factor : ℕ → ℕ) (inst : Instance) : inst.encode ∈ noLanguage conditionalMachine parameters factor ↔ IsNo inst conditionalMachine parameters factor

theorem Complexity.GapMINCKT.Multiplicative.noLanguage_subset_additive {conditionalTapes : ℕ} (conditionalMachine : OracleTM conditionalTapes) (parameters : Parameters) (factor : ℕ → ℕ) (hfactor : ∀ (length : ℕ), 1 ≤ factor length) : noLanguage conditionalMachine parameters factor ⊆ GapMINCKT.noLanguage conditionalMachine parameters

The multiplicative no language is contained in the additive no language when the factor is at least one.

theorem Complexity.GapMINCKT.Multiplicative.noLanguage_factor_anti {conditionalTapes : ℕ} (conditionalMachine : OracleTM conditionalTapes) (parameters : Parameters) {first second : ℕ → ℕ} (hfactor : ∀ (length : ℕ), first length ≤ second length) : noLanguage conditionalMachine parameters second ⊆ noLanguage conditionalMachine parameters first

Pointwise larger factors give pointwise smaller no languages.

@[simp]

theorem Complexity.GapMINCKT.Multiplicative.noLanguage_one {conditionalTapes : ℕ} (conditionalMachine : OracleTM conditionalTapes) (parameters : Parameters) : (noLanguage conditionalMachine parameters fun (_length : ℕ) => 1) = GapMINCKT.noLanguage conditionalMachine parameters

Factor one recovers the additive no language exactly.

def Complexity.GapMINCKT.Multiplicative.problem {ordinaryTapes conditionalTapes : ℕ} (ordinaryMachine : TM ordinaryTapes) (conditionalMachine : OracleTM conditionalTapes) (parameters : Parameters) (factor : ℕ → ℕ) (hwidening : parameters.IsWidening) (hfactor : ∀ (length : ℕ), 1 ≤ factor length) : PromiseProblem

Definition 6.5's widening-certified multiplicative promise.

Equations

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

@[simp]

theorem Complexity.GapMINCKT.Multiplicative.problem_yesInstances {ordinaryTapes conditionalTapes : ℕ} (ordinaryMachine : TM ordinaryTapes) (conditionalMachine : OracleTM conditionalTapes) (parameters : Parameters) (factor : ℕ → ℕ) (hwidening : parameters.IsWidening) (hfactor : ∀ (length : ℕ), 1 ≤ factor length) : (problem ordinaryMachine conditionalMachine parameters factor hwidening hfactor).yesInstances = yesLanguage ordinaryMachine conditionalMachine parameters

@[simp]

theorem Complexity.GapMINCKT.Multiplicative.problem_noInstances {ordinaryTapes conditionalTapes : ℕ} (ordinaryMachine : TM ordinaryTapes) (conditionalMachine : OracleTM conditionalTapes) (parameters : Parameters) (factor : ℕ → ℕ) (hwidening : parameters.IsWidening) (hfactor : ∀ (length : ℕ), 1 ≤ factor length) : (problem ordinaryMachine conditionalMachine parameters factor hwidening hfactor).noInstances = noLanguage conditionalMachine parameters factor

theorem Complexity.GapMINCKT.Multiplicative.mapReducesVia_additive {ordinaryTapes conditionalTapes : ℕ} (ordinaryMachine : TM ordinaryTapes) (conditionalMachine : OracleTM conditionalTapes) (parameters : Parameters) (factor : ℕ → ℕ) (hwidening : parameters.IsWidening) (hfactor : ∀ (length : ℕ), 1 ≤ factor length) : (problem ordinaryMachine conditionalMachine parameters factor hwidening hfactor).MapReducesVia (GapMINCKT ordinaryMachine conditionalMachine parameters hwidening) id

The identity map side-preservingly reduces every factor-at-least-one multiplicative promise to the additive factor-one promise.

theorem Complexity.GapMINCKT.Multiplicative.mapReducesPoly_additive {ordinaryTapes conditionalTapes : ℕ} (ordinaryMachine : TM ordinaryTapes) (conditionalMachine : OracleTM conditionalTapes) (parameters : Parameters) (factor : ℕ → ℕ) (hwidening : parameters.IsWidening) (hfactor : ∀ (length : ℕ), 1 ≤ factor length) : (problem ordinaryMachine conditionalMachine parameters factor hwidening hfactor).MapReducesPoly (GapMINCKT ordinaryMachine conditionalMachine parameters hwidening)

The semantic identity reduction is polynomial time.

theorem Complexity.GapMINCKT.Multiplicative.promiseNPHard_additive {ordinaryTapes conditionalTapes : ℕ} (ordinaryMachine : TM ordinaryTapes) (conditionalMachine : OracleTM conditionalTapes) (parameters : Parameters) (factor : ℕ → ℕ) (hwidening : parameters.IsWidening) (hfactor : ∀ (length : ℕ), 1 ≤ factor length) (hhard : PromiseNPHard (problem ordinaryMachine conditionalMachine parameters factor hwidening hfactor)) : PromiseNPHard (GapMINCKT ordinaryMachine conditionalMachine parameters hwidening)

NP-hardness of a factor-at-least-one multiplicative gap transfers to the additive factor-one promise. The direction follows the narrowing of the multiplicative no side.

theorem Complexity.GapMINCKT.Multiplicative.P_eq_NP_of_hard_of_additive_mem_PromiseP {ordinaryTapes conditionalTapes : ℕ} (ordinaryMachine : TM ordinaryTapes) (conditionalMachine : OracleTM conditionalTapes) (parameters : Parameters) (factor : ℕ → ℕ) (hwidening : parameters.IsWidening) (hfactor : ∀ (length : ℕ), 1 ≤ factor length) (hhard : PromiseNPHard (problem ordinaryMachine conditionalMachine parameters factor hwidening hfactor)) (hmembership : GapMINCKT ordinaryMachine conditionalMachine parameters hwidening ∈ PromiseP) : P = NP

If the multiplicative conditional gap is NP-hard while the corresponding additive gap has a deterministic polynomial-time completion, then P = NP.

theorem Complexity.GapMINCKT.Multiplicative.P_eq_NP_of_hard_of_estimatorLanguage_mem_P {ordinaryTapes conditionalTapes : ℕ} (ordinaryMachine : TM ordinaryTapes) (conditionalMachine : OracleTM conditionalTapes) (parameters : Parameters) (factor : ℕ → ℕ) (hwidening : parameters.IsWidening) (hfactor : ∀ (length : ℕ), 1 ≤ factor length) (hhard : PromiseNPHard (problem ordinaryMachine conditionalMachine parameters factor hwidening hfactor)) {estimate : Estimator} (hestimate : estimate.SatisfiesBounds ordinaryMachine conditionalMachine parameters) (hpolynomial : estimatorLanguage estimate ∈ P) : P = NP

A valid conditional-complexity estimator whose threshold language is in P rules out NP-hardness of the corresponding multiplicative gap unless P = NP. This is the promise-hardness endpoint of the SoI estimator route.