ch:dependent-staging: dependent stage checking

Problem, result, and invariant. Check a finite dependent staged fragment in which every variable is used at the stage where it was declared, quotation advances one stage, and escape returns through a code type to the enclosing stage. Maintain exact equality between the requested stage depth and the stage stored in each context entry; weakening the comparison to an order would admit raw cross-stage variables.

Representation tradeoff. The companion represents a stage word by a natural depth. This gives an exact, inspectable lookup test and is sufficient for the one-name fragment. It conflates distinct words of equal length and cannot express stage abstraction or application. A list of stage names would represent the full word and make quotation append explicit, at the cost of name equality, freshness, and two substitutions instead of arithmetic on a depth.

First complete version. Define natural and vector-indexed types, code types, entries carrying a depth and a type, and the lookup function. Add variables, natural literals, empty vectors, and vector cons. The minimal end-to-end case infers Vec(1) for a singleton vector at depth zero; the type computation therefore exercises a dependent index before any staging rule is added.

Remaining cases. Add the artifact’s nondependent function types, lambdas, and applications. The constructor PiTy Ty Ty stores a closed codomain and therefore implements an arrow, despite its name; dependent codomain substitution is checked separately in SubstitutionCore.agda. Add quotation by checking its body at the successor depth and returning a code type at the enclosing depth. Add escape by requiring a code type whose payload is checked at the successor depth, and add persistence only for the represented natural payload. Implement the escape–quote evaluation rule after typing. The exact-stage variable lookup is proof-emphasized: it is the variable premise preserved by the renaming and term-substitution clauses of lemma 130.3.

Observable result. The accepted run prints the singleton vector index, its quoted code type, the escape–quote result, the shifted persistent natural, rejection of a raw crossing, and All 5 Chapter 130 corpus cases passed.

A failing version. Delete the stage comparison from the zero-index lookup clause. The mutant still typechecks and leaves every accepted fixture unchanged, but reports raw-crossing: accepted. The exact stdout oracle rejects the new line.

Acceptance test. Apply subappendix E.6. Require one passing inline test, the exact accepted transcript, and audit []. Replay the mutation, require failure on the raw-crossing line, restore, and rerun all four commands.

Mathematical boundary. The corpus is a finite witness for the exact-stage lookup case of lemma 130.3 and the closed final-form cases used by corollary 130.16. It proves neither theorem and does not mechanize preservation, confluence, or strong normalization. It also omits distinct stage names, stage abstraction, and stage application. Run agda SubstitutionCore.agda to check the independent proof companion. Its raw dependent layer represents index expressions, vectors indexed by them, and dependent products; substitution descends beneath the dependent codomain and computes the two displayed vector examples. Its separate term family is indexed by a natural stage depth and an intrinsic context, with length-indexed vectors and code. The file defines term renaming, simultaneous substitution, explicit persistence, and typed beta and quote–escape steps, so preservation of those intrinsic steps is a typechecked consequence. Natural depth still identifies different stage words of the same length, and the two layers are not a full mutually intrinsic dependent calculus.