Arithmetic access to the canonical structure encoding

Base-card tuple indices and prefix sums give exactly the bit positions defined by the original site enumeration. The equalities include arbitrary relation arities, nullary relations, and the one-hot blocks for distinguished constants. Consequently the arithmetic addresses recover the encoded relation and constant bits, without changing the wire format. Fixed-width base expansion recovers the tuple coordinates; scanning the numeric indices reproduces the encoder's tuple enumeration exactly.

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

Tuple packing is the usual little-endian positional numeral.

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

Each extracted coordinate is a base-card digit, including at cardinality zero.

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

A tuple of valid coordinates has an index inside its relation truth table.

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

The arithmetic index selects the tuple itself in the encoder's enumeration.

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

Arithmetic tuple lookup recovers a bit from a relation's standalone truth table.

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

Every extracted coordinate lies in a positive-cardinality universe.

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

Re-encoding the coordinates recovers every index inside the tuple table.

theorem Complexity.DescriptiveComplexity.map_allTuples_eq_range {α : 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))

Enumerating tuples agrees with scanning their numeric indices in order.

theorem Complexity.DescriptiveComplexity.encodingPosition_relation (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)

Arithmetic relation addresses equal the existing enumeration-based positions.

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

Arithmetic constant addresses equal the existing one-hot positions.

theorem Complexity.DescriptiveComplexity.getElem?_encodeStruct_relation {V : Vocabulary} (A : DecFinStruct V) (r : Fin V.numRels) (args : Fin (V.relArity r) → Fin A.card) : (encodeStruct A)[relationAddress V A.card r fun (i : Fin (V.relArity r)) => ↑(args i)]? = some (A.rel r args)

Reading the arithmetic relation address returns the corresponding relation bit.

theorem Complexity.DescriptiveComplexity.getElem?_encodeStruct_constant {V : Vocabulary} (A : DecFinStruct V) (c : Fin V.numConsts) (a : Fin A.card) : (encodeStruct A)[constantAddress V A.card c ↑a]? = some (decide (A.const c = a))

Reading the arithmetic constant address tests equality with the distinguished element.