ch:path-dependent-types: stable path lookup

Problem and result. Follow immutable field paths and singleton aliases while refusing to form a replacement whose changed path has no declared type. The accepted program must reach a lambda from x.a.c, replace two occurrences one at a time, reject the missing-field target, preserve a declared suffix, and report an alias cycle.

Representation. The environment is a finite association structure containing immutable object fields, path aliases, and terminal lambdas. Runtime lookupPath carries a decreasing fuel bound and a visited-path list. The separate declaredPath computation checks the root, every prefix, and the declared label of a complete path; aliases are followed with their own fuel and visited set. The declaredUse check applies declaredPath to every complete path changed by replacement. These computations derive their answers from the environment; the request contains no trusted Boolean certificate.

First complete version. Implement variables and field-path syntax, field lookup in one object, and recursive lookup through an alias. Record each visited path before following it. The chapter environment then takes x.a to y.b and continues through field c to the stored lambda.

Remaining cases. Make rewriteOneUse traverse left-to-right and stop after its first replacement. The two-occurrence fixture calls it twice and requires the reported count to be one on each call. Gate replaceAliases on declaredUse; this rejects an undeclared target and also rejects a rewrite that would retain an undeclared suffix. Finally use the visited list to return Cycle for mutually recursive aliases instead of exhausting fuel and pretending that exhaustion proves divergence.

Observable result. The eight named lines in subappendix E.10 are the complete oracle. The run ends All 8 Chapter 108 corpus cases passed.; its cycle result is a finite diagnostic, not a theorem about arbitrary lookup. The retained suffix line distinguishes a complete changed-path check from a root-only gate.

A failing version. Delete the declaredUse conjunct while retaining the declared-root gate. This mutant still typechecks and still rejects the undeclared root, but the retained-suffix oracle fails and the accepted summary is absent. The executable record in subappendix E.10 stores the exact mutant identity.

Acceptance test. Require the exact stdout and audit result [] recorded in subappendix E.10. The named mutation must make its test fail; restoring the prefix gate must restore every accepted outcome. The executable record in subappendix E.10 alone stores commands, source identities, and the mutation transcript.

Mathematical boundary. The implementation is bounded and finite. It does not establish path-lookup termination, replacement formation, initialization preservation, extended progress, or pDOT safety.