Fixed-width circuit-candidate enumeration

Canonical small-circuit codes and valid fixed-width descriptions enumerate exactly the same bounded well-formed raw circuits. Consequently, replacing the variable-length survivor domain preserves its cardinality exactly.

noncomputable def Complexity.AntiChecker.candidateCodeFixedWidthEquiv (arity threshold : ℕ) : ↥(CandidateCode arity threshold) ≃ CircuitCode.FixedWidth.ValidDescription arity threshold

Canonical variable-length candidates are in exact correspondence with valid fixed-width circuit descriptions.

Equations

• Complexity.AntiChecker.candidateCodeFixedWidthEquiv arity threshold = Complexity.AntiChecker.candidateCodeFixedWidthEquivInternal arity threshold

theorem Complexity.AntiChecker.decode_candidateCodeFixedWidthEquiv {arity threshold : ℕ} (code : ↥(CandidateCode arity threshold)) : CircuitCode.RawCircuit.decode? ↑code = some (↑((candidateCodeFixedWidthEquiv arity threshold) code)).toRawCircuit

A candidate code decodes to the raw circuit represented by its associated fixed-width description.

theorem Complexity.AntiChecker.candidateCodeFixedWidthEquiv_symm_val {arity threshold : ℕ} (description : CircuitCode.FixedWidth.ValidDescription arity threshold) : ↑((candidateCodeFixedWidthEquiv arity threshold).symm description) = (↑description).toRawCircuit.encode

Mapping a valid fixed-width description back to the canonical candidate domain returns the raw encoding of its represented circuit.

theorem Complexity.AntiChecker.card_validDescription_eq_candidateCodes (arity threshold : ℕ) : Fintype.card (CircuitCode.FixedWidth.ValidDescription arity threshold) = (candidateCodes arity threshold).card

The fixed-width valid-description type has exactly as many members as the canonical variable-length candidate-code set.

theorem Complexity.AntiChecker.fixedWidth_codeWidth_le_codeLengthBound (arity threshold : ℕ) : CircuitCode.FixedWidth.codeWidth arity threshold ≤ codeLengthBound arity threshold

The fixed-width description cube fits inside the existing uniform unary code-length bound.