feat(interval): add ordered bounds constructor

[kim-em]

Summary

• add a sealed interval constructor for independently preflighted ordered dyadic bounds
• expose exact closed-bounds semantics and general agreement with admitted checked constructors
• provide a comparison-free proof transport from an already-established rational endpoint inequality
• add cross-module conformance, including a far-exponent canary, while keeping untrusted callers on capped Within APIs
• state the opaque boundary explicitly: the view theorem supports semantic proof quotation, but DecidableEq-based replay cannot reduce through the sealed constructor and needs a separate exact initial-target evidence path

This is the semantic quotation artifact identified by the bounded raw-token rational experiment. It does not add rational syntax, make the sealed representation transparent, or claim to solve generic runtime replay by itself.

Validation

• prior full lake build: 10,003 jobs
• exact rebased head: HexIntervalMathlib.IntervalConformance, 8,802 jobs
• published trust surface: 503 Lean files, no axioms, sorries, or native_decide
• copyright, dependency-DAG, conformance, forbidden-token, and diff checks

[kim-em]

Strengthened exact head to f9dad8a10 after a clean combined consumer build exposed a stale-transitive-import defect that warm artifacts had masked. The Mathlib semantics module now imports HexInterval.Canonical directly. This head also adds a non-computing ordered_of_consistent proof route and the general checked/unchecked agreement theorem eq_ordered_ofRawWithin; conformance examples no longer present a bare order by decide as the usage pattern. Focused core, Mathlib, and conformance builds plus DAG/trust/header/forbidden/diff checks are green. Replacement exact-head CI and fresh review are required before merge.