interval: compose operation semantics from packages

[kim-em]

Summary

• add function-independent operation meanings assembled from package relations
• require an aligned meaning for every expression node and derive generic prefix stability
• generalize the Real.exp proof schema to arbitrary exponential nodes, with a nested-exp theorem and fail-closed source-node test

Trust boundary

• no native_decide, axioms, or sorries
• runtime package lookup is data; all semantic consequences remain ordinary kernel proofs
• syntax-to-relation linking and ordered seed discharge remain explicit next steps in the SPEC

Validation

• lake build HexInterval.Experiment.OperationSemantics HexIntervalMathlib.Experiment.ExpSign HexIntervalMathlib.ExpSignConformance
• copyright, line-count, DAG, trust-surface, diff, and factor-freshness checks