Typed Anti-Checker Lemma generators

This module exposes the exact multi-output generator interface from the Oliveira--Pich--Santhanam Anti-Checker Lemma and its construction from correct approximate-counter families. No theorem deriving those counter families from NP ⊆ PPoly is asserted here.

@[simp]

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.unpackSample_apply {count arity : ℕ} (output : BitString (count * arity)) (sample : Fin count) (coordinate : Fin arity) : unpackSample output sample coordinate = output (finProdFinEquiv (sample, coordinate))

Packed samples use row-major indexing.

@[simp]

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.length_unpackSamples {count arity : ℕ} (output : BitString (count * arity)) : (unpackSamples output).length = count

Unpacking produces exactly the requested number of samples.

@[simp]

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.getElem_unpackSamples {count arity : ℕ} (output : BitString (count * arity)) (sample : Fin count) : (unpackSamples output)[↑sample] = unpackSample output sample

Reading sample i after unpacking returns row i of the packed output.

@[simp]

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.truthTable_inputIndex {arity : ℕ} (target : BitString arity → Bool) (input : BitString arity) : truthTable target (MCSP.Instance.inputIndex input) = target input

The generator's canonical input table stores the target at its canonical little-endian input index.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.isHardAt_iff_minimumSize_gt {arity : ℕ} (beta : PositiveRationalScale) (target : BitString arity → Bool) : IsHardAt beta target ↔ hardThreshold beta arity < (MCSP.Instance.ofFunction arity (hardThreshold beta arity) target).minimumSize

Hardness is strict minimum circuit size above the large threshold.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.isHardAt_iff_sizeComplexity_gt {arity : ℕ} [NeZero arity] (beta : PositiveRationalScale) (target : BitString arity → Bool) : IsHardAt beta target ↔ hardThreshold beta arity < Circuit.sizeComplexity Basis.andOr2 target

At positive arity, hardness uses the library's exact fan-in-two circuit complexity measure.

@[simp]

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.Generator.length_inputs {overhead arity : ℕ} {beta : PositiveRationalScale} [NeZero arity] (generator : Generator overhead beta arity) (table : BitString (2 ^ arity)) : (generator.inputs table).length = sampleCount beta arity

Every generator run prints exactly the selected sample count.

@[simp]

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.Generator.length_inputsFor {overhead arity : ℕ} {beta : PositiveRationalScale} [NeZero arity] (generator : Generator overhead beta arity) (target : BitString arity → Bool) : (generator.inputsFor target).length = sampleCount beta arity

Target-specialized generation preserves the exact sample count.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.Generator.outputBitCount_le_sizeBound {overhead arity : ℕ} {beta : PositiveRationalScale} [NeZero arity] (generator : Generator overhead beta arity) : outputBitCount beta arity ≤ generatorSizeBound overhead beta arity

Merely printing the packed outputs already consumes no more gates than the generator's stated size bound.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.Generator.isCorrect_iff_encode_not_mem {overhead arity : ℕ} {beta : PositiveRationalScale} [NeZero arity] (generator : Generator overhead beta arity) : generator.IsCorrect ↔ ∀ (target : BitString arity → Bool), IsHardAt beta target → (SuccinctMCSP.Instance.ofInputs (smallThreshold beta arity) target (generator.inputsFor target)).encode ∉ SuccinctMCSP

Exact encoded SuccinctMCSP form of the generator's anti-checker contract.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.existsCorrectGeneratorAt_iff_of_ne (overhead : ℕ) (beta : PositiveRationalScale) {arity : ℕ} (harity : arity ≠ 0) : ExistsCorrectGeneratorAt overhead beta arity ↔ ∃ (generator : Generator overhead beta arity), generator.IsCorrect

At a nonzero arity, the total existence predicate is the expected typed generator existence statement.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.hasGenerators_iff_cutoff : HasGenerators ↔ ∃ (overhead : ℕ) (cutoff : PositiveRationalScale), ∀ beta ≤ cutoff, ∀ᶠ (arity : ℕ) in Filter.atTop, ExistsCorrectGeneratorAt overhead beta arity

Cutoff form of the small-positive-beta quantifier, retaining the independent sufficiently-large-arity quantifier.