Anti-checker generator output padding -- proof internals

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.unpackSample_padPackedSamples_internal {sourceCount targetCount arity : ℕ} (hbudget : sourceCount ≤ targetCount) (input : BitString (sourceCount * arity)) (sample : Fin targetCount) : unpackSample (padPackedSamples hbudget input) sample = Fin.append (fun (x : Fin (targetCount - sourceCount)) (x_1 : Fin arity) => false) (unpackSample input) (Fin.cast ⋯ sample)

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.unpackSamples_padPackedSamples_internal {sourceCount targetCount arity : ℕ} (hbudget : sourceCount ≤ targetCount) (input : BitString (sourceCount * arity)) : unpackSamples (padPackedSamples hbudget input) = AntiChecker.padInputsTo targetCount (unpackSamples input)

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.eval_packedSamplePaddingSource_internal {sourceCount targetCount arity : ℕ} (hbudget : sourceCount ≤ targetCount) (input : BitString (sourceCount * arity)) (output : Fin (targetCount * arity)) : (packedSamplePaddingSource hbudget output).eval input = padPackedSamples hbudget input output

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.eval_packedSamplePaddingCircuit_internal {sourceCount targetCount arity : ℕ} [NeZero (sourceCount * arity)] [NeZero (targetCount * arity)] (hbudget : sourceCount ≤ targetCount) (input : BitString (sourceCount * arity)) : (packedSamplePaddingCircuit hbudget).eval input = padPackedSamples hbudget input

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.size_packedSamplePaddingCircuit_internal {sourceCount targetCount arity : ℕ} [NeZero (sourceCount * arity)] [NeZero (targetCount * arity)] (hbudget : sourceCount ≤ targetCount) : (packedSamplePaddingCircuit hbudget).size = targetCount * arity

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.eval_paddedSelectionCircuit_internal {overhead arity : ℕ} {beta : PositiveRationalScale} [NeZero arity] (family : ApproximateCounterFamily overhead beta arity) (hbudget : requiredRoundCount beta arity ≤ sampleCount beta arity) (table : BitString (2 ^ arity)) : (paddedSelectionCircuit family hbudget).snd.eval table = padPackedSamples hbudget ((fullSelectionSamplesCircuit family).snd.eval table)

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.size_paddedSelectionCircuit_internal {overhead arity : ℕ} {beta : PositiveRationalScale} [NeZero arity] (family : ApproximateCounterFamily overhead beta arity) (hbudget : requiredRoundCount beta arity ≤ sampleCount beta arity) : (paddedSelectionCircuit family hbudget).snd.size = (fullSelectionSamplesCircuit family).snd.size + outputBitCount beta arity

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.exists_eval_paddedSelectionCircuit_isEstimateSelectionTrace_internal {overhead arity : ℕ} {beta : PositiveRationalScale} [NeZero arity] (family : ApproximateCounterFamily overhead beta arity) (hbudget : requiredRoundCount beta arity ≤ sampleCount beta arity) (target : BitString arity → Bool) : ∃ (inputs : Fin (requiredRoundCount beta arity) → BitString arity), unpackSamples ((paddedSelectionCircuit family hbudget).snd.eval (truthTable target)) = AntiChecker.padInputsTo (sampleCount beta arity) (List.ofFn inputs) ∧ AntiChecker.IsEstimateSelectionTrace (family.extensionEstimator target) (List.ofFn inputs)

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.eventually_eval_paddedSelectionCircuit_isFor_of_correctCounterFamily_internal (beta : PositiveRationalScale) : ∀ᶠ (arity : ℕ) in Filter.atTop, ∀ (harity : arity ≠ 0) (overhead : ℕ) (family : ApproximateCounterFamily overhead beta arity) (hbudget : requiredRoundCount beta arity ≤ sampleCount beta arity), family.IsCorrect → ∀ (target : BitString arity → Bool), IsHardAt beta target → AntiChecker.IsFor target (smallThreshold beta arity) (unpackSamples ((paddedSelectionCircuit family hbudget).snd.eval (truthTable target)))