K3C Alpha: valid lists, membership, and semantic lookup

K3B proved that natural numbers can carry finite, outer-head cell histories and that an entry can be recovered through the relational predicate ListAt. K3C is the first client-facing layer over that representation. It introduces two readable definitions and seventeen reusable theorems without adding a list type, an indexing function, or a new kernel constant.

Exact evidence boundary

These seventeen rows belong to Alpha v2 with body_checked evidence. Every expanded statement is a closed formula of the unchanged PA language, every dependency-curried tactic body is accepted by the intuitionistic kernel, every declared direct dependency survives removal testing, and false-conclusion mutations fail. They are not yet checked-use facts: a two-pass isolated empty-context closure receipt is pending while WMI is unavailable. Stable remains exactly 432 theorems, and Alpha v1 remains byte-for-byte sealed.

Two conservative definitions

The mathematical surface is

\[\begin{split} \begin{aligned} \operatorname{CellListValid}(z) &:\!\Longleftrightarrow \exists \ell\;\operatorname{CellListLen}(z,\ell),\\ \operatorname{ListMember}(z,a) &:\!\Longleftrightarrow \exists i\;\operatorname{ListAt}(z,i,a). \end{aligned} \end{split}\]

CellListValid hides the length of the represented list. ListMember hides the index of an occurrence. Both are expanded before parsing into formulas over only (0,S,+,\times,=), connectives, and quantifiers. In particular, membership is relational and permits repeated values; it does not choose a distinguished occurrence.

The list orientation is inherited from K3B. If

\[ \operatorname{Cell}(z,h,t) \quad:\!\Longleftrightarrow\quad z=S\bigl((h+t)S(h+t)+(t+t)\bigr), \]

then (h) is the entry at outer index (0), and index (S(i)) in (z) is index (i) in the tail (t).

The seventeen-theorem interface

Layer	Theorems	Mathematical role
validity	cell_list_valid_nil, cell_list_valid_cell_intro, cell_list_valid_cases, cell_list_valid_cell_elim, list_at_implies_cell_list_valid	construct, split, and descend through valid codes; recover validity from lookup
membership	list_member_implies_cell_list_valid, list_member_nil_false, list_member_cell_intro_head, list_member_cell_intro_tail, list_member_cell_elim, list_member_cell_iff, list_member_pointwise_transport	domain, nil exclusion, head/tail introduction and elimination, and representation-independent transport
semantic lookup	list_at_exists_unique, cell_list_nonempty_iff_head_exists, cell_list_code_eq_lookup_values, cell_list_code_eq_iff_pointwise, cell_list_decompose_unique	total and unique in-range lookup, nonemptiness, extensional equality, and unique outer-cell decomposition

The most useful equations are the following. For a valid tail,

\[ \operatorname{Cell}(z,h,t) \Longrightarrow \bigl(\operatorname{ListMember}(z,a) \leftrightarrow a=h\lor\operatorname{ListMember}(t,a)\bigr). \]

For two represented lists of the same length, code equality is equivalent to agreement of every pair of values returned at every in-range index. And every successor-length list has a uniquely determined outer head and tail.

Sparse dependency view

Yellow hexagons are definitions, green rectangles are previously checked-use inputs, blue rounded rectangles are the new Alpha-only theorem rows, and the grey dashed box is a future gate rather than a theorem in this tranche. The diagram is a grouped conceptual spine; the exact catalog—not these grouped arrows—is authoritative for declared direct dependencies.

Proof anatomy

The proofs stay constructive throughout.

1. Validity cases induct on the hidden represented length. Length zero gives nil; successor length exposes one exact cell and a valid tail.

2. Membership elimination inducts on the hidden lookup index. At zero, list_at_head_iff identifies the value with the outer head. At a successor, list_at_succ_iff moves the lookup to the tail.

3. Unique lookup first constructs a value with list_at_exists, then compares any competing value with list_at_functional.

4. Extensional equality proves the easy direction by lookup functionality and the hard direction with K3B’s cell_list_extensional theorem.

5. Unique decomposition exposes one cell from a successor length and uses exact-cell functionality to identify every competing head and tail.

No proof uses excluded middle, double-negation elimination, choice, a trusted solver, or equality of raw beta-history codes.

One complete native proof body

Here is the exact tactic sequence of list_at_exists_unique, with the single long have type rendered through its readable ListAt name. Its two declared dependencies are introduced as local hypotheses by the body checker. The later empty-context compiler must replace those hypotheses with their checked certificates through Cut nodes.

intro z
intro l
intro i
intro hlength
intro hbound
have hexists : exists a. ListAt(z,i,a)
specialize list_at_exists z
specialize list_at_exists l
specialize list_at_exists i
apply list_at_exists
exact hlength
exact hbound
cases hexists
exists x
split
exact hexists_witness
intro d
intro hlookup_d
specialize list_at_functional z
specialize list_at_functional i
specialize list_at_functional d
specialize list_at_functional x
apply list_at_functional
exact hlookup_d
exact hexists_witness

The displayed ListAt in the have line is the readable version. The source factory substitutes its complete conservative expansion before parsing, so the kernel sees no ListAt constant.

Exact body receipts

Each tuple below is

(direct dependencies, tactic commands, proof nodes, depth,
 distinct proof objects, proof-DAG edges, reused objects)

Theorem	Receipt
cell_list_valid_nil	(1,4,5,5,5,4,0)
cell_list_valid_cell_intro	(1,18,19,13,19,18,0)
cell_list_valid_cases	(2,35,41,22,41,40,0)
cell_list_valid_cell_elim	(3,33,56,23,56,55,0)
list_at_implies_cell_list_valid	(1,14,15,11,15,14,0)
list_member_implies_cell_list_valid	(1,9,21,13,21,20,0)
list_member_nil_false	(5,33,41,19,41,40,0)
list_member_cell_intro_head	(1,18,19,13,19,18,0)
list_member_cell_intro_tail	(1,20,21,15,21,20,0)
list_member_cell_elim	(3,77,100,41,100,99,0)
list_member_cell_iff	(3,32,79,23,79,78,0)
list_member_pointwise_transport	(2,37,71,25,71,70,0)
list_at_exists_unique	(2,25,30,19,30,29,0)
cell_list_nonempty_iff_head_exists	(2,38,46,14,46,45,0)
cell_list_code_eq_lookup_values	(1,17,40,24,40,39,0)
cell_list_code_eq_iff_pointwise	(2,30,62,29,62,61,0)
cell_list_decompose_unique	(2,29,36,22,36,35,0)

The largest authored body has only 100 structural proof nodes. That is not an empty-context size estimate: closing a row embeds its dependency certificates through checked Cut sharing. A local capacity preflight closed the five semantic-interface rows; the largest was 160,934 structural occurrences at depth 89. Those ephemeral numbers guide capacity planning but do not replace the pending sealed receipt.

The next gate: append and prefix restriction

The interface was chosen to support a canonical next definition:

\[\begin{split} \begin{aligned} \operatorname{CellListAppend}(x,y,z) :\!\Longleftrightarrow \exists \ell,m\;(&\operatorname{CellListLen}(x,\ell)\land \operatorname{CellListLen}(y,m)\land \operatorname{CellListLen}(z,\ell+m)\land{}\\ &[\forall i,a\;\operatorname{ListAt}(x,i,a)\to \operatorname{ListAt}(z,i,a)]\land{}\\ &[\forall j,a\;\operatorname{ListAt}(y,j,a)\to \operatorname{ListAt}(z,\ell+j,a)]), \end{aligned} \end{split}\]

followed by exact prefix restriction

\[ \operatorname{CellListRestrict}(z,k,w) :\!\Longleftrightarrow \operatorname{CellListLen}(w,k)\land \exists r\;\operatorname{CellListAppend}(w,r,z). \]

Append existence will recurse through cell_list_decompose_unique; append functionality will compare the two results with cell_list_code_eq_iff_pointwise; restriction will then become a prefix factorization rather than a second competing representation.

Sources and reproduction

• representation RFC

• definition surface

• validity proofs

• membership proofs

• semantic-interface proofs

• exact proof audit

• cold-closure runner

• reviewed WMI job wrapper

From the repository root:

PYTHONPATH=peano-lab/py python3 -m pytest -q \
  peano-lab/py/tests/test_ha_cell_list_membership_surface_candidate.py \
  peano-lab/py/tests/test_ha_cell_list_membership_candidate.py
make peano-library-alpha-v2-check

Continue backward to K3B cell histories and lookup, or forward to the append/restriction design in the linked RFC.