The selected GapMCSP magnification frontier -- proof internals

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

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

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

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