Anti-checker counter encodings -- proof internals

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.packLabeledSamples_input_internal {count arity : ℕ} (samples : Fin count → SuccinctMCSP.Sample arity) (sample : Fin count) (coordinate : Fin arity) : packLabeledSamples samples (finProdFinEquiv (sample, coordinate.castSucc)) = (samples sample).input coordinate

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.packLabeledSamples_output_internal {count arity : ℕ} (samples : Fin count → SuccinctMCSP.Sample arity) (sample : Fin count) : packLabeledSamples samples (finProdFinEquiv (sample, Fin.last arity)) = (samples sample).output

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.unpackLabeledSample_packLabeledSamples_internal {count arity : ℕ} (samples : Fin count → SuccinctMCSP.Sample arity) (sample : Fin count) : unpackLabeledSample (packLabeledSamples samples) sample = samples sample

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

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.packLabeledSamples_unpackLabeledSamples_internal {count arity : ℕ} (input : BitString (count * (arity + 1))) : packLabeledSamples (unpackLabeledSamples input) = input

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.packTargetSamples_input_internal {count arity : ℕ} (target : BitString arity → Bool) (inputs : Fin count → BitString arity) (sample : Fin count) (coordinate : Fin arity) : packTargetSamples target inputs (finProdFinEquiv (sample, coordinate.castSucc)) = inputs sample coordinate

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.packTargetSamples_output_internal {count arity : ℕ} (target : BitString arity → Bool) (inputs : Fin count → BitString arity) (sample : Fin count) : packTargetSamples target inputs (finProdFinEquiv (sample, Fin.last arity)) = target (inputs sample)

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.counterValue_lt_two_pow_internal {width : ℕ} (output : BitString width) : counterValue output < 2 ^ width