feat(interval): authenticate per-node literal powers

[kim-em]

Summary

• replace configured constant/exponent values with value-agnostic dyadic and natural literal operations plus binary natural power over ordered node edges
• seed exact literal singleton facts through the checked node-indexed InitialContext and preserve exact per-node exponents across reification, runtime replay, and emitted proof construction
• retain traversal-local evaluator-proof memoization while adapting the public tactic and controller stack to transactional initial-context writes
• migrate the Rule/runtime/frontend/emitter/tactic conformance surface, including stale-update refusal and (1 / 2)^2 + (3 / 4)^3 = 43 / 64

Dependency

Stacked on #9532. This PR deliberately targets upstream main; its diff will shrink to the two literal/power commits when #9532 merges.

Validation

• lake build HexIntervalMathlib.TacticConformance HexIntervalMathlib.RuntimeEmitConformance (8,814 jobs) on the exact stacked head
• dependency DAG check
• published trust surface: 503 Lean files, no axioms, sorries, or native_decide
• diff/whitespace checks