Fixed-width anti-checker counter domains -- proof internals

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

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

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

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

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