The selected GapMCSP magnification frontier -- definitions

This layer states the nested lower-bound quantifiers from the selected Oliveira--Pich--Santhanam frontier without asserting the magnification theorem. The denominator constant is fixed first. A positive solver exponent is then chosen, and every sufficiently small positive threshold exponent must give an eventual-in-input-length circuit lower bound.

structure Complexity.GapMCSP.Magnification.DenominatorConstant : Type

A positive candidate for the universal denominator constant c in the selected GapMCSP thresholds.

• value : ℕ

  The natural value of the constant.

• value_pos : 0 < self.value

  The constant is at least one.

def Complexity.GapMCSP.Magnification.DenominatorConstant.parametersAt (constant : DenominatorConstant) (beta : PositiveRationalScale) : Parameters

Instantiate the selected finite parameters at one positive exponent beta, keeping the denominator constant fixed.

Equations

• constant.parametersAt beta = { beta := beta, constant := constant.value, constant_pos := ⋯ }

def Complexity.GapMCSP.Magnification.DenominatorConstant.HasSmallBetaCircuitLowerBound (constant : DenominatorConstant) (epsilon : PositiveRationalScale) : Prop

At fixed c and epsilon, every sufficiently small positive beta gives a raw GapMCSP problem outside eventual circuit size N^(1+epsilon).

The outer filter is over beta; HasEventualCircuitLowerBound separately allows finitely many exceptional input lengths for each selected problem.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.GapMCSP.Magnification.DenominatorConstant.HasMagnificationLowerBoundHypothesis (constant : DenominatorConstant) : Prop

The complete lower-bound antecedent at one fixed denominator constant: some positive epsilon works for every sufficiently small positive beta.

Equations

• constant.HasMagnificationLowerBoundHypothesis = ∃ (epsilon : Complexity.PositiveRationalScale), constant.HasSmallBetaCircuitLowerBound epsilon