Fixed-width circuit-candidate enumeration -- proof internals

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

Internal exact equivalence between canonical candidate codes and bounded well-formed raw circuits.

Equations

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

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

Internal exact equivalence between the old canonical candidate-code type and valid fixed-width descriptions.

Equations

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

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

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

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

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