Documentation

Complexitylib.Metacomplexity.MCSP.Gap.Slice.Internal

Arity-indexed Gap MCSP slices -- proof internals #

source
theorem Complexity.GapMCSP.SliceParameters.reducesTo_refl_internal (parameters : SliceParameters) :
parameters.ReducesTo parameters
source
theorem Complexity.GapMCSP.SliceParameters.ReducesTo.trans_internal {first second third : SliceParameters} (hfirst : first.ReducesTo second) (hsecond : second.ReducesTo third) :
first.ReducesTo third
source
theorem Complexity.GapMCSP.mem_sliceYesLanguage_encode_iff_internal (parameters : SliceParameters) (inst : MCSP.Instance) :
inst.encode ∈ sliceYesLanguage parameters ↔ inst.threshold = parameters.yesThreshold inst.arity ∧ inst.HasCircuitAtMost
source
theorem Complexity.GapMCSP.mem_sliceNoLanguage_encode_iff_internal (parameters : SliceParameters) (inst : MCSP.Instance) :
inst.encode ∈ sliceNoLanguage parameters ↔ inst.threshold = parameters.yesThreshold inst.arity ∧ parameters.noThreshold inst.arity < inst.minimumSize
source
theorem Complexity.GapMCSP.disjoint_sliceLanguages_internal (parameters : SliceParameters) (hgap : parameters.IsGap) :
Disjoint (sliceYesLanguage parameters) (sliceNoLanguage parameters)
source
theorem Complexity.GapMCSP.sliceProblem_mapReducesVia_rethreshold_internal {source target : SliceParameters} (hparameters : source.ReducesTo target) (hsource : source.IsGap) (htarget : target.IsGap) :
{ yesInstances := sliceYesLanguage source, noInstances := sliceNoLanguage source, disjoint := ⋯ }.MapReducesVia { yesInstances := sliceYesLanguage target, noInstances := sliceNoLanguage target, disjoint := ⋯ } (MCSP.rethreshold target.yesThreshold)