Correctness of encoded table positions

The site enumeration is complete, has the expected length, and reproduces the existing encoder when mapped to table values. These facts justify direct reads.

theorem Complexity.DescriptiveComplexity.mem_encodingTableSites_internal (V : Vocabulary) (card : ℕ) (site : InputSite V card) : site ∈ encodingTableSites V card

theorem Complexity.DescriptiveComplexity.encodingTableSites_length_internal (V : Vocabulary) (card : ℕ) : (encodingTableSites V card).length = (List.map (fun (i : Fin V.numRels) => card ^ V.relArity i) (List.finRange V.numRels)).sum + V.numConsts * card

theorem Complexity.DescriptiveComplexity.map_encodingTableSites_internal {V : Vocabulary} (A : DecFinStruct V) : List.map (inputSiteValue A) (encodingTableSites V A.card) = encodeRelsC A ++ encodeConstsC A

theorem Complexity.DescriptiveComplexity.encodingPosition_lt_internal (V : Vocabulary) (card : ℕ) (site : InputSite V card) : encodingPosition V card site < encodingLength V card

theorem Complexity.DescriptiveComplexity.getElem?_encodeStruct_position_internal {V : Vocabulary} (A : DecFinStruct V) (site : InputSite V A.card) : (encodeStruct A)[encodingPosition V A.card site]? = some (inputSiteValue A site)

theorem Complexity.DescriptiveComplexity.encodingLength_strictMono_internal (V : Vocabulary) : StrictMono (encodingLength V)

theorem Complexity.DescriptiveComplexity.encodingTableSites_nodup_internal (V : Vocabulary) (card : ℕ) : (encodingTableSites V card).Nodup

theorem Complexity.DescriptiveComplexity.getElem?_encodeStruct_header_internal {V : Vocabulary} (A : DecFinStruct V) (i : Fin (A.card + 1)) : (encodeStruct A)[↑i]? = some (decide (↑i < A.card))

theorem Complexity.DescriptiveComplexity.encodeStruct_eq_of_values_internal {V : Vocabulary} (A : DecFinStruct V) (bits : List Bool) (hlen : bits.length = encodingLength V A.card) (hheader : ∀ (i : Fin (A.card + 1)), bits[↑i]? = some (decide (↑i < A.card))) (hsites : ∀ (site : InputSite V A.card), bits[encodingPosition V A.card site]? = some (inputSiteValue A site)) : encodeStruct A = bits