TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-12

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The sequence-length and coordinate-reading functions are primitive recursive

Statement

For the coding from A natural-number coding of finite sequences, the following total functions are primitive recursive:

the decoded length function $len (s)$ defined by $len (s) = k if s = ⌜ (a_{0}, \dots, a_{k - 1}) ⌝_{s e q},$ and $len (s) = 0$ otherwise, and
the coordinate-reading function $entry (s, i)$ defined by $entry (s, i) = a_{i} if s = ⌜ (a_{0}, \dots, a_{k - 1}) ⌝_{s e q} and i < k,$ and $entry (s, i) = 0$ otherwise.

Facts & Assumptions

Given: The sequence coding from A natural-number coding of finite sequences.

[L1]

Primitive recursive functions are closed under the basic arithmetic, characteristic, and bounded-quantification constructions from Basic arithmetic operations and bounded quantification are primitive recursive.

[L2]

A coded finite sequence has binary numeral $1 1^{k} 0 c (bin (a_{0})) \dots c (bin (a_{k - 1}))$ , with each block $c (w) = 1^{∣ w ∣} 0 w$ , by A natural-number coding of finite sequences.

Proof

technique · direct

1.1

By bounded search on quotients and remainders, one can primitive-recursively recover the binary length of a positive integer and each individual bit of its canonical binary numeral. Using [L2], a bounded scan first reads the sentinel and unary header, obtaining a candidate $k$ . It then parses exactly $k$ self-delimiting blocks, checks that each payload is a canonical binary numeral, and verifies that the final block ends at the end of the numeral. Only if all these checks succeed does it return $k$ ; otherwise it returns $0$ . All scan bounds are at most the binary length of $s$ , so this full validity test and the total function $len$ are primitive recursive by [L1].

L1L2givenconstruct

2.1

Once $len (s) = k$ is known, the start and end of the $i$ th block $c (bin (a_{i}))$ are found by another bounded scan through the same binary numeral: each block begins with a run of $1$ 's whose length is the bit-length of $a_{i}$ , followed by one delimiter $0$ , followed by exactly that many payload bits. The integer represented by that payload is then recovered by a bounded primitive-recursive evaluation of binary place values.

L1L2step 1.1construct

3.1

If the bounded scan shows that $i \geq len (s)$ or that the numeral of $s$ is not of the required form, define the output to be $0$ . Otherwise return the value decoded in step 2.1. Because every search range is bounded by the bit-length of $s$ , the total function $entry (s, i)$ is primitive recursive by [L1].

L1step 2.1construct

4.1

Steps 1.1 and 3.1 prove that both the length function and the total coordinate-reading function are primitive recursive.

step 1.1step 3.1∎

Depends on

Used by

Dependency tree · two levels

7 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Jeremy Avigad and Richard Zach, Recursive Functions (standard reference, not scraped)
Klaus Sutner, Coding Functions (standard reference, not scraped)