Fixed-width anti-checker counter domains

Valid bounded circuit descriptions encode injectively into one parameter-sized Boolean cube. Consequently, counting encoded survivors is exactly the existing labeled survivor count, with no delimiter parser or padding multiplicity.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.mem_encodedCandidateLabeledSurvivorCodes_iff {count arity threshold : ℕ} {samples : Fin count → SuccinctMCSP.Sample arity} {encoded : BitString (candidateCodeWidth arity threshold)} : encoded ∈ encodedCandidateLabeledSurvivorCodes arity threshold samples ↔ EncodedDescriptionMatchesLabeledSamples samples encoded

Membership in the fixed-width survivor domain is exactly successful decoding to a valid description that matches every sample.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.mem_encodedCandidateLabeledSurvivorCodes_iff_exists_description {count arity threshold : ℕ} {samples : Fin count → SuccinctMCSP.Sample arity} {encoded : BitString (candidateCodeWidth arity threshold)} : encoded ∈ encodedCandidateLabeledSurvivorCodes arity threshold samples ↔ ∃ (description : CircuitCode.FixedWidth.ValidDescription arity threshold), CircuitCode.FixedWidth.Description.decode? encoded = some ↑description ∧ DescriptionMatchesLabeledSamples samples description

Equivalently, a survivor word decodes to one valid description that matches every labeled sample.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.mem_encodedSurvivorSet_iff {count arity threshold : ℕ} {input : BitString (count * (arity + 1))} {encoded : BitString (candidateCodeWidth arity threshold)} : encoded ∈ encodedSurvivorSet arity threshold input ↔ EncodedDescriptionMatchesLabeledSamples (unpackLabeledSamples input) encoded

Packed-input survivor membership uses the decoded fixed-description predicate on the unpacked labeled samples.

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

Encoding canonical labeled survivors in the fixed Boolean cube preserves their cardinality exactly.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.card_encodedSurvivorSet {count arity threshold : ℕ} (input : BitString (count * (arity + 1))) : (encodedSurvivorSet arity threshold input).card = candidateLabeledSurvivorCount arity threshold (unpackLabeledSamples input)

The packed-input survivor set has exactly the canonical labeled survivor count.