Documentation

Complexitylib.DescriptiveComplexity.Encoding.Positions

Reading the structure encoding by table site #

The computable positions recover every relation and constant-table bit. The full encoded length is strictly increasing with universe size, so at a fixed input length there can be at most one structure size.

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

Every relation and constant-table site occurs in the encoder's ordering.

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

Every table position lies within the full encoded input.

source
theorem Complexity.DescriptiveComplexity.encodeStruct_length_eq {V : Vocabulary} (A : DecFinStruct V) :
(encodeStruct A).length = encodingLength V A.card

The existing structure encoder has the named encoded length.

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

Reading a table site's computed position recovers exactly its stored value.

source
theorem Complexity.DescriptiveComplexity.card_lt_encodingLength (V : Vocabulary) (card : ℕ) :
card < encodingLength V card

The unary prefix alone is longer than the represented universe size.

source
theorem Complexity.DescriptiveComplexity.encodingLength_pos (V : Vocabulary) (card : ℕ) :
0 < encodingLength V card

Encoded lengths are positive even when all relation and constant tables are empty.

source
instance Complexity.DescriptiveComplexity.instNeZeroNatEncodingLength (V : Vocabulary) (card : ℕ) :
NeZero (encodingLength V card)
source
theorem Complexity.DescriptiveComplexity.encodingLength_strictMono (V : Vocabulary) :
StrictMono (encodingLength V)

The unary prefix makes encoded length strictly increasing in universe size.

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

Every table site occurs exactly once in the encoder's ordering.

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

The header contains card true bits followed by the false terminator.

source
theorem Complexity.DescriptiveComplexity.encodeStruct_eq_of_values {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

Correct length, header, and table bits characterize the full encoding.