Circuit-level anti-checker selection rounds -- proof internals

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.eval_candidateCounterInputCircuit_internal {arity prefixLength : ℕ} (candidate : Fin (2 ^ arity)) (table : BitString (2 ^ arity)) (packedPrefix : BitString (prefixLength * (arity + 1))) : (candidateCounterInputCircuit arity prefixLength candidate).eval (selectionRoundInput table packedPrefix) = packLabeledSamples (candidateLabeledSamples candidate table packedPrefix)

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.eval_candidateSampleCircuit_internal {arity prefixLength : ℕ} (candidate : Fin (2 ^ arity)) (table : BitString (2 ^ arity)) (packedPrefix : BitString (prefixLength * (arity + 1))) : (candidateSampleCircuit arity prefixLength candidate).eval (selectionRoundInput table packedPrefix) = candidateSampleBits candidate table

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.eval_candidateCounterRecordCircuit_internal {overhead arity prefixLength : ℕ} {beta : PositiveRationalScale} (counter : ApproximateCounterCircuit overhead beta arity prefixLength) (candidate : Fin (2 ^ arity)) (table : BitString (2 ^ arity)) (packedPrefix : BitString (prefixLength * (arity + 1))) : (candidateCounterRecordCircuit counter candidate).snd.eval (selectionRoundInput table packedPrefix) = Fin.append (counter.circuit.eval (packLabeledSamples (candidateLabeledSamples candidate table packedPrefix))) (candidateSampleBits candidate table)

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.size_candidateCounterRecordCircuit_internal {overhead arity prefixLength : ℕ} {beta : PositiveRationalScale} (counter : ApproximateCounterCircuit overhead beta arity prefixLength) (candidate : Fin (2 ^ arity)) : (candidateCounterRecordCircuit counter candidate).snd.size = counter.circuit.size + (prefixLength + 1) * (arity + 1) + (arity + 1)

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.selectionCandidateCount_add_one_internal (arity : ℕ) : selectionCandidateCount arity + 1 = 2 ^ arity

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.eval_packedCandidateCounterRecords_internal {overhead arity prefixLength : ℕ} {beta : PositiveRationalScale} (counter : ApproximateCounterCircuit overhead beta arity prefixLength) (table : BitString (2 ^ arity)) (packedPrefix : BitString (prefixLength * (arity + 1))) : (packedCandidateCounterRecords counter).snd.eval (selectionRoundInput table packedPrefix) = BitString.packKeyedRecords (selectionCandidateCount arity) (candidateCounterKeys counter table packedPrefix) (candidateCounterPayloads table)

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.size_packedCandidateCounterRecords_internal {overhead arity prefixLength : ℕ} {beta : PositiveRationalScale} (counter : ApproximateCounterCircuit overhead beta arity prefixLength) : (packedCandidateCounterRecords counter).snd.size = (selectionCandidateCount arity + 1) * (counter.circuit.size + (prefixLength + 1) * (arity + 1) + (arity + 1))

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.eval_minimumCounterRecordCircuit_internal {overhead arity prefixLength : ℕ} {beta : PositiveRationalScale} (counter : ApproximateCounterCircuit overhead beta arity prefixLength) (table : BitString (2 ^ arity)) (packedPrefix : BitString (prefixLength * (arity + 1))) : (minimumCounterRecordCircuit counter).snd.eval (selectionRoundInput table packedPrefix) = Fin.append (minimumCounterRecord counter table packedPrefix).1 (minimumCounterRecord counter table packedPrefix).2

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.size_minimumCounterRecordCircuit_internal {overhead arity prefixLength : ℕ} {beta : PositiveRationalScale} (counter : ApproximateCounterCircuit overhead beta arity prefixLength) : (minimumCounterRecordCircuit counter).snd.size = (selectionCandidateCount arity + 1) * (counter.circuit.size + (prefixLength + 1) * (arity + 1) + (arity + 1)) + ((selectionCandidateCount arity + 1) * (counterOutputWidth beta arity + (arity + 1)) + selectionCandidateCount arity * (20 * counterOutputWidth beta arity + 5 * (arity + 1) + 1))

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.candidateSampleBits_input_internal {arity : ℕ} (candidate : Fin (2 ^ arity)) (table : BitString (2 ^ arity)) (coordinate : Fin arity) : candidateSampleBits candidate table coordinate.castSucc = MCSP.Instance.inputOfIndex candidate coordinate

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.candidateSampleBits_output_internal {arity : ℕ} (candidate : Fin (2 ^ arity)) (table : BitString (2 ^ arity)) : candidateSampleBits candidate table (Fin.last arity) = table candidate

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.exists_minimumCounterRecord_eq_candidate_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)), minimumCounterRecord counter table packedPrefix = (candidateCounterKey counter candidate table packedPrefix, candidateSampleBits candidate table)

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.minimumCounterRecord_key_le_candidate_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)) : (minimumCounterRecord counter table packedPrefix).1.unsignedValue ≤ (candidateCounterKey counter candidate table packedPrefix).unsignedValue

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.exists_minimumCounterRecord_candidate_isEstimateMinimizer_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)), minimumCounterRecord counter table packedPrefix = (candidateCounterKey counter candidate table packedPrefix, candidateSampleBits candidate table) ∧ AntiChecker.IsEstimateMinimizer (counterRoundEstimate counter table packedPrefix) (MCSP.Instance.inputOfIndex candidate)

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.exists_eval_minimumCounterRecordCircuit_eq_candidate_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)), (minimumCounterRecordCircuit counter).snd.eval (selectionRoundInput table packedPrefix) = Fin.append (candidateCounterKey counter candidate table packedPrefix) (candidateSampleBits candidate table) ∧ AntiChecker.IsEstimateMinimizer (counterRoundEstimate counter table packedPrefix) (MCSP.Instance.inputOfIndex candidate)