# K3B Alpha: cell histories and extensional lookup This chapter is the readable front end to the **Alpha-only** K3B finite-data bridge. It represents a finite list by its terminal doubled-Cantor cell code and uses a Gödel-β computation history to witness how that code was built. The resulting `ListAt` relation has the expected outer-head equations, unique values, and an extensionality theorem—without adding lists, projections, division, or a function-valued lookup to the Peano term grammar. ```{admonition} Closed Alpha evidence is not Stable promotion :class: important WMI job **219217** checked all seventeen selected theorem rows twice from the empty context. Both passes were deterministic and every resulting certificate contains zero uses of double-negation elimination. Their release membership is **Alpha-only** and their proof evidence is **closed checked**. The underlying receipt retains the legacy evidence spelling `closed_checked_candidate`; that does not make the rows private, nor does it promote them into the 432-theorem Stable checked-use registry. The graph below uses descriptive names until K3B is integrated into the unified Alpha tag space. See {doc}`Alpha and Stable library editions `. ```
17closed Alpha roots
2deterministic cold passes
95,253largest certificate
0DNE proof objects
## Explore the direct dependencies The embedded map starts in a deliberately sparse neighborhood view. Click a node to make it the focus; only its direct prerequisites and direct dependents remain visible. The full-map option still records only direct edges, and its default arrow mode draws only edges incident to the selected node. Yellow hexagons are conservative definitions, blue rounded nodes are Alpha-only theorems or support, and green rectangles are Stable boundary lemmas. Release membership and proof evidence are separate node fields; neither creates an extra arrow.

Open the K3B map in a full page

The solid arrows are proof dependencies and point from prerequisite to dependent. Dashed purple arrows are notation relationships. They explain which readable definitions occur in a statement; they never participate in a proof path and add no logical premise. ## The unchanged arithmetic underneath All the names in this section are authoring notation. Each call is hygienically expanded before the ordinary formula parser runs, and the kernel receives only first-order formulas over $$ 0,\qquad S,\qquad +,\qquad \times,\qquad =. $$ ### Strict order The development uses the ordinary gap representation $$ i ### Bounded β decoding `BetaAt(b,c,i,a)` says that $a$ is the bounded remainder of $b$ at the $i$th β modulus: $$ \operatorname{BetaAt}(b,c,i,a) \quad:\!\Longleftrightarrow\quad \begin{cases} \exists H,\;H+S(a)=S\bigl(S(i)c\bigr),\\ \exists Q,\;b=Q\,S\bigl(S(i)c\bigr)+a. \end{cases} $$ Thus the modulus is $1+(i+1)c$, and the first witness is the strict bound on the remainder. ### Exact cells The successor tag makes nil and every nonempty cell disjoint: $$ \operatorname{Cell}(u,h,t) \quad:\!\Longleftrightarrow\quad u=S\!\left((h+t)S(h+t)+(t+t)\right). $$ Here $h$ is the head, $t$ the tail code, and $u$ the resulting cell code. The Alpha strict-K3 support proves constructor existence, functionality, and strict descent of both components. ### Reverse construction histories A history begins at nil, ends at the displayed code, and records one exact cell at each adjacent β position: $$ \begin{aligned} \operatorname{CellHistory}(z,l;b,c) \quad:\!\Longleftrightarrow\quad &\operatorname{BetaAt}(b,c,0,0)\\ {}\land{}&\operatorname{BetaAt}(b,c,l,z)\\ {}\land{}&\forall j ### Semantic length Raw β witnesses are intentionally hidden: $$ \operatorname{CellListLen}(z,l) \quad:\!\Longleftrightarrow\quad \exists b,c,\;\operatorname{CellHistory}(z,l;b,c). $$ Different pairs $(b,c)$ may encode the same finite trace. The represented list is identified by its terminal exact-cell code $z$, not by a chosen β witness. ### Selection inside one history witness The local authoring abbreviation $$ \begin{aligned} \operatorname{HistoryAt}(l;b,c;i,a) \quad:\!\Longleftrightarrow\quad \exists j,t,u,\;&j+S(i)=l\\ {}\land{}&\operatorname{BetaAt}(b,c,j,t)\\ {}\land{}&\operatorname{BetaAt}(b,c,S(j),u)\\ {}\land{}&\operatorname{Cell}(u,a,t) \end{aligned} $$ selects edge $j$ by counting $i$ from the outside. ### Extensional client lookup Finally, `ListAt` existentially hides the history: $$ \begin{aligned} \operatorname{ListAt}(z,i,a) \quad:\!\Longleftrightarrow\quad \exists l,b,c,j,t,u,\;&\operatorname{CellHistory}(z,l;b,c)\\ {}\land{}&j+S(i)=l\\ {}\land{}&\operatorname{BetaAt}(b,c,j,t)\\ {}\land{}&\operatorname{BetaAt}(b,c,S(j),u)\\ {}\land{}&\operatorname{Cell}(u,a,t). \end{aligned} $$ The existential order $l,b,c,j,t,u$, right-associated conjunctions, and cell orientation `Cell(u,a,t)` are frozen parts of the surface contract. The fully expanded call has 3,331 characters, 54 formula constructors, 210 total PA syntax nodes, and SHA-256 `b83d91b6ec8e6b83fe637e1533c72beef54c7e7a4b41f1518bce8785cc9f11ce`. ## A concrete two-cell trace Start with nil and construct heads $0$ and then $2$: $$ 0 \xrightarrow{\ h=0\ } 1 \xrightarrow{\ h=2\ } 15. $$ Indeed, `Cell(1,0,0)` and `Cell(15,2,1)` both satisfy the exact polynomial. The trace values $(0,1,15)$ are simultaneously decoded by the distinct β witnesses $(b,c)=(1288,6)$ and $(3690,8)$. Outer-head lookup therefore gives $$ \operatorname{ListAt}(15,0,2), \qquad \operatorname{ListAt}(15,1,0). $$ This fixture illustrates both orientations at once: construction proceeds inner-to-outer, lookup counts outer-to-inner. It also exposes why raw β-code equality would be the wrong notion of list equality. ## The lookup ladder The order below is the proof-engineering order, not just a presentation order. T01 is a definition and therefore has no proof certificate. T02–T10 are included among the seventeen rows closed by job 219217. | Rung | Deliverable | Mathematical role | Proof idea | |---:|---|---|---| | T01 | `ListAt` | conservative outer-head lookup relation | expand D01/D02 and hide all β witnesses | | T02 | `cell_history_extend_preserves_prefix` | extend a history while retaining every old decoded entry | apply `beta_prefix_extend` at $S(l)$ | | T03 | `list_at_domain` | expose a semantic length and prove $i