Correctness of arithmetic encoding addresses

Index a flattened list by the total length of preceding blocks plus an offset within the selected block. Applied first to tuples and then to relation tables, this identifies arithmetic addresses with the encoder's existing site positions.

theorem Complexity.DescriptiveComplexity.tupleIndex_eq_sum_internal (card : ℕ) {k : ℕ} (args : Fin k → ℕ) : tupleIndex card args = ∑ i : Fin k, args i * card ^ ↑i

theorem Complexity.DescriptiveComplexity.tupleDigits_eq_div_pow_internal (card k index : ℕ) (i : Fin k) : tupleDigits card k index i = index / card ^ ↑i % card

theorem Complexity.DescriptiveComplexity.getElem?_flatMap_offset_internal {α β : Type} (xs : List α) (f : α → List β) (i : Fin xs.length) (j : ℕ) (hj : j < (f xs[↑i]).length) : (List.flatMap f xs)[(List.map (fun (x : α) => (f x).length) (List.take (↑i) xs)).sum + j]? = (f xs[↑i])[j]?

theorem Complexity.DescriptiveComplexity.tupleIndex_lt_internal {card k : ℕ} (args : Fin k → Fin card) : (tupleIndex card fun (i : Fin k) => ↑(args i)) < card ^ k

theorem Complexity.DescriptiveComplexity.getElem?_allTuples_index_internal {card k : ℕ} (args : Fin k → Fin card) : (allTuples card k)[tupleIndex card fun (i : Fin k) => ↑(args i)]? = some args

theorem Complexity.DescriptiveComplexity.tupleDigits_lt_internal {card : ℕ} (hcard : 0 < card) (k index : ℕ) (i : Fin k) : tupleDigits card k index i < card

theorem Complexity.DescriptiveComplexity.tupleIndex_tupleDigits_internal {card : ℕ} (hcard : 0 < card) (k index : ℕ) (hi : index < card ^ k) : tupleIndex card (tupleDigits card k index) = index

theorem Complexity.DescriptiveComplexity.map_allTuples_eq_range_internal {α : Type} {card : ℕ} (hcard : 0 < card) (k : ℕ) (f : (Fin k → ℕ) → α) : List.map (fun (args : Fin k → Fin card) => f fun (i : Fin k) => ↑(args i)) (allTuples card k) = List.map (fun (index : ℕ) => f (tupleDigits card k index)) (List.range (card ^ k))

theorem Complexity.DescriptiveComplexity.encodingPosition_relation_internal (V : Vocabulary) (card : ℕ) (r : Fin V.numRels) (args : Fin (V.relArity r) → Fin card) : encodingPosition V card (Sum.inl ⟨r, args⟩) = relationAddress V card r fun (i : Fin (V.relArity r)) => ↑(args i)

theorem Complexity.DescriptiveComplexity.encodingPosition_constant_internal (V : Vocabulary) (card : ℕ) (c : Fin V.numConsts) (a : Fin card) : encodingPosition V card (Sum.inr (c, a)) = constantAddress V card c ↑a