Elaborate literal Grammar-v1 Bytes sizes exactly

[abiggerhammer]

Summary

Continue Matrix SURF-008 / ledger PHIL-SURFACE-ELAB-001 with a bounded Bytes[...] type bridge built only on the already-verified context-free Nat literal elaboration from #477.

Contract

• Bytes[0], Bytes[7], and other decimal Nat literals map exactly to Core TyBytes (RefNat n);
• only RefNat results are accepted as intrinsic byte sizes;
• Bytes[n] remains unresolved until a competent binding-aware name elaborator establishes the identity and Nat sort of n;
• non-Bytes types remain outside this bridge;
• the bridge never invents a source-name binding merely to form TyBytes.

Executable pressure

Phase1GrammarV1IntrinsicBytesTypeElaborationMain.hs parses Bytes[0], Bytes[7], Bytes[n], and a non-Bytes type. The literal sizes must elaborate exactly; the contextual name and non-Bytes form must fail closed.

This is the eighth bounded SURF-008 slice after #462, #464, #466, #468, #471, #474, and #477; full Grammar-v1 elaboration correspondence remains open.