Polynomial-time access to structure encodings

The universe size, tuple coordinates, and bit positions are natural numbers written in unary by polynomial-time machines. Fixed-arity tuple indices, relation addresses, constant addresses, and encoding lengths use only fixed sums, powers, and products. Bit reads at these positions therefore have actual FP implementations, including the false default on missing input bits.

The unary-cardinality parser and the encoded-length check are also polynomial time. Encoding.Validity uses these primitives to recognize valid encodings in P, and ModelChecking.PolynomialTime proves the same bound for fixed first-order queries. SecondOrder.PolynomialTime extends evaluation to relation witnesses and proves polynomial-time existential-SO certificate checking.

theorem Complexity.DescriptiveComplexity.tupleIndex_unary {card : List Bool → ℕ} {k : ℕ} {args : List Bool → Fin k → ℕ} (hcard : UnaryFn card) (hargs : ∀ (i : Fin k), UnaryFn fun (z : List Bool) => args z i) : UnaryFn fun (z : List Bool) => tupleIndex (card z) (args z)

Fixed-arity tuple indices are polynomial-time unary numbers.

theorem Complexity.DescriptiveComplexity.tupleDigits_unary {card index : List Bool → ℕ} (hcard : UnaryFn card) (hindex : UnaryFn index) (k : ℕ) (i : Fin k) : UnaryFn fun (z : List Bool) => tupleDigits (card z) k (index z) i

Extracting a fixed coordinate of a polynomial-time tuple index is polynomial-time.

theorem Complexity.DescriptiveComplexity.relationAddress_unary (V : Vocabulary) (r : Fin V.numRels) {card : List Bool → ℕ} {args : List Bool → Fin (V.relArity r) → ℕ} (hcard : UnaryFn card) (hargs : ∀ (i : Fin (V.relArity r)), UnaryFn fun (z : List Bool) => args z i) : UnaryFn fun (z : List Bool) => relationAddress V (card z) r (args z)

Computing a fixed relation's bit address is polynomial-time.

theorem Complexity.DescriptiveComplexity.constantAddress_unary (V : Vocabulary) (c : Fin V.numConsts) {card a : List Bool → ℕ} (hcard : UnaryFn card) (ha : UnaryFn a) : UnaryFn fun (z : List Bool) => constantAddress V (card z) c (a z)

Computing a fixed constant's one-hot bit address is polynomial-time.

theorem Complexity.DescriptiveComplexity.encodingLength_unary (V : Vocabulary) {card : List Bool → ℕ} (hcard : UnaryFn card) : UnaryFn fun (z : List Bool) => encodingLength V (card z)

The full encoded structure length is polynomial-time in a polynomial-time universe size.

theorem Complexity.DescriptiveComplexity.DecREnv.encodingLength_unary (rctx : List ℕ) {card : List Bool → ℕ} (hcard : UnaryFn card) : UnaryFn fun (z : List Bool) => encodingLength (card z) rctx

A fixed relation-witness context's certificate length is a polynomial-time unary number.

theorem Complexity.DescriptiveComplexity.encodedCard_unary : UnaryFn fun (input : List Bool) => (List.takeWhile id input).length

The universe size read from an input's leading unary block is polynomial-time.

theorem Complexity.DescriptiveComplexity.encodingLengthMatches_fpPred (V : Vocabulary) : FPPred fun (input : List Bool) => input.length = encodingLength V (List.takeWhile id input).length

Testing the full encoding length against the parsed cardinality is polynomial-time.

theorem Complexity.DescriptiveComplexity.relationBit_fpPred (V : Vocabulary) (r : Fin V.numRels) {bits : List Bool → List Bool} {card : List Bool → ℕ} {args : List Bool → Fin (V.relArity r) → ℕ} (hbits : bits ∈ FP) (hcard : UnaryFn card) (hargs : ∀ (i : Fin (V.relArity r)), UnaryFn fun (z : List Bool) => args z i) : FPPred fun (z : List Bool) => (bits z)[relationAddress V (card z) r (args z)]?.getD false = true

A relation-table bit can be tested in polynomial time at polynomial-time coordinates.

theorem Complexity.DescriptiveComplexity.constantBit_fpPred (V : Vocabulary) (c : Fin V.numConsts) {bits : List Bool → List Bool} {card a : List Bool → ℕ} (hbits : bits ∈ FP) (hcard : UnaryFn card) (ha : UnaryFn a) : FPPred fun (z : List Bool) => (bits z)[constantAddress V (card z) c (a z)]?.getD false = true

A constant's one-hot bit can be tested in polynomial time.