Documentation

Complexitylib.Metacomplexity.MCSP.Magnification.Parameters

GapMCSP hardness-magnification parameters #

This module exposes the exact finite raw GapMCSP family selected for the first hardness-magnification target. Its floor-rounded yes/no thresholds always form a promise gap, floor-to-ceiling exponent changes cost at most a factor of two, and the rounded solver bound agrees exactly with its arity form on N = 2^n inputs.

source
@[simp]
theorem Complexity.GapMCSP.Magnification.Parameters.yesThreshold_zero (parameters : Parameters) :
parameters.yesThreshold 0 = 0

At arity zero, division by c*n makes the yes threshold zero.

source
@[simp]
theorem Complexity.GapMCSP.Magnification.Parameters.noThreshold_zero (parameters : Parameters) :
parameters.noThreshold 0 = 1

At arity zero, the no threshold is 2^0 = 1.

source
theorem Complexity.GapMCSP.Magnification.Parameters.yesThreshold_le_noThreshold (parameters : Parameters) (arity : ℕ) :
parameters.yesThreshold arity ≤ parameters.noThreshold arity

The finite yes threshold never exceeds the no threshold.

source
theorem Complexity.GapMCSP.Magnification.Parameters.sliceParameters_isGap (parameters : Parameters) :
parameters.sliceParameters.IsGap

The selected thresholds form a valid GapMCSP slice at every arity.

source
@[simp]
theorem Complexity.GapMCSP.Magnification.Parameters.sliceParameters_yesThreshold (parameters : Parameters) :
parameters.sliceParameters.yesThreshold = parameters.yesThreshold
source
@[simp]
theorem Complexity.GapMCSP.Magnification.Parameters.sliceParameters_noThreshold (parameters : Parameters) :
parameters.sliceParameters.noThreshold = parameters.noThreshold
source
theorem Complexity.GapMCSP.Magnification.Parameters.yesThreshold_mul_denominator_le_noThreshold (parameters : Parameters) (arity : ℕ) :
parameters.yesThreshold arity * (parameters.constant * arity) ≤ parameters.noThreshold arity

Restoring the denominator after natural division stays below the no threshold.

source
theorem Complexity.GapMCSP.Magnification.Parameters.noThreshold_pos (parameters : Parameters) (arity : ℕ) :
0 < parameters.noThreshold arity

The large-circuit threshold is always positive.

source
theorem Complexity.GapMCSP.Magnification.Parameters.yesThreshold_pos_of_denominator_le (parameters : Parameters) {arity : ℕ} (harity : 0 < arity) (hdenominator : parameters.constant * arity ≤ parameters.beta.powFloor arity) :
0 < parameters.yesThreshold arity

The small-circuit threshold is positive once its natural divisor fits below the rounded binary exponential.

source
theorem Complexity.GapMCSP.Magnification.Parameters.eventually_denominator_le_powFloor (parameters : Parameters) :
∀ᶠ (arity : ℕ) in Filter.atTop, parameters.constant * arity ≤ parameters.beta.powFloor arity

The rounded binary exponential eventually dominates the selected linear denominator c*n.

source
theorem Complexity.GapMCSP.Magnification.Parameters.eventually_yesThreshold_pos (parameters : Parameters) :
∀ᶠ (arity : ℕ) in Filter.atTop, 0 < parameters.yesThreshold arity

The selected small-circuit threshold is positive at every sufficiently large arity.

source
theorem Complexity.GapMCSP.Magnification.Parameters.noThreshold_le_powCeil (parameters : Parameters) (arity : ℕ) :
parameters.noThreshold arity ≤ parameters.beta.powCeil arity

Floor rounding puts the no threshold below the ceiling-rounded power.

source
theorem Complexity.GapMCSP.Magnification.Parameters.powCeil_le_two_mul_noThreshold (parameters : Parameters) (arity : ℕ) :
parameters.beta.powCeil arity ≤ 2 * parameters.noThreshold arity

Ceiling rounding increases the no threshold by at most a factor of two.

source
@[simp]
theorem Complexity.GapMCSP.Magnification.circuitBound_pow (epsilon : PositiveRationalScale) (arity : ℕ) :
circuitBound epsilon (2 ^ arity) = circuitBoundAtArity epsilon arity

On raw length N = 2^n, the rounded N^(1+epsilon) bound agrees exactly with its arity-indexed presentation.

source
theorem Complexity.GapMCSP.Magnification.circuitBound_tableBits (epsilon : PositiveRationalScale) (inst : MCSP.Instance) :
circuitBound epsilon inst.tableBits.length = circuitBoundAtArity epsilon inst.arity

The solver bound on a canonical table payload depends on its represented arity exactly as intended.

source
theorem Complexity.GapMCSP.Magnification.truthTableLength_le_circuitBoundAtArity (epsilon : PositiveRationalScale) (arity : ℕ) :
2 ^ arity ≤ circuitBoundAtArity epsilon arity

A slightly-superlinear solver bound is at least the raw truth-table length.

source
def Complexity.GapMCSP.Magnification.Parameters.rawProblem (parameters : Parameters) :
PromiseProblem

The selected finite raw GapMCSP promise at exponent beta and constant c.

Equations
Instances For
    source
    @[simp]
    theorem Complexity.GapMCSP.Magnification.Parameters.rawProblem_yesInstances (parameters : Parameters) :
    parameters.rawProblem.yesInstances = rawSliceYesLanguage parameters.sliceParameters
    source
    @[simp]
    theorem Complexity.GapMCSP.Magnification.Parameters.rawProblem_noInstances (parameters : Parameters) :
    parameters.rawProblem.noInstances = rawSliceNoLanguage parameters.sliceParameters
    source
    theorem Complexity.GapMCSP.Magnification.Parameters.mem_rawProblem_yesInstances_tableBits_iff (parameters : Parameters) (inst : MCSP.Instance) :
    inst.tableBits ∈ parameters.rawProblem.yesInstances ↔ inst.minimumSize ≤ parameters.yesThreshold inst.arity

    Exact minimum-size semantics of the selected yes side.

    source
    theorem Complexity.GapMCSP.Magnification.Parameters.mem_rawProblem_noInstances_tableBits_iff (parameters : Parameters) (inst : MCSP.Instance) :
    inst.tableBits ∈ parameters.rawProblem.noInstances ↔ parameters.noThreshold inst.arity < inst.minimumSize

    Exact minimum-size semantics of the selected no side.

    source
    theorem Complexity.GapMCSP.Magnification.Parameters.mem_rawProblem_promise_imp_isRawTruthTable (parameters : Parameters) {bits : List Bool} (hmem : bits ∈ parameters.rawProblem.promise) :
    MCSP.IsRawTruthTable bits

    Every promised input in the selected finite family has raw length 2^n.

    source
    def Complexity.GapMCSP.Magnification.Parameters.HasPointwiseCircuitLowerBound (parameters : Parameters) (epsilon : PositiveRationalScale) :
    Prop

    The selected raw problem has a pointwise circuit lower bound at exponent 1+epsilon.

    Equations
    Instances For
      source
      def Complexity.GapMCSP.Magnification.Parameters.HasEventualCircuitLowerBound (parameters : Parameters) (epsilon : PositiveRationalScale) :
      Prop

      The selected raw problem has a circuit lower bound even when finitely many exceptional input lengths are allowed.

      Equations
      Instances For
        source
        theorem Complexity.GapMCSP.Magnification.Parameters.HasEventualCircuitLowerBound.pointwise {parameters : Parameters} {epsilon : PositiveRationalScale} (hlower : parameters.HasEventualCircuitLowerBound epsilon) :
        parameters.HasPointwiseCircuitLowerBound epsilon

        An eventual lower bound implies the corresponding pointwise lower bound.