Documentation

Complexitylib.Metacomplexity.MCSP.Gap.Slice

Arity-indexed Gap MCSP slices #

This module exposes canonical GapMCSP[s_yes, s_no] promises. Its reduction theorem keeps the represented truth table fixed, writes the target yes threshold into the code, and exposes the two exact inequalities needed for side preservation.

source
theorem Complexity.GapMCSP.SliceParameters.reducesTo_refl (parameters : SliceParameters) :
parameters.ReducesTo parameters

Every threshold pair reduces to itself.

source
theorem Complexity.GapMCSP.SliceParameters.ReducesTo.trans {first second third : SliceParameters} (hfirst : first.ReducesTo second) (hsecond : second.ReducesTo third) :
first.ReducesTo third

Parameter order composes.

source
@[simp]
theorem Complexity.GapMCSP.mem_sliceYesLanguage_encode_iff (parameters : SliceParameters) (inst : MCSP.Instance) :
inst.encode ∈ sliceYesLanguage parameters ↔ inst.threshold = parameters.yesThreshold inst.arity ∧ inst.HasCircuitAtMost

Membership in the encoded yes slice exposes its forced threshold and MCSP witness predicate.

source
@[simp]
theorem Complexity.GapMCSP.mem_sliceNoLanguage_encode_iff (parameters : SliceParameters) (inst : MCSP.Instance) :
inst.encode ∈ sliceNoLanguage parameters ↔ inst.threshold = parameters.yesThreshold inst.arity ∧ parameters.noThreshold inst.arity < inst.minimumSize

Membership in the encoded no slice exposes both finite thresholds.

source
theorem Complexity.GapMCSP.disjoint_sliceLanguages (parameters : SliceParameters) (hgap : parameters.IsGap) :
Disjoint (sliceYesLanguage parameters) (sliceNoLanguage parameters)

A pointwise gap makes the two encoded slice languages disjoint.

source
def Complexity.GapMCSP.sliceProblem (parameters : SliceParameters) (hgap : parameters.IsGap) :
PromiseProblem

Canonical arity-indexed Gap MCSP promise problem.

Equations
Instances For
    source
    @[simp]
    theorem Complexity.GapMCSP.sliceProblem_yesInstances (parameters : SliceParameters) (hgap : parameters.IsGap) :
    (sliceProblem parameters hgap).yesInstances = sliceYesLanguage parameters
    source
    @[simp]
    theorem Complexity.GapMCSP.sliceProblem_noInstances (parameters : SliceParameters) (hgap : parameters.IsGap) :
    (sliceProblem parameters hgap).noInstances = sliceNoLanguage parameters
    source
    theorem Complexity.GapMCSP.sliceProblem_mapReducesVia_rethreshold {source target : SliceParameters} (hparameters : source.ReducesTo target) (hsource : source.IsGap) (htarget : target.IsGap) :
    (sliceProblem source hsource).MapReducesVia (sliceProblem target htarget) (MCSP.rethreshold target.yesThreshold)

    Exact table-preserving reduction between ordered threshold slices. The map re-encodes only the target yes threshold; MCSP.rethreshold_comp and MCSP.length_rethreshold_of_decode?_eq_some give its composition and precise output-length behavior.