Guarded Feedback (delay/Later<Clock, T>, v0)

What delay/Later<Clock, T> are as a checked construct, the smallest real slice of guarded feedback that is soundly buildable now, whether reg <- expr already is an informal version of this judgment (it is not — see §2), and the FIX-ω resolution D-093 §7 and D-094 §5/§7 both named as a binding obligation and explicitly declined to make — made here, not deferred a third time. Principles in force: P-1 (no implicit behavior), P-2 (cost visible), P-3 (meaning survives lowering), P-9 (diagnostics name their judgment). This doc is the later/feedback slice of D-010's stratified judgment that 17 leaned on informally and 18/19 both fenced off as the one interaction their v0s could not reach.

Committed design

1. What's specified vs. what exists in code, re-verified

03 §5 (D-013, D-029) commits the construct precisely: "a register is delay : (init: T, next: Signal<T>) → Later<Clock, Signal<T>>; feedback is legal only through Later." next is an ordinary expression, re-evaluated every cycle — this is guarded feedback in the Nakano/Guarded-Cubical-Agda sense (a ▷/"later" modality guarding recursive occurrences so a fixed point is only well-founded if every self-reference is delayed by at least one step), but D-013 is explicit that Strata ships only the unary case — later = "next cycle in this clock domain" — not the general ∀κ-quantified guarded recursion of the proof-assistant literature: "the unary case — later = 'next cycle in this domain' — is far simpler [than full clocked type theory]... Multi-clock guarded quantification (∀κ) is DEFERRED." The comparison point named directly is Clash, where a register-free feedback loop type-checks and only fails at simulation-divergence or synthesis-time-combinational-loop time; Strata's committed improvement is that an unguarded cycle is rejected compositionally — a component's feedback port demands Later<_, T> in its own signature, so causality safety is visible from the signature alone, without opening the body (D-013 calls this out as "critical for agent composition"). A post-elaboration graph check remains as a backstop for whatever the signature-level check cannot see.

D-029's soundness content is FIX-ω, and §5's own text gives its shape directly, not just an English gloss layered on top: "the feedback rule requires FIX-ω: usage inside a feedback body is ω-promoted, because feedback re-executes every cycle and the naive rule let a 1-graded value be spent once per cycle, a bug neither QTT nor guarded recursion alone can express." The corollary D-013 records as "load-bearing and pleasant" is the reconciliation: ω-graded periodic capabilities (initiation intervals, 03 §3) remain usable in feedback — II is precisely how linearity reconciles with per-cycle reuse. This is the closest thing D-013 gives to a formal type rule; the wave-2 core-calculus probe (open-problems.md OP-7) that found the bug and proved the fix lives in probes/core-calculus/'s λ-strata⁰ fragment (23 typing + 4 WF rules), not in this doc's source tree — OP-7's entry records the finding ("the naive feedback rule accepts a 1-graded value spent once per cycle... fixed by FIX-ω (ω-promotion of feedback-body usage)") and its status as one of two GAPS-FOUND-and-repaired cross-discipline unsoundnesses in the phase-1/2 fragment, both now closed at the calculus level. What OP-7 does not give is an implementation-level algorithm against this codebase's actual linear_uses/UseCount shape — that is this doc's job, done in §5.

Re-verifying the zero-representation claim, directly. grep -n "\"delay\"\|Later\|guarded\|feedback" crates/strata-syntax/src/parser.rs crates/strata-hir/src/lib.rs crates/strata-check/src/lib.rs returns nothing — confirmed again here, third time this project has run this exact grep (D-093 §7, D-094 §5, now this doc) and gotten the identical empty result. find . -iname "*.strata" | xargs grep -ln "delay" and grep -rn "delay\|Later" fixtures/ also return nothing: no fixture in the corpus uses delay, guarded feedback, or anything Later-shaped. This is a real divergence from every prior doc in this series. D-092's mem was forced by fifo.strata's same-cycle push/pop; D-094's linear let was scoped against a construct (04's capability tokens) that at least has a named motivating shape even without a fixture. delay/Later has neither a fixture nor an existing partially-parsing surface (ghost's situation before D-093, or linear's absence before D-094 — this is the same absence, but this time there is also no forcing example anywhere in the corpus to scope against). The honest finding this doc must state plainly, matching the "smallest real forced slice" discipline every prior doc in this series used: nothing in the current corpus forces a specific shape for delay/Later. This doc's v0 is scoped directly off D-013/D-029's own committed signature instead — the only concrete evidence source available — not off a fixture, because none exists. §2 makes this scoping decision explicit rather than pretending a fixture-forced answer exists.

2. The central architectural question, resolved directly: reg <- expr is not an informal Later judgment

A plausible hypothesis, worth checking before designing anything new: maybe delay/Later is not a new primitive at all, but the formal typing story that justifies why reg name <- expr; (D-079, already implemented, already lowering to seq.firreg today) is sound — in which case v0 might mean "make RegisterUpdate checking go through a real Later-typed judgment" rather than "add delay(...) from scratch."

Checked directly against crates/strata-check/src/lib.rs's StatementKind::RegisterUpdate handling (~line 2773) — the hypothesis is false. Register-update checking is not, even informally, a Later-typed judgment. What actually happens: target's existing type want (the register's plain element type T, not Later<Clock, T> or any modally-wrapped type) is looked up, value is checked with self.expr(value, true, Some(&want)), and the result is compared for type equality against want via types_equal — ordinary same-cycle type checking, the identical code path used for let initializers and component outputs. There is no Later<_, _> type anywhere in TypeKind (§1's grep already established this), no separate "next-cycle" type distinct from T that value is checked against, and no modal wrapper stripped or introduced anywhere in this function. The only place D-092/D-093 gesture at "the guarded-feedback vocabulary" is the reject_if_tainted skip: a register update's value slot is the one place mem_tainted values are deliberately not rejected ("this is the one legal latency-boundary crossing... No reject_if_tainted call, deliberately"). That is a single boolean bypass in an unrelated taint pass (D-092's mem-read-latency bookkeeping), not a modal type judgment — it encodes "you're allowed to let a one-cycle-delayed value settle here," which is necessary but nowhere near sufficient for what Later<Clock, T> needs to mean (a type that only becomes T after crossing a clock edge, that cannot be read as T before that crossing, and that composes across component boundaries via a real type in a signature, per D-013's "critical for agent composition" claim).

The CIRCT lowering side confirms the same finding from a different angle: crates/strata-circt/src/lib.rs lowers a CheckedRegisterUpdate's value straight to %{register_name} = seq.firreg %{next_name} clock ... (~line 328) — the "next" MLIR value is just the lowered form of the checked value expression, with no intervening modal representation at any IR layer. reg <- expr works today, and works soundly for the single-register, non-recursive case, precisely because it never needed a Later type: a bare register update is a leaf construct (assign a same-cycle-computed value to a next-cycle-visible storage cell), not a recursive one. Later's actual job, per D-013's signature, is different and harder: delay(init, next) takes next: Signal<T> — an expression that is itself allowed to read the very value being delayed, closing a feedback loop, which is exactly the shape reg <- expr today has no mechanism to check at all (nothing stops, or needs to stop, a plain register update's value expression from being self-referential today, because self-reference through a bare register happens to already be guarded by the register itself at the hardware level — the checker just never had to prove that, it got it for free from seq.firreg's semantics). Formalizing Later is therefore not "give reg <- expr a type it was informally already using" — it is a new, separate judgment for a strictly more general construct (arbitrary self-referential next expressions, not just a bare storage write), and D-093/D-094's "guarded-feedback vocabulary" language in 17/18 was aspirational cross-referencing to the concept later names, not evidence of literal reusable machinery. This is the same kind of "checked directly, not assumed" finding D-092 §1 modeled for TypeKind::Array — except here the answer comes out the other way: v0 must build a real new judgment, not finish an existing informal one.

3. The v0 decision: a new delay(init, next) builtin, one non-nested call per component, no new grammar

Decision: v0 adds delay(init, next) as a recognized builtin call — not new parser grammar, since ExprKind::Call already parses arbitrary path(args) expressions generically — checked as a new CheckedExprKind::Delay { init, next } node (promoting it into checked IR the same way D-092 §6 promoted Index from a Ty-only computation), typed Later<Clock, T> via a new TypeKind::Later { domain: Option<String>, inner: Box<TypeRef> } variant. v0 scopes to exactly one, non-nested delay call per component body, its init restricted to a same-cycle, non-recursive expression, and its next restricted to referencing the delay's own result at most (no mutual feedback between two or more delays).

Syntax: nothing new to parse. crates/strata-hir/src/lib.rs::ExprKind::Call { callee, turbofish, args } (line 144) already covers delay(init_expr, next_expr) as an ordinary call expression — the same shape ghost fn calls, .wrapping_add(...)-style method calls, and every other function invocation already use. This is a genuinely different finding from D-094's linear qualifier (which needed a real new binder keyword because nothing linear-shaped existed to parse): delay needs zero strata-syntax grammar work. What's missing is entirely downstream — recognizing the callee name delay as a builtin (the same "special-case a known callee path" move calls_ghost_fn already makes for ghost fn, crates/strata-check/src/lib.rs ~line 1908) and giving it a real checked representation instead of falling through to ArtifactIneligibility::UnsupportedExpression the way an ordinary unresolved Call does today (confirmed: CheckedExprKind has no Call variant at all — every call expression that isn't specially recognized is checker-invisible past taint-walking).

Why one non-nested delay per component, not the fully general recursive-feedback case D-013's signature admits in principle. Three considerations, mirroring how D-092 §3 scoped mem to one read port/one write port rather than full multi-port:

• No fixture forces more. §1 already establishes there is nothing in the corpus to scope against. Absent a forcing example, the responsible default is the smallest slice that still exercises the actual hard part (a self-referential next argument that must be checked, not merely accepted) rather than a maximally general recursive-binding-group construct nothing currently needs.
• This is the shape D-029's own type rule is stated over. delay : (init: T, next: Signal<T>) → Later<Clock, Signal<T>> is a single function of one init/next pair; nothing in D-013/D-029 asks for N mutually-recursive delays resolved as a group (that would be closer to general guarded corecursion — letrec under ▷ — which D-013 explicitly disclaims as out of scope: "full clocked type theory exists only inside proof assistants... no programming language ships it"). Scoping to one non-nested call per component is scoping to exactly what's committed, not inventing a restriction.
• Mutual/nested feedback is real future work, not a simplicity shortcut. A design with two registers whose next-values depend on each other (a common shift-register/handshake pattern) still expresses today via two ordinary reg <- expr; statements referencing each other's current values — that pattern doesn't need delay at all, because each individual register update is still a leaf write (§2). delay/Later earns its keep specifically for the case where the feedback needs to be typed as a value — passed to or returned from a function, stored in a signature, checked for causality without opening the body — which D-013's "critical for agent composition" framing says is the whole point. v0's one-call-per-component scope is deliberately the smallest case that already needs a real value-level Later type to be sound, without also taking on multi-delay interaction, which is genuinely new design space this doc declines to open speculatively (the same posture D-092 §7 took toward true multi-port memories).

4. The Later<Clock, T> typing judgment

Later<Clock, T> as a type: "not yet, but next cycle in domain Clock." A value of type Later<'d, T> cannot be used anywhere a plain T is expected — reading it as T before crossing the clock edge it names is exactly the unguarded-cycle bug D-013 rejects compositionally. The only two legal operations in v0:

1. Introduction, via delay. delay(init: T, next: Signal<T>) -> Later<'d, T> where 'd is the clock domain the enclosing component/block is elaborated against (inferred from ambient context, matching how clock_domain-scoped bodies already resolve their domain today — no new domain-inference machinery, reusing what 07-compiler-architecture.md's domain-inference story already does for reg). init is checked as an ordinary same-cycle expression of type T, with no self-reference permitted — init may not mention the delay call's own result (there is nothing to refer to yet; this is the base case, checked the same way reg's reset(v) expression is checked today, an ordinary same-cycle typed expression with no special allowance). next is checked as an expression of type T evaluated in a scope where the delay's own result is bound, at type T (not Later<'d, T>), to a synthetic name available only inside next — this is the "peel the modality inside the guard" move guarded recursion always needs: syntactically, next may refer to the delayed value's settled value from the previous cycle, at ordinary type T, precisely because by the time next next fires, one clock edge has already elapsed. This is the "guardedness" in "guarded feedback": the self-reference is only well-typed because it is provably behind exactly one Later step, the same discipline Nakano's ▷-modality and Guarded Cubical Agda's later/fix combinator both enforce, specialized to Strata's single unary "next cycle in this domain" case rather than the general ∀κ-indexed clock-variable theory.
2. Elimination. A Later<'d, T> value may only be consumed by (a) another delay's next/init position in the same domain 'd (feedback composing with feedback), or (b) crossing into an ordinary reg <- expr; update whose target register is itself in domain 'd — the same "assign it to a reg first" discharge pattern D-092 §2's mem-taint diagnostic already tells users to use for one-cycle-delayed mem reads, reused here for the identical reason (both are "you're holding a next-cycle value; the legal way to hold onto it across the boundary is a register"). Anywhere else — a component output, a same-cycle comparison, a return value typed T — a Later<'d, T> value is rejected with a diagnostic naming the judgment (P-9): "value has type Later<'d, T>; it is not yet valid this cycle — assign it to a register or pass it to another delay's next/init before using it as T".

Checker mechanics. CheckedExprKind::Delay { init, next } is produced by a new small function paralleling fn index's promotion pattern (D-092 §6): resolve the callee path to the delay builtin, type-check init against the expected T (inferred from context — an annotated let, or the declared type of whatever the delay's result flows into), open a synthetic scope binding the delayed value's settled type (T) for next's type-checking pass, type-check next against T in that scope, and construct the checked node with a Ty::Known(TypeKind::Later { domain, inner: Box::new(T) }) result type. check_type (crates/strata-check/src/lib.rs ~line 5057) gets a TypeKind::Later { inner, .. } => check_type(inner, ...) arm, structurally identical to the existing TypeKind::Stamped { inner, .. } => check_type(inner, ...)/TypeKind::Ref(inner) => ... peeling arms already there.

Why not reuse TypeKind::Stamped for this, the way D-092 reused TypeKind::Array for mem. Checked directly rather than assumed, because the reuse move worked for D-092 and is worth trying first here too: TypeKind::Stamped { domain: Option<String>, inner, event: Option<String> } already exists and already carries a "domain" field, which looks superficially like exactly what Later<Clock, T> needs. It is not a fit. Stamped is D-014's epoch-generativity mechanism (16-syntax.md §12, §15: "stamped T — the one epoch keyword users write," "Stamped<T,D> and Crosses are elaboration-owned," the unit-epoch normalization rule) — it tags a value with which reset epoch/domain generation it belongs to, a nominal-identity concern (D-014, OP-2's adjacent territory) orthogonal to clock-cycle timing. A Later<Clock, T> value's whole point is "valid one clock edge from now, in this domain," a temporal fact about cycle count, not a generativity fact about epoch identity — the same kind of orthogonality D-092 §2 already established for mem-read latency ("later" as a timing modality) versus D-014's stamping. Conflating them would let a stamped value silently satisfy a Later obligation or vice versa, which is exactly the kind of implicit-behavior violation P-1 exists to catch. v0 needs its own TypeKind::Later variant — structurally small (two fields: an optional domain label, one inner TypeRef, mirroring Stamped's shape without adopting its semantics), but a real new variant, not a reuse.

5. FIX-ω, resolved: branch (b), structural rejection until ω-promotion ships

D-094 §5/§7 stated the obligation precisely and left it as the binding condition for "whoever implements delay/Later<_,_> checking next": "either (a) teach linear_uses to recognize a next-argument position and ω-promote any linear reference found there... or (b) structurally reject any linear reference inside a next argument until (a) is done." This doc is that implementer. Per D-093 §7 and D-094 §5's shared standing commitment ("must ship atomically with delay/Later checking, not as a follow-up"), this section makes the choice — branch (b) — and specifies it completely enough to implement in the same change as §3/§4's delay/Later checker work.

Why (b), not (a). (a) requires designing what "ω-promoted" concretely means for a LinearBinding's exactly-once obligation once a reference to it appears inside next — and that design is not as settled as it looks. The corollary D-013 §5 records ("ω-graded periodic capabilities remain usable in feedback") is about capabilities that are already ω-graded flowing into feedback cleanly; it says nothing about what happens to a grade-1 binding's own end-of-scope "must be consumed exactly once" obligation when its only reference is inside a re-executing next. Two readings are both defensible and give different answers: (i) a reference inside next discharges the obligation once, permanently, regardless of how many cycles later it's "used" again (treating the delay call itself as the one consuming event) — but this contradicts ω-promotion's own premise, which is that usage inside a feedback body is unrestricted, not single; or (ii) a reference inside next never discharges the obligation at all, because "ω" means the count is exempted from the linear tally entirely, which then raises the question of how a linear value is ever legally consumed by feedback under this reading, since nothing else counts as consumption either. Resolving this cleanly needs a real answer to "what does 'consumed' mean for a grade-1 binding whose only use is inside a construct that re-executes forever" — exactly the kind of type-system-feature design D-093 §2 and D-094 §2 both explicitly declined to bundle with a narrower, smaller v0 ("inventing both X and its checker simultaneously... is a different (and much larger) decision"). Choosing (a) here would repeat exactly the scope-bundling every prior doc in this series has consistently declined.

(b) has no such gap: it is a pure safety property (nothing that must be consumed exactly once may cross into an unrestrictedly-re-executing context at all, full stop) expressible entirely in terms of local_linear's existing membership, with no new UseCount variant, no change to linear_uses's reconciliation algebra (combine_linear_uses, Select's join rule), and no design decision about what "consumed via feedback" means — because v0 forbids the case outright rather than defining it. It closes the soundness gap OP-7 found (nothing linear can reach a feedback body unvetted, so the "spent once in source, spent once per cycle at runtime" bug is structurally unreachable, the same "unreachable by construction" property D-094 §5 wanted but couldn't get because delay didn't exist yet) while leaving (a) as a well-scoped, well-motivated future relaxation once the "what does consumption-via-feedback mean" question gets its own decision.

The concrete rule, against linear_uses's actual landed shape (crates/strata-check/src/lib.rs, commit 3ee33b0). linear_uses(expr, target, name, decl_span) gets one new match arm for the new CheckedExprKind::Delay { init, next } node from §4:

reject_linear_in_feedback_next is a new function, structurally a membership-checking sibling to mem_tainted/ghost_tainted (a flat structural walk, not a counting one — it has no single target, it asks "does any linear-tracked local appear anywhere in this subtree") rather than a sibling to linear_uses itself:

This diagnostic fires every time a linear binding is referenced inside next — including once per reference if next mentions it more than once, matching this checker's existing "fail fast, name every occurrence" posture (combine_linear_uses's double-use diagnostic already does the same). A delay call whose next argument is entirely free of local_linear members type-checks normally; init's ordinary counting is unaffected either way, because init is not a re-executing position (§4: it is the base case, evaluated once, at elaboration, exactly like any other same-cycle expression).

This is a complete resolution, not a deferral. It is deliberately conservative — it forbids some patterns a fuller (a)-shaped checker might eventually accept (a linear capability legitimately "spent" once by being folded into a feedback accumulator, for instance) — but it is sound, fully specified, and closes the exact gap D-093/D-094 both flagged as non-optional at this boundary. Per those docs' shared standing commitment, this section ships in the same change as delay/Later checking itself; there is no future doc permitted to defer this a fourth time — either the (a)-relaxation gets its own scoped decision once a concrete pattern needs it (§7's north star), or (b) stands as the permanent answer.

6. Pipeline ownership

• strata-syntax. No changes. delay(init, next) parses today as an ordinary Call expression (§3) — the first construct in this decision series (D-092/093/094/095) where the syntax layer needs zero new grammar for its v0.
• strata-hir. No new StatementKind (unlike ghost let/linear let, delay is an expression builtin, not a statement-shaped binder) — ExprKind::Call already lowers correctly; recognition of delay as a builtin happens entirely in strata-check, the same layering calls_ghost_fn already uses (HIR doesn't need to know delay is special, only the checker does). One addition: TypeKind::Later { domain: Option<String>, inner: Box<TypeRef> } (§4), a peer of TypeKind::Stamped.
• strata-check. The bulk of the work: (a) a delay-callee-recognition path structurally paralleling calls_ghost_fn's existing callee-path matching; (b) CheckedExprKind::Delay { init: Box<CheckedExpr>, next: Box<CheckedExpr> }, promoted the way Index was promoted from a Ty-only computation (D-092 §6); (c) the Later<'d, T> typing judgment from §4 — introduction via delay, elimination only into another delay's next/init or a same-domain reg <- expr;, rejected everywhere else with a named diagnostic; (d) a TypeKind::Later peeling arm in check_type; (e) the FIX-ω resolution from §5 — reject_linear_in_feedback_next and the one new linear_uses match arm, landed in the same change as (a)-(d), per §5's non-deferrable commitment.
• strata-arch-ir / strata-circt. A delay call that passes checking lowers to exactly the same seq.firreg shape a reg/reg <- expr pair already produces today (§2 already established that reg <- expr needed no Later machinery to lower correctly) — delay(init, next) elaborates to a synthesized register (reset value init, next-cycle value the lowered form of next, next's self-reference resolved to a read of that same register's current value) plus a Binding::Register entry, reusing CheckedRegisterUpdate's existing lowering path unchanged. This is worth stating explicitly, mirroring D-093 §6's "no changes at all" framing for grade 0's arch-IR story: Later<'d, T> is a purely compile-time causality-and-timing proof about how a value came to exist; once it's checked sound, the synthesized hardware is indistinguishable from hand-written reg/reg <- expr. No new arch-IR node type, no new CIRCT op — delay's entire contribution is at the type-checking layer, exactly as D-013's "critical for agent composition" framing implies (the value it adds is a checked signature-level guarantee, not new runtime behavior).

7. v0 scope

In v0:

• delay(init, next) recognized as a builtin call (§3) — no new grammar, a new CheckedExprKind::Delay node and a new TypeKind::Later { domain, inner } type.
• Exactly one, non-nested delay call per component body; init restricted to a same-cycle, non-self-referential expression; next may refer only to that same delay's own settled value (no mutual feedback between two or more delays).
• The Later<'d, T> typing judgment (§4): introduction via delay, elimination only into another delay's next/init (same domain) or an ordinary reg <- expr; update (same domain) — rejected everywhere else with a named diagnostic.
• FIX-ω, resolved as branch (b): any linear-tracked binding referenced inside a delay's next argument is rejected outright, via reject_linear_in_feedback_next and one new linear_uses match arm, shipped in the same change as the rest of this v0 — not deferred.
• Lowering: a checked delay produces exactly the seq.firreg shape a hand-written reg/reg <- expr pair already produces — no new arch-IR node, no new CIRCT op.
• TypeKind::Later is a distinct variant from TypeKind::Stamped — investigated and rejected as a reuse target (§4): Stamped is D-014 epoch-generativity, a different axis from clock-cycle timing.

Deferred (north star), and why each is safely deferrable:

• Multiple/mutual delay calls in one component, general guarded corecursion. No fixture and no committed spec text (§3) asks for more than the unary single-call case; D-013 itself disclaims full clocked type theory / general ∀κ guarded recursion as out of scope. Extending beyond one call is a real future decision once a concrete multi-register feedback pattern forces it, the same "wait for a fixture" discipline D-092 §7 used for multi-port memories.
• FIX-ω branch (a) — ω-promotion of linear references inside next, as a relaxation of §5's branch (b). Not implementable soundly without first answering what "consumed via feedback" means for a grade-1 binding's end-of-scope obligation (§5's two-reading gap) — a real, separate type-system design question this doc declines to bundle with the smaller, sound v0, the same posture D-093/D-094 both took toward D-039's fuller capability-token design.
• Multi-clock guarded quantification (∀κ), cross-domain delay. D-013 §5 names this DEFERRED directly; cross-domain feedback stays routed through the existing typed CDC bridge (04 §7), sidestepping the multi-clock modality entirely, exactly as D-013 already commits.
• A declared combinational-read escape hatch or any interaction with mem's own later-modality vocabulary (17 §2). mem's registered-read timing and delay's feedback typing are both instances of the same "next cycle" concept at the type-system level (§4 gives Later<'d,T> a real definition for the first time), but unifying mem's informal "reuses the guarded-feedback vocabulary" language with this doc's actual TypeKind::Later is a genuine follow-on integration this doc does not do — mem reads keep their current ad hoc one-cycle-latency taint-based enforcement (D-092 §2/§6) unchanged in v0; retrofitting mem reads to be typed Later<'d, T> for real is future work, named here so it isn't lost.
• The post-elaboration whole-graph causality check D-013 §5 names as a backstop to the signature-level Later check. v0 relies on the signature-level check alone (§4); the graph-level backstop is real future robustness work, not required for v0's single-call, non-nested scope to be sound (a lone delay call cannot form an unguarded cycle the signature check misses — the backstop earns its keep once multiple delays/components compose, which is itself deferred above).

North star

FIX-ω branch (a) as a scoped, separately-decided relaxation once a concrete pattern (most likely a capability-token or credit value legitimately "spent" once by folding into a feedback accumulator) forces the "what does consumption-via-feedback mean" question to be answered rather than sidestepped; multi-delay/mutual-feedback support and the general guarded-corecursion case; multi-clock guarded quantification (∀κ) once cross-domain feedback needs more than the CDC-bridge escape hatch already provides; unifying mem's informal one-cycle-latency enforcement with this doc's real TypeKind::Later judgment so the checker has one timing modality instead of two parallel ad hoc ones; the post-elaboration whole-program causality graph check as a backstop once multi-delay composition exists to need one.

Open problems touching this doc

OP-7 (one core calculus) — this doc is the "whoever implements delay/Later<_,_> checking next" both 18 §7 and 19 §5/§7 named as owing FIX-ω atomically with feedback typing; §5 discharges that obligation by choosing and fully specifying branch (b) (structural rejection) rather than deferring a third time. The core-calculus probe's FIX-ω rule (ω-promotion) is proven sound at the calculus level (probes/core-calculus/); this doc's branch (b) is a strictly more conservative implementation choice than the calculus's own fix, not a contradiction of it — v0 simply doesn't yet build the (a)-shaped checker the calculus's rule would need to be realized as ω-promotion rather than rejection. OP-8 (dynamic-latency capabilities) is adjacent — delay's Later<Clock,T> is a fixed, statically-known one-cycle delay, the Filament-lineage static-interval case OP-8's committed stance already scopes phase 2 to; nothing in this doc engages OP-8's dynamic-latency question.