Finite iteration of anti-checker selection rounds -- proof internals

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.eval_selectionPrefixCircuit_zero_internal {overhead arity : ℕ} {beta : PositiveRationalScale} (family : ApproximateCounterFamily overhead beta arity) (hrounds : 0 ≤ requiredRoundCount beta arity) (table : BitString (2 ^ arity)) : (selectionPrefixCircuit family 0 hrounds).snd.eval table = selectionRoundInput table (emptyLabeledPrefix arity)

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.size_selectionPrefixCircuit_zero_internal {overhead arity : ℕ} {beta : PositiveRationalScale} (family : ApproximateCounterFamily overhead beta arity) (hrounds : 0 ≤ requiredRoundCount beta arity) : (selectionPrefixCircuit family 0 hrounds).snd.size = 2 ^ arity

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.eval_selectionPrefixCircuit_succ_internal {overhead arity rounds : ℕ} {beta : PositiveRationalScale} (family : ApproximateCounterFamily overhead beta arity) (hrounds : rounds + 1 ≤ requiredRoundCount beta arity) (table : BitString (2 ^ arity)) : (selectionPrefixCircuit family (rounds + 1) hrounds).snd.eval table = (selectionRoundStateCircuit (family.counter (selectionPrefixCounterIndex hrounds))).snd.eval ((selectionPrefixCircuit family rounds ⋯).snd.eval table)

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.size_selectionPrefixCircuit_succ_internal {overhead arity rounds : ℕ} {beta : PositiveRationalScale} (family : ApproximateCounterFamily overhead beta arity) (hrounds : rounds + 1 ≤ requiredRoundCount beta arity) : (selectionPrefixCircuit family (rounds + 1) hrounds).snd.size = (selectionPrefixCircuit family rounds ⋯).snd.size + (selectionRoundStateCircuit (family.counter (selectionPrefixCounterIndex hrounds))).snd.size

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.candidateLabeledSamples_truthTable_packTargetSamples_internal {arity prefixLength : ℕ} (target : BitString arity → Bool) (inputs : Fin prefixLength → BitString arity) (input : BitString arity) : candidateLabeledSamples (MCSP.Instance.inputIndex input) (truthTable target) (packTargetSamples target inputs) = fun (sample : Fin (prefixLength + 1)) => SuccinctMCSP.Sample.ofFunction target (Fin.cons input inputs sample)

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.selectionRoundSuccessorInput_truthTable_packTargetSamples_internal {arity prefixLength : ℕ} (target : BitString arity → Bool) (inputs : Fin prefixLength → BitString arity) (candidate : Fin (2 ^ arity)) : selectionRoundSuccessorInput candidate (truthTable target) (packTargetSamples target inputs) = selectionTraceState target (Fin.cons (MCSP.Instance.inputOfIndex candidate) inputs)

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.counterRoundEstimate_truthTable_packTargetSamples_internal {overhead arity prefixLength : ℕ} {beta : PositiveRationalScale} (counter : ApproximateCounterCircuit overhead beta arity prefixLength) (target : BitString arity → Bool) (inputs : Fin prefixLength → BitString arity) (input : BitString arity) : counterRoundEstimate counter (truthTable target) (packTargetSamples target inputs) input = counter.estimate (packTargetSamples target (Fin.cons input inputs))

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.counterRoundEstimate_eq_extensionEstimator_internal {overhead arity rounds : ℕ} {beta : PositiveRationalScale} (family : ApproximateCounterFamily overhead beta arity) (target : BitString arity → Bool) (inputs : Fin rounds → BitString arity) (hrounds : rounds + 1 ≤ requiredRoundCount beta arity) : counterRoundEstimate (family.counter (selectionPrefixCounterIndex hrounds)) (truthTable target) (packTargetSamples target inputs) = family.extensionEstimator target (List.ofFn inputs)

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.exists_eval_selectionPrefixCircuit_isEstimateSelectionTrace_internal {overhead arity rounds : ℕ} {beta : PositiveRationalScale} (family : ApproximateCounterFamily overhead beta arity) (target : BitString arity → Bool) (hrounds : rounds ≤ requiredRoundCount beta arity) : ∃ (inputs : Fin rounds → BitString arity), (selectionPrefixCircuit family rounds hrounds).snd.eval (truthTable target) = selectionTraceState target inputs ∧ AntiChecker.IsEstimateSelectionTrace (family.extensionEstimator target) (List.ofFn inputs)

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.exists_eval_fullSelectionStateCircuit_isEstimateSelectionTrace_internal {overhead arity : ℕ} {beta : PositiveRationalScale} (family : ApproximateCounterFamily overhead beta arity) (target : BitString arity → Bool) : ∃ (inputs : Fin (requiredRoundCount beta arity) → BitString arity), (fullSelectionStateCircuit family).snd.eval (truthTable target) = selectionTraceState target inputs ∧ AntiChecker.IsEstimateSelectionTrace (family.extensionEstimator target) (List.ofFn inputs)

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.unpackSample_selectionTraceState_projection_internal {arity rounds : ℕ} (target : BitString arity → Bool) (inputs : Fin rounds → BitString arity) (sample : Fin rounds) : unpackSample (selectionTraceState target inputs ∘ selectionSampleOutputMap arity rounds) sample = inputs sample

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.eval_fullSelectionSamplesCircuit_internal {overhead arity : ℕ} {beta : PositiveRationalScale} [NeZero arity] (family : ApproximateCounterFamily overhead beta arity) (table : BitString (2 ^ arity)) : (fullSelectionSamplesCircuit family).snd.eval table = (fullSelectionStateCircuit family).snd.eval table ∘ selectionSampleOutputMap arity (requiredRoundCount beta arity)

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.size_fullSelectionSamplesCircuit_internal {overhead arity : ℕ} {beta : PositiveRationalScale} [NeZero arity] (family : ApproximateCounterFamily overhead beta arity) : (fullSelectionSamplesCircuit family).snd.size = (fullSelectionStateCircuit family).snd.size + requiredRoundCount beta arity * arity

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