Relation-certificate encoding proofs

Completeness and cardinality of the site enumeration give absence of duplicates. Reading at a site's index then yields both directions of the encoding bijection.

theorem Complexity.DescriptiveComplexity.DecREnv.mem_encodingSites_internal (card : ℕ) (rctx : List ℕ) (site : EncodingSite card rctx) : site ∈ encodingSites card rctx

theorem Complexity.DescriptiveComplexity.DecREnv.encodingSites_length_internal (card : ℕ) (rctx : List ℕ) : (encodingSites card rctx).length = encodingLength card rctx

theorem Complexity.DescriptiveComplexity.DecREnv.encodingSites_nodup_internal (card : ℕ) (rctx : List ℕ) : (encodingSites card rctx).Nodup

theorem Complexity.DescriptiveComplexity.DecREnv.read_encode_internal {card : ℕ} {rctx : List ℕ} (ρ : DecREnv card rctx) : read card rctx ρ.encode = ρ

theorem Complexity.DescriptiveComplexity.DecREnv.encode_read_internal (card : ℕ) (rctx : List ℕ) (bits : List Bool) (h : bits.length = encodingLength card rctx) : (read card rctx bits).encode = bits

theorem Complexity.DescriptiveComplexity.DecREnv.encodingPolynomial_eval_internal (card : ℕ) (rctx : List ℕ) : Polynomial.eval card (encodingPolynomial rctx) = encodingLength card rctx

theorem Complexity.DescriptiveComplexity.DecREnv.encodingLength_mono_internal (rctx : List ℕ) : Monotone fun (card : ℕ) => encodingLength card rctx