Typed Anti-Checker Lemma generators -- definitions

An Anti-Checker Lemma generator is a multi-output circuit whose input is an n-variable truth table and whose packed output contains exactly the selected number of n-bit sample points. Its semantic contract is universal in the input truth table: whenever the represented function is hard at the large threshold, the printed points anti-check it at the smaller threshold.

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.unpackSample {count arity : ℕ} (output : BitString (count * arity)) (sample : Fin count) : BitString arity

Read one fixed-width sample from a row-major packed bit string.

Equations

• Complexity.GapMCSP.Magnification.AntiCheckerLemma.unpackSample output sample coordinate = output (finProdFinEquiv (sample, coordinate))

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.unpackSamples {count arity : ℕ} (output : BitString (count * arity)) : List (BitString arity)

Split a packed output into its ordered list of fixed-width samples.

Equations

• Complexity.GapMCSP.Magnification.AntiCheckerLemma.unpackSamples output = List.ofFn (Complexity.GapMCSP.Magnification.AntiCheckerLemma.unpackSample output)

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.truthTable {arity : ℕ} (target : BitString arity → Bool) : BitString (2 ^ arity)

Canonical little-endian truth-table input expected by the generator.

Equations

• Complexity.GapMCSP.Magnification.AntiCheckerLemma.truthTable target = (Complexity.MCSP.Instance.ofFunction arity 0 target).table

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.IsHardAt {arity : ℕ} (beta : PositiveRationalScale) (target : BitString arity → Bool) : Prop

The target has no circuit at the large threshold.

Equations

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

structure Complexity.GapMCSP.Magnification.AntiCheckerLemma.Generator (overhead : ℕ) (beta : PositiveRationalScale) (arity : ℕ) [NeZero arity] : Type

A typed multi-output circuit with the exact input width, output width, and rounded size bound from the Anti-Checker Lemma.

• internalGates : ℕ

  Number of internal gates in the generator circuit.

• circuit : Circuit Basis.andOr2 (2 ^ arity) (outputBitCount beta arity) self.internalGates

  Circuit mapping a truth table to the packed sample inputs.

• size_le : self.circuit.size ≤ generatorSizeBound overhead beta arity

  Published ceiling-rounded size bound.

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.Generator.inputs {overhead arity : ℕ} {beta : PositiveRationalScale} [NeZero arity] (generator : Generator overhead beta arity) (table : BitString (2 ^ arity)) : List (BitString arity)

Run the generator on a packed truth table and unpack its sample inputs.

Equations

• generator.inputs table = Complexity.GapMCSP.Magnification.AntiCheckerLemma.unpackSamples (generator.circuit.eval table)

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.Generator.inputsFor {overhead arity : ℕ} {beta : PositiveRationalScale} [NeZero arity] (generator : Generator overhead beta arity) (target : BitString arity → Bool) : List (BitString arity)

Run the generator on the canonical truth table of a target function.

Equations

• generator.inputsFor target = generator.inputs (Complexity.GapMCSP.Magnification.AntiCheckerLemma.truthTable target)

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.Generator.IsCorrect {overhead arity : ℕ} {beta : PositiveRationalScale} [NeZero arity] (generator : Generator overhead beta arity) : Prop

The generator prints an anti-checker for every target hard at the large threshold.

Equations

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

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.ExistsCorrectGeneratorAt (overhead : ℕ) (beta : PositiveRationalScale) (arity : ℕ) : Prop

A total arity-indexed assertion that handles the circuit model's positive input and output arity requirements explicitly.

Equations

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

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.HasGenerators : Prop

Quantifier structure of the Anti-Checker Lemma's conclusion: one natural overhead constant works for every sufficiently small positive beta and all sufficiently large truth-table arities.

Equations

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