interval: budget canonical-table gcd work

[kim-em]

Summary

• add caller-owned maxGcdInputBits and aggregate maxGcdWork limits to the canonical raw-rational table boundary
• preflight every entry's gcd operand widths and nonzero work proxy before invoking Nat.gcd
• thread remaining work through the complete table and report the first entry whose gcd cannot run
• preserve deterministic per-entry failure ordering and all canonicality/value-field proofs

Cost model

The reference work proxy is max 1 numeratorBits * max 1 denominatorBits, so canonical zero and every other gcd invocation consume nonzero budget. Each input must first fit maxGcdInputBits; a successful entry subtracts its cost from the caller-owned remaining aggregate.

Exact/one-short conformance covers the input cap, canonical zero, cumulative exhaustion, an otherwise unused tail, and logical/resource precedence.

Validation

• lake build HexIntervalExperiment +HexInterval.RationalTableConformance:olean +HexInterval.RationalCertificateConformance:olean
• python3 scripts/check_dag.py
• forbidden-token scan and git diff --check

No native_decide, norm_num, Grind, axiom, or sorry. This is a stacked draft on #8944; independent audit and Opus review will run asynchronously.