Certified native runtime

Runtime declarations referenced by generated tensor-pattern terms. The elaborator and planners remain meta-level implementation modules; this facade contains the executable loops, builders, and their semantic correctness theorems.