feat(interval): prove exact dyadic fact semantics

[kim-em]

Summary

• interpret the checked open/closed/unbounded dyadic interval facts as subsets of ℝ
• prove successful executable intersection is exactly semantic conjunction and install it as the generic FactDomainSchema
• exercise strict ties, empty intersections, independently unbounded inputs, and transparent generic target weakening

Exact reconciliation

• base: c216fe2fb744cac7d503511c68402a03c9aeaea2 (post-Table12 main)
• head: af0b1226036933c001c70554774a9ac907d98f96
• preserves PNT log-table, nested-log, exponential-tail, and Table12 examples plus all earlier interval content
• proof-only Lake freshness exemption is pinned to exact resolved lakefile.lean blob db3b912684e66f7e9759d5e19e9695b262211fc0

Verification

• lake build HexIntervalMathlib.Experiment.DyadicInterval HexIntervalMathlib.DyadicIntervalConformance HexInterval.NestedBranchConformance HexIntervalMathlib.PntLogTableConformance HexIntervalMathlib.PntNestedLogConformance HexIntervalMathlib.PntExpTailConformance HexIntervalMathlib.PntTable12Conformance HexIntervalMathlib.ReluConformance (2241 jobs)
• copyright, file-line, DAG, trust-surface, Phase 4, factor-freshness, PNT-inventory, and diff checks
• guarded axiom report: only propext, Classical.choice, and Quot.sound
• no added native_decide, axiom, sorry, admit, unsafe, or implemented_by
• fresh exact-head Opus review and exact-head CI required before merge readiness