GapMCSP hardness-magnification parameters -- proof internals

theorem Complexity.GapMCSP.Magnification.Parameters.yesThreshold_zero_internal (parameters : Parameters) : parameters.yesThreshold 0 = 0

theorem Complexity.GapMCSP.Magnification.Parameters.noThreshold_zero_internal (parameters : Parameters) : parameters.noThreshold 0 = 1

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

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

theorem Complexity.GapMCSP.Magnification.Parameters.yesThreshold_mul_denominator_le_noThreshold_internal (parameters : Parameters) (arity : ℕ) : parameters.yesThreshold arity * (parameters.constant * arity) ≤ parameters.noThreshold arity

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

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

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

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

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

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

theorem Complexity.GapMCSP.Magnification.circuitBound_pow_internal (epsilon : PositiveRationalScale) (arity : ℕ) : circuitBound epsilon (2 ^ arity) = circuitBoundAtArity epsilon arity

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

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