Anti-checker counter encodings

This module exposes the exact fixed-width interface between labeled sample prefixes and the approximate counter circuits used by the Anti-Checker Lemma.

@[simp]

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

Input coordinate j of packed sample i is stored at row-major position (i, j).

@[simp]

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

The last coordinate of each packed sample row stores its output label.

@[simp]

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

Unpacking one row after packing recovers the original labeled sample.

@[simp]

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

Unpacking after packing recovers the complete labeled-sample vector.

@[simp]

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

Packing after unpacking recovers every fixed-width input string.

@[simp]

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

A target-labeled packed row preserves every input coordinate.

@[simp]

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

A target-labeled packed row stores the target's value as its final bit.

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

A width-bit counter output always denotes a number below 2^width.