interval: replay rational arithmetic edges

[kim-em]

Summary

• add a strategy-neutral table-indexed edge language for add, sub, mul, total inv, eq, le, and lt
• validate every reference and preflight the complete edge list's lookup, temporary-width, and arithmetic-work budgets before evaluating any integer cross-product
• replay naive integer identities over canonical raw rationals and prove that ready establishes every indexed edge's Core Rat proposition
• cover signed values, zero arithmetic and 0⁻¹ = 0, every operation failure, each reference role, exact/one-short resources, and later preflight failures outranking earlier false identities

Resource boundary

Temporary widths use zero-aware multiplication and addition/subtraction bounds and include every intermediate in the SPEC identity. Arithmetic work is a fixed per-edge aggregate computed only from bounded internal counters, checked against a caller-owned remaining total, and never supplied by the certificate. Complete canonical-table gcd input/work accounting comes from stacked PR #8950.

Validation

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

No native_decide, norm_num, Grind, axiom, or sorry. This is stacked on #8950; independent source audit found no arithmetic or proof defect, and fresh Opus/CI reviews will run asynchronously.