Fixed-width anti-checker counter domains -- definitions

Affine hashing acts directly on the fixed-width binary descriptions of valid bounded circuits. Each survivor has one canonical word, with no delimiter, parser branch, or padding multiplicity.

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.candidateCodeWidth (arity threshold : ℕ) : ℕ

Fixed cube dimension for circuit descriptions at one arity and gate threshold.

Equations

• Complexity.GapMCSP.Magnification.AntiCheckerLemma.candidateCodeWidth arity threshold = Complexity.CircuitCode.FixedWidth.codeWidth arity threshold

instance Complexity.GapMCSP.Magnification.AntiCheckerLemma.instNeZeroNatCandidateCodeWidth (arity threshold : ℕ) : NeZero (candidateCodeWidth arity threshold)

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.EncodedDescriptionMatchesLabeledSamples {count arity threshold : ℕ} (samples : Fin count → SuccinctMCSP.Sample arity) (encoded : BitString (candidateCodeWidth arity threshold)) : Prop

One fixed-width word decodes to a valid description matching every labeled sample. Malformed count words and invalid descriptions are rejected.

Equations

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

@[instance_reducible]

instance Complexity.GapMCSP.Magnification.AntiCheckerLemma.instDecidableEncodedDescriptionMatchesLabeledSamples {count arity threshold : ℕ} (samples : Fin count → SuccinctMCSP.Sample arity) (encoded : BitString (candidateCodeWidth arity threshold)) : Decidable (EncodedDescriptionMatchesLabeledSamples samples encoded)

Equations

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

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.encodedCandidateLabeledSurvivorCodes {count : ℕ} (arity threshold : ℕ) (samples : Fin count → SuccinctMCSP.Sample arity) : Finset (BitString (candidateCodeWidth arity threshold))

Canonical fixed-width words that decode to valid descriptions surviving a labeled sample vector.

Equations

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

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.encodedSurvivorSet {count : ℕ} (arity threshold : ℕ) (input : BitString (count * (arity + 1))) : Finset (BitString (candidateCodeWidth arity threshold))

The fixed-width survivor set associated with a packed labeled-sample input.

Equations

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