ch:dependent-intersections: same-subject views

Problem and invariant. Admit an annotated intersection only when both views erase to one finite shape. Projections must preserve that shape.

Two representations. Full de Bruijn lambda syntax would support beta-eta normalization. The selected three-shape grammar isolates the same-subject gate without pretending to implement historical Nuprl typing.

First complete version. Define shapes, annotations, and structural erasure. Add explicit shape equality, recursive admission, then identity, record, and mismatched fixtures. Test both projection annotations last.

Observable result. Four named cases pass and the run ends All 4 Chapter 93 corpus cases passed.

A failing version. Remove the shape-equality conjunct in the intersection case. The mismatched-pair oracle fails and the test exits 1.

Acceptance and boundary. Apply all four commands in subappendix E.7; require an empty audit after restoration. Shape equality is executable boundary evidence, not Kopylov’s semantic theorem.