The selected GapMCSP magnification frontier

This module exposes the exact lower-bound antecedent of the selected Oliveira--Pich--Santhanam magnification theorem. It keeps a fixed denominator constant, the small-positive-beta quantifier, and the eventual input-length circuit lower bound separate. It does not assert the conditional class separation. Of the anti-checker construction, only the circuit-assembly half is proved (AntiCheckerLemma.hasGenerators_of_hasApproximateCounterFamilies: correct approximate-counter families yield the generators). Deriving HasApproximateCounterFamilies from NP ⊆ P/poly, and the solver and magnification steps, remain to be formalized.

@[simp]

theorem Complexity.GapMCSP.Magnification.DenominatorConstant.parametersAt_beta (constant : DenominatorConstant) (beta : PositiveRationalScale) : (constant.parametersAt beta).beta = beta

@[simp]

theorem Complexity.GapMCSP.Magnification.DenominatorConstant.parametersAt_constant (constant : DenominatorConstant) (beta : PositiveRationalScale) : (constant.parametersAt beta).constant = constant.value

theorem Complexity.GapMCSP.Magnification.DenominatorConstant.hasSmallBetaCircuitLowerBound_iff (constant : DenominatorConstant) (epsilon : PositiveRationalScale) : constant.HasSmallBetaCircuitLowerBound epsilon ↔ ∃ (cutoff : PositiveRationalScale), ∀ beta ≤ cutoff, (constant.parametersAt beta).HasEventualCircuitLowerBound epsilon

The small-positive-beta lower bound is equivalently witnessed by one positive cutoff.

theorem Complexity.GapMCSP.Magnification.DenominatorConstant.HasSmallBetaCircuitLowerBound.pointwise {constant : DenominatorConstant} {epsilon : PositiveRationalScale} (hlower : constant.HasSmallBetaCircuitLowerBound epsilon) : ∀ᶠ (beta : PositiveRationalScale) in PositiveRationalScale.atZeroFromPositive, (constant.parametersAt beta).HasPointwiseCircuitLowerBound epsilon

Eventual-in-input-length lower bounds for all small beta imply the corresponding pointwise lower bounds for all small beta.

theorem Complexity.GapMCSP.Magnification.DenominatorConstant.hasMagnificationLowerBoundHypothesis_iff (constant : DenominatorConstant) : constant.HasMagnificationLowerBoundHypothesis ↔ ∃ (epsilon : PositiveRationalScale) (cutoff : PositiveRationalScale), ∀ beta ≤ cutoff, (constant.parametersAt beta).HasEventualCircuitLowerBound epsilon

Explicit cutoff form of the complete selected lower-bound antecedent at a fixed denominator constant.

theorem Complexity.GapMCSP.Magnification.DenominatorConstant.HasMagnificationLowerBoundHypothesis.pointwise {constant : DenominatorConstant} (hlower : constant.HasMagnificationLowerBoundHypothesis) : ∃ (epsilon : PositiveRationalScale), ∀ᶠ (beta : PositiveRationalScale) in PositiveRationalScale.atZeroFromPositive, (constant.parametersAt beta).HasPointwiseCircuitLowerBound epsilon

The complete eventual lower-bound hypothesis also yields a positive solver exponent with pointwise lower bounds throughout a small-beta tail.