Typed Anti-Checker Lemma generators -- proof internals

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

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

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

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

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

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

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

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

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

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.Generator.isCorrect_iff_encode_not_mem_internal {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

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

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