Compose verified binding-aware Grammar-v1 types

[abiggerhammer]

Summary

Continue Matrix SURF-008 / ledger PHIL-SURFACE-ELAB-001 by composing the already-verified context-free type dispatcher with the live Nat-bound Bytes[...] bridge from #499 and binding-aware Proof[...] bridge from #509.

Contract

• primitive Unit/Bool/U, literal-sized Bytes, unspecialized Frame, narrow lossless Validated, and other already-verified context-free forms retain exactly the Compose verified Validated routing into intrinsic Grammar-v1 types #496 dispatcher meaning;
• Bytes[...] additionally admits only the Elaborate live Nat-bound Grammar-v1 Bytes types exactly #499 live simple-name Nat-index form; literal and live-name routes are the two already-verified fragments, not new fallback semantics;
• Proof[...] delegates only to the Compose live Grammar-v1 propositions into Proof types #509 binding-aware Proof bridge, which already includes intrinsic and live relation/claim leaves under exact logical composition;
• wrong-sort, unknown, or consumed bindings, arithmetic/projection/specialization, named/tuple/refinement and other unresolved contextual forms remain fail-closed;
• no new binding, type identity, element mode, coercion, sort rule, evidence, static specialization, or fallback interpretation is invented.

Executable pressure

The existing Phase1GrammarV1IntrinsicTypeCompositionMain.hs audit gate now also pressures the composed binding-aware type dispatcher from real Grammar-v1 source. It covers intrinsic types, literal and live Nat Bytes, live and intrinsic Proof types, Frame and Validated preservation, and fail-closed wrong-sort/unknown Bytes plus unknown, consumed, arithmetic, and specialized Proof leaves. The existing Audit Reconciliation workflow already owns this gate.

This is the twenty-fifth bounded SURF-008 slice after #462, #464, #466, #468, #471, #474, #477, #478, #481, #482, #485, #486, #488, #489, #491, #492, #494, #496, #498, #499, #501, #505, #506, and #509; full Grammar-v1 elaboration correspondence remains open.