Multiplicative-gap conditional MinKT -- proof internals #
theorem
Complexity.GapMINCKT.Multiplicative.isNo_iff_no_relaxedWitness_internal
{conditionalTapes : ℕ}
(inst : Instance)
(conditionalMachine : OracleTM conditionalTapes)
(parameters : Parameters)
(factor : ℕ → ℕ)
:
theorem
Complexity.GapMINCKT.Multiplicative.isNo_implies_additive_internal
{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
theorem
Complexity.GapMINCKT.Multiplicative.isNo_factor_anti_internal
{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
theorem
Complexity.GapMINCKT.Multiplicative.not_isNo_of_isYes_internal
{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)
:
theorem
Complexity.GapMINCKT.Multiplicative.noLanguage_mem_encode_iff_internal
{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_internal
{conditionalTapes : ℕ}
(conditionalMachine : OracleTM conditionalTapes)
(parameters : Parameters)
(factor : ℕ → ℕ)
(hfactor : ∀ (length : ℕ), 1 ≤ factor length)
:
noLanguage conditionalMachine parameters factor ⊆ GapMINCKT.noLanguage conditionalMachine parameters
theorem
Complexity.GapMINCKT.Multiplicative.noLanguage_factor_anti_internal
{conditionalTapes : ℕ}
(conditionalMachine : OracleTM conditionalTapes)
(parameters : Parameters)
{first second : ℕ → ℕ}
(hfactor : ∀ (length : ℕ), first length ≤ second length)
:
noLanguage conditionalMachine parameters second ⊆ noLanguage conditionalMachine parameters first
theorem
Complexity.GapMINCKT.Multiplicative.noLanguage_one_internal
{conditionalTapes : ℕ}
(conditionalMachine : OracleTM conditionalTapes)
(parameters : Parameters)
:
(noLanguage conditionalMachine parameters fun (_length : ℕ) => 1) = GapMINCKT.noLanguage conditionalMachine parameters
theorem
Complexity.GapMINCKT.Multiplicative.disjoint_yesLanguage_noLanguage_internal
{ordinaryTapes conditionalTapes : ℕ}
(ordinaryMachine : TM ordinaryTapes)
(conditionalMachine : OracleTM conditionalTapes)
(parameters : Parameters)
(factor : ℕ → ℕ)
(hwidening : parameters.IsWidening)
(hfactor : ∀ (length : ℕ), 1 ≤ factor length)
:
Disjoint (yesLanguage ordinaryMachine conditionalMachine parameters) (noLanguage conditionalMachine parameters factor)