Circuit-level anti-checker selection rounds -- definitions

A selection round receives the target truth table followed by an already selected prefix of labeled samples. For each fixed candidate input, a circuit hardwires that input, reads its label from the truth table, evaluates the appropriate approximate counter on the extended prefix, and carries the labeled candidate beside the resulting counter key.

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.selectionRoundInputWidth (arity prefixLength : ℕ) : ℕ

Input width for one circuit-level selection round: the truth table followed by a row-major packed prefix of labeled samples.

Equations

• Complexity.GapMCSP.Magnification.AntiCheckerLemma.selectionRoundInputWidth arity prefixLength = 2 ^ arity + prefixLength * (arity + 1)

instance Complexity.GapMCSP.Magnification.AntiCheckerLemma.instNeZeroNatSelectionRoundInputWidth (arity prefixLength : ℕ) : NeZero (selectionRoundInputWidth arity prefixLength)

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.selectionRoundInput {arity prefixLength : ℕ} (table : BitString (2 ^ arity)) (packedPrefix : BitString (prefixLength * (arity + 1))) : BitString (selectionRoundInputWidth arity prefixLength)

Canonical input to one circuit-level selection round.

Equations

• Complexity.GapMCSP.Magnification.AntiCheckerLemma.selectionRoundInput table packedPrefix = Fin.append table packedPrefix

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.candidateSample {arity : ℕ} (candidate : Fin (2 ^ arity)) (table : BitString (2 ^ arity)) : SuccinctMCSP.Sample arity

The labeled sample represented by one fixed candidate and the candidate's truth-table bit.

Equations

• Complexity.GapMCSP.Magnification.AntiCheckerLemma.candidateSample candidate table = { input := Complexity.MCSP.Instance.inputOfIndex candidate, output := table candidate }

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.candidateLabeledSamples {arity prefixLength : ℕ} (candidate : Fin (2 ^ arity)) (table : BitString (2 ^ arity)) (packedPrefix : BitString (prefixLength * (arity + 1))) : Fin (prefixLength + 1) → SuccinctMCSP.Sample arity

Counter input obtained by prepending one fixed candidate to the previously selected labeled prefix.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.candidateSampleBits {arity : ℕ} (candidate : Fin (2 ^ arity)) (table : BitString (2 ^ arity)) : BitString (arity + 1)

Fixed-width payload carrying a candidate input followed by its target label.

Equations

• Complexity.GapMCSP.Magnification.AntiCheckerLemma.candidateSampleBits candidate table i = Fin.lastCases (table candidate) (Complexity.MCSP.Instance.inputOfIndex candidate) i

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.candidateCounterSources (arity prefixLength : ℕ) (candidate : Fin (2 ^ arity)) : Fin ((prefixLength + 1) * (arity + 1)) → Circuit.InputSource (selectionRoundInputWidth arity prefixLength)

Mixed constants and live inputs supplying the counter for one fixed candidate.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.candidateSampleSources (arity prefixLength : ℕ) (candidate : Fin (2 ^ arity)) : Fin (arity + 1) → Circuit.InputSource (selectionRoundInputWidth arity prefixLength)

Mixed constants and one live truth-table bit carrying the labeled candidate as a selector payload.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.candidateCounterInputCircuit (arity prefixLength : ℕ) (candidate : Fin (2 ^ arity)) : Circuit Basis.andOr2 (selectionRoundInputWidth arity prefixLength) ((prefixLength + 1) * (arity + 1)) 0

Materialize the labeled extended prefix expected by one counter circuit.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.candidateSampleCircuit (arity prefixLength : ℕ) (candidate : Fin (2 ^ arity)) : Circuit Basis.andOr2 (selectionRoundInputWidth arity prefixLength) (arity + 1) 0

Materialize the labeled candidate payload.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.candidateCounterRecordCircuit {overhead arity prefixLength : ℕ} {beta : PositiveRationalScale} (counter : ApproximateCounterCircuit overhead beta arity prefixLength) (candidate : Fin (2 ^ arity)) : (internalGates : ℕ) × Circuit Basis.andOr2 (selectionRoundInputWidth arity prefixLength) (counterOutputWidth beta arity + (arity + 1)) internalGates

Evaluate one approximate counter on a fixed candidate and carry the candidate's labeled sample beside the counter output.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.selectionCandidateCount (arity : ℕ) : ℕ

Number of comparisons needed to select among all 2^arity candidates.

Equations

• Complexity.GapMCSP.Magnification.AntiCheckerLemma.selectionCandidateCount arity = 2 ^ arity - 1

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.selectionCandidateEquiv (arity : ℕ) : Fin (selectionCandidateCount arity + 1) ≃ Fin (2 ^ arity)

Reindex the tournament's count + 1 records by all truth-table inputs.

Equations

• Complexity.GapMCSP.Magnification.AntiCheckerLemma.selectionCandidateEquiv arity = finCongr ⋯

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.candidateCounterKey {overhead arity prefixLength : ℕ} {beta : PositiveRationalScale} (counter : ApproximateCounterCircuit overhead beta arity prefixLength) (candidate : Fin (2 ^ arity)) (table : BitString (2 ^ arity)) (packedPrefix : BitString (prefixLength * (arity + 1))) : BitString (counterOutputWidth beta arity)

Counter-output key associated with one fixed candidate.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.counterRoundEstimate {overhead arity prefixLength : ℕ} {beta : PositiveRationalScale} (counter : ApproximateCounterCircuit overhead beta arity prefixLength) (table : BitString (2 ^ arity)) (packedPrefix : BitString (prefixLength * (arity + 1))) (input : BitString arity) : ℕ

Natural extension estimate computed by the counter for an arbitrary candidate input.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.candidateCounterRecordFamily {overhead arity prefixLength : ℕ} {beta : PositiveRationalScale} (counter : ApproximateCounterCircuit overhead beta arity prefixLength) : Fin (selectionCandidateCount arity + 1) → (internalGates : ℕ) × Circuit Basis.andOr2 (selectionRoundInputWidth arity prefixLength) (counterOutputWidth beta arity + (arity + 1)) internalGates

All fixed-candidate key-payload circuits, reindexed for the recursive tournament layout.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.candidateCounterKeys {overhead arity prefixLength : ℕ} {beta : PositiveRationalScale} (counter : ApproximateCounterCircuit overhead beta arity prefixLength) (table : BitString (2 ^ arity)) (packedPrefix : BitString (prefixLength * (arity + 1))) : Fin (selectionCandidateCount arity + 1) → BitString (counterOutputWidth beta arity)

Semantic counter keys in tournament record order.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.candidateCounterPayloads {arity : ℕ} (table : BitString (2 ^ arity)) : Fin (selectionCandidateCount arity + 1) → BitString (arity + 1)

Semantic labeled-candidate payloads in tournament record order.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.GapMCSP.Magnification.AntiCheckerLemma.packedCandidateCounterRecords {overhead arity prefixLength : ℕ} {beta : PositiveRationalScale} (counter : ApproximateCounterCircuit overhead beta arity prefixLength) : (internalGates : ℕ) × Circuit Basis.andOr2 (selectionRoundInputWidth arity prefixLength) (BitString.keyedTournamentInputWidth (selectionCandidateCount arity) (counterOutputWidth beta arity + (arity + 1))) internalGates

Pack every fixed-candidate counter record in the exact recursive layout consumed by the minimum tournament.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.minimumCounterRecord {overhead arity prefixLength : ℕ} {beta : PositiveRationalScale} (counter : ApproximateCounterCircuit overhead beta arity prefixLength) (table : BitString (2 ^ arity)) (packedPrefix : BitString (prefixLength * (arity + 1))) : BitString (counterOutputWidth beta arity) × BitString (arity + 1)

Semantic winner of exhaustive counter-key minimization.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.GapMCSP.Magnification.AntiCheckerLemma.minimumCounterRecordCircuit {overhead arity prefixLength : ℕ} {beta : PositiveRationalScale} (counter : ApproximateCounterCircuit overhead beta arity prefixLength) : (internalGates : ℕ) × Circuit Basis.andOr2 (selectionRoundInputWidth arity prefixLength) (counterOutputWidth beta arity + (arity + 1)) internalGates

Exhaustive selector returning a minimum counter key and its labeled candidate payload.

Equations

• One or more equations did not get rendered due to their size.