Anti-checker counter relation

This module exposes the exact finite relation estimated by the conditional approximate counter circuits in the Anti-Checker Lemma construction.

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

Valid fixed-width descriptions surviving a labeled sample vector have exactly the existing canonical survivor count.

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

Explicit target labels recover the existing target-relative consistency predicate on the corresponding input list.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.candidateLabeledSurvivorCount_targetSamples {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)

Counting target-labeled vectors agrees exactly with the canonical survivor count on the corresponding input list.

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

The fixed-width sample codec preserves the survivor count exactly.

@[simp]

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.candidateLabeledSurvivorCount_unpack_packTargetSamples {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)

Decoding a packed target-labeled vector recovers the existing canonical survivor count on its input list.