Resolves the FIX-ω obligation D-093 §7 and D-094 §5/§7 both named as binding on "whoever implements delay/Later next" and explicitly declined to make — resolved here, not deferred a third time. Tested and falsified a plausible hypothesis before designing anything new: reg <- expr is NOT an informal Later judgment. Checked directly against StatementKind::RegisterUpdate — it type-checks the update value against the register's plain element type T with ordinary same-cycle equality; the only "guarded-feedback vocabulary" D-092/ D-093 referenced turns out to be a single boolean bypass in the unrelated mem-taint pass, not a modal type. Later<Clock,T> is therefore a real new judgment, not existing machinery to formalize. v0 needs zero new syntax — delay(init, next) already parses as an ordinary Call expression — but does need a new CheckedExprKind::Delay node and a new TypeKind::Later variant (investigated and rejected reusing TypeKind::Stamped: that's D-014 epoch-generativity, a different axis from clock-cycle timing). Scoped to one non-nested delay call per component, forced by the committed signature itself since no fixture in the corpus uses delay/feedback at all — the first doc in this series with no forcing example to scope against. FIX-ω resolved as branch (b): any linear-tracked binding referenced inside a delay's next argument is rejected outright, not ω-promoted. Branch (a) would require first deciding what "consumed via feedback" means for a grade-1 binding's end-of-scope obligation — a real separate design question, not a good bundle for this v0. (b) is sound, fully specified, needs no new UseCount variant, and closes OP-7's exact gap; (a) is named north star, not another punt. Lowering is unchanged from today's reg/seq.firreg path — Later<'d,T> is a purely compile-time causality proof with zero runtime representation once checked sound. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
versecafe committed on 8/20/2026, 4:39:42 AMparent3ee33b0
3 files changedLine totals unavailable