Elaborate live Grammar-v1 relation operands exactly

[abiggerhammer]

Summary

Continue Matrix SURF-008 / ledger PHIL-SURFACE-ELAB-001 by composing the verified intrinsic-literal and live-simple-reference bridges into Grammar-v1 relation leaves, with the existing Core proposition sort checker as the competence boundary. Repair the Grammar-v1 proposition parser so relation operands are parsed as complete additive expressions before shorter proposition forms are selected.

Contract

• each relation operand must already have verified reference-term meaning: either an intrinsic scalar literal from Elaborate Grammar-v1 scalar literals to Core reference terms #477 or a live unqualified, unspecialized, zero-argument binding from Elaborate live Grammar-v1 simple references exactly #498;
• proposition parsing probes the complete relation_proposition production first without consuming input, so identifier-, literal-, and parenthesis-led relation operands retain their full additive-expression structure;
• the parser-selected relation operator is preserved exactly through the Route Grammar-v1 relations to exact Core propositions #468 mapping, including canonical operand reversal for > / >=;
• the completed proposition is accepted only when the existing checkPropositionSorts checker succeeds against the current Core state;
• same-sort Boolean/UInt/Nat equality and valid Nat/UInt ordering may therefore elaborate exactly;
• sort mismatches, invalid ordered sorts, unknown/consumed names, qualification, specialization, calls, projections, arithmetic/compound operands, and non-relation propositions remain fail-closed at elaboration;
• no new binding table, sort rule, coercion, fallback relation interpretation, or evidence is introduced.

Executable pressure

The existing Phase1GrammarV1RelationElaborationMain.hs gate now also pressures binding-aware relation elaboration from real Grammar-v1 source: exact Nat ordering, mixed live-Nat/literal comparison, Boolean equality, UInt equality, and greater-than canonicalization. It parses projection and arithmetic relations including (n).field == n and n + 1 == m while confirming those richer operands still fail closed in the bounded elaborator, along with sort mismatch, Boolean ordering, unknown, qualified, specialized, called, consumed, and non-relation forms.

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