Iterable anti-checker selection rounds -- proof internals #
theorem
Complexity.GapMCSP.Magnification.AntiCheckerLemma.selectionRoundSuccessorInputMap_precompose_internal
{arity prefixLength : ℕ}
(beta : PositiveRationalScale)
(candidate : Fin (2 ^ arity))
(table : BitString (2 ^ arity))
(packedPrefix : BitString (prefixLength * (arity + 1)))
(key : BitString (counterOutputWidth beta arity))
:
Fin.append (selectionRoundInput table packedPrefix) (Fin.append key (candidateSampleBits candidate table)) ∘ selectionRoundSuccessorInputMap beta arity prefixLength = selectionRoundSuccessorInput candidate table packedPrefix
theorem
Complexity.GapMCSP.Magnification.AntiCheckerLemma.eval_selectionRoundCombinedCircuit_internal
{overhead arity prefixLength : ℕ}
{beta : PositiveRationalScale}
(counter : ApproximateCounterCircuit overhead beta arity prefixLength)
(table : BitString (2 ^ arity))
(packedPrefix : BitString (prefixLength * (arity + 1)))
:
(selectionRoundCombinedCircuit counter).snd.eval (selectionRoundInput table packedPrefix) = Fin.append (selectionRoundInput table packedPrefix)
((minimumCounterRecordCircuit counter).snd.eval (selectionRoundInput table packedPrefix))
theorem
Complexity.GapMCSP.Magnification.AntiCheckerLemma.size_selectionRoundCombinedCircuit_internal
{overhead arity prefixLength : ℕ}
{beta : PositiveRationalScale}
(counter : ApproximateCounterCircuit overhead beta arity prefixLength)
:
(selectionRoundCombinedCircuit counter).snd.size = selectionRoundInputWidth arity prefixLength + (minimumCounterRecordCircuit counter).snd.size
theorem
Complexity.GapMCSP.Magnification.AntiCheckerLemma.exists_eval_selectionRoundStateCircuit_eq_successor_internal
{overhead arity prefixLength : ℕ}
{beta : PositiveRationalScale}
(counter : ApproximateCounterCircuit overhead beta arity prefixLength)
(table : BitString (2 ^ arity))
(packedPrefix : BitString (prefixLength * (arity + 1)))
:
∃ (candidate : Fin (2 ^ arity)),
(selectionRoundStateCircuit counter).snd.eval (selectionRoundInput table packedPrefix) = selectionRoundSuccessorInput candidate table packedPrefix ∧ AntiChecker.IsEstimateMinimizer (counterRoundEstimate counter table packedPrefix)
(MCSP.Instance.inputOfIndex candidate)
theorem
Complexity.GapMCSP.Magnification.AntiCheckerLemma.size_selectionRoundStateCircuit_internal
{overhead arity prefixLength : ℕ}
{beta : PositiveRationalScale}
(counter : ApproximateCounterCircuit overhead beta arity prefixLength)
:
(selectionRoundStateCircuit counter).snd.size = selectionRoundInputWidth arity prefixLength + (minimumCounterRecordCircuit counter).snd.size + selectionRoundInputWidth arity (prefixLength + 1)