[ET-L2] ET-6/ET-7: Structural Gate absent (no additive pairs, no refusal statement)

[hyperpolymath]

src/kernel/Anytype/Core/Check.idr:69-83 has multiplicative TProd/LetPair only — no additive & with CAR/CDR, no subject-reduction proof, and no statement of the refused structural classes. The admitted/refused classes are specified in systemet docs/theory/ (Structural Gate doc); the kernel needs the admitted fragment implemented and the refusal boundary stated. Cites: ET-6, ET-7.

🤖 Generated with Claude Code