ch:tarski-universes: ch:tarski-universes

Problem and invariant. Implement a finite code language whose dependent-product body uses de Bruijn index zero for the newly bound variable. Decoding and quotation must preserve constructor shape, and scope checking must reject escaping indices.

Two representations. Named variables make examples legible but require alpha-equivalence. De Bruijn indices make the executable round trip literal. The chapter retains named binders; the artifact chooses indices only for its finite scope oracle.

Build order. Add base codes and decoding, sums, then products. Add quotation before scope checking so a malformed body cannot be mistaken for a round-trip failure.

Observable result and mutation. The run prints five named passes and the recorded summary. Mutate the product scope case to check its body at the old depth; the dependent positive probe must fail.

Acceptance and boundary. Run all four appendix E commands, require the recorded transcript and empty audit, restore the source after mutation, and rerun. The result checks only this finite syntax. It does not establish substitution or derivation coherence for definition 75.1.