ch:uniqueness-types: uniqueness eligibility

Problem and invariant. Decide the finite eligibility cases without claiming to infer uniqueness for the chapter calculus. Maintain this invariant: an outer $\mathsf{u}$ view is accepted only at reference count one, and an overwrite is accepted only when uniqueness, count, layout, and outgoing-edge typing all hold.

Two representations. One representation stores a full attributed type and graph node. The companion uses the smaller data Attr and passes reference count, layout compatibility, and edge typing as explicit inputs. The first mirrors the mathematical object; the second keeps every rejection premise visible.

First complete version. Define leqAttr with Unique <= Shared and no converse. Add useAllowed, then updateEligible. Finally define the list-constructor constraint as spine attribute below element attribute. Test each clause before composing the six-case oracle.

Observable result. The accepted corpus prints six named PASS lines and ends All 6 Chapter 47 corpus cases passed. The paired cases distinguish duplicated unique from duplicated shared use and unique from shared spine relinking.

A failing version. Reverse the attribute-order arguments in the constructor constraint. In the code, the affected definition is consConstraint. The program remains type-correct, but it accepts the forbidden $\mathsf{m}\le \mathsf{u}$ direction and the final inline oracle fails.

Acceptance test. Run the four commands recorded in appendix E. Require a silent check, one passing inline test, the exact seven-line run transcript, and an empty audit. Restore the accepted clause after replaying the mutation and repeat all four commands.

Mathematical boundary. The program decides six finite Boolean instances. It does not count references in a graph, construct a typing derivation, run conventional or attribute inference, establish preservation, or verify quicksort.