Anti-checker counter relation -- proof internals

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.card_candidateLabeledSurvivorDescriptions_internal {count arity threshold : ℕ} (samples : Fin count → SuccinctMCSP.Sample arity) : (candidateLabeledSurvivorDescriptions arity threshold samples).card = candidateLabeledSurvivorCount arity threshold samples

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.codeMatchesTargetSamples_iff_internal {count arity : ℕ} (target : BitString arity → Bool) (inputs : Fin count → BitString arity) (code : List Bool) : CodeMatchesLabeledSamples (fun (sample : Fin count) => SuccinctMCSP.Sample.ofFunction target (inputs sample)) code ↔ AntiChecker.ConsistentCode target (List.ofFn inputs) code

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.candidateLabeledSurvivorCount_targetSamples_internal {count arity threshold : ℕ} (target : BitString arity → Bool) (inputs : Fin count → BitString arity) : (candidateLabeledSurvivorCount arity threshold fun (sample : Fin count) => SuccinctMCSP.Sample.ofFunction target (inputs sample)) = AntiChecker.candidateSurvivorCount target threshold (List.ofFn inputs)

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.candidateLabeledSurvivorCount_unpack_pack_internal {count arity threshold : ℕ} (samples : Fin count → SuccinctMCSP.Sample arity) : candidateLabeledSurvivorCount arity threshold (unpackLabeledSamples (packLabeledSamples samples)) = candidateLabeledSurvivorCount arity threshold samples

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.candidateLabeledSurvivorCount_unpack_packTargetSamples_internal {count arity threshold : ℕ} (target : BitString arity → Bool) (inputs : Fin count → BitString arity) : candidateLabeledSurvivorCount arity threshold (unpackLabeledSamples (packTargetSamples target inputs)) = AntiChecker.candidateSurvivorCount target threshold (List.ofFn inputs)