| store-typing | 163 | owner | function values and closures in Val: Fits contains no arrow clause | the language cut, docs/research/history/language-cut.md section 1 |
| store-typing | 96 | owner | raw subtyping in handle arms: comparisons use Equiv under Ty.subN | checker compares and joins in normalized order (decisions row 137, E4-TYPED-CE-009) |
| store-typing | 156 | owner | dangling scope handles: ScopeLive presence required at Ty.scope | machine halts on absent scope in prepareScopedExitR (E4-SCHED-CE-020) |
| residual-program-typing | 163 | owner | stored function values and closures: stored Eff syntax uses first-order program trees, while proof-side RProgram carries Lean function continuations at visible operations | the language cut, docs/research/history/language-cut.md section 1; row 163 excludes stored function values, not functions in the semantic model |
| residual-program-typing | 117 | owner | open root requirement rows: M5, M6c and M7 take the premise rootTy.requires = empty | rc.112 runs closed root rows (Effect.ts:17494-17497), while retaining separate per-position obligations |
| residual-program-typing | 148 | coordinator | general bind closure: sequencing is proved per construct via compatibility lemmas | closing marker unguard fixes exit type (E4-TYPED-CE-030) |
| scope-lifetime-finalization | 156 | owner | closure or exit of absent scopes: ScopeLive required | machine halts on absent scope in prepareScopedExitR |
| scope-lifetime-finalization | 152 | owner | badName and notImplemented defect transmission during close walk | ShapeFree exclusion on encoded causes in exit types (row 152) |
| reactive-scheduling | 106 | owner | unbounded token indices: QueueOk enforces GuardState.keysBelow | fresh token bounds protect scheduler invariants (decisions row 106) |
| reactive-scheduling | 107 | owner | defect-bearing exit boundaries: ExitOk requires NoShapeDefect | badName and notImplemented defects excluded from typed exits |
| reactive-scheduling | 134 | owner | untyped timer and race columns in configuration typing | E4-TYPED-CE-024 through CE-029 separate timer, waiter, and race keys |
| exact-codecs | 128 | owner | arbitrary syntactic equality: embeddings are exact modulo normJ and normS | JSON object key order and Schema AST annotations do not affect decoding |
| exact-codecs | 179 | coordinator | unconditional metadata preservation: normS erases only nine approved keys | arbitrary effect4/* annotations cannot be silently discarded |
| subtyping-algebra | 137 | owner | raw subtyping for checker comparisons: subN normalizes both sides first | raw sub does not distribute products over unions (E4-TYPED-CE-009) |
| subtyping-algebra | 163 | owner | arrow subtyping: Ty contains no function constructor | the language cut, docs/research/history/language-cut.md section 1 |
| initial-algebras-folds | 127 | owner | recursive-type unfolding in inhabited: inhabited is a fold over finite syntax | Ty is an inductive data type with no infinite equi-recursive unfolding |
| context-requirements | 117 | owner | open root requirement rows: M5, M6c and M7 require rootTy.requires = empty | rc.112 runs closed rows (Effect.ts:17494-17497) |
| context-requirements | 104 | owner | lexical environment capture in layers: layers build at closed points | Point.layerBuild prevents layer bodies from reading outer environments (E4-PROV-CE-005) |
| context-requirements | 105 | owner | mismatched layer values: layer value must fit declared service type | LayerHasTy requires declared service carrier and value subtyping (E4-PROV-CE-006) |
| host-session-protocol | 122 | owner | in-engine boundary decoding: Decision 12 adopts Route A typed membership | boundary decode checks membership before runtime admission (host-boundary.md section 7) |
| host-session-protocol | 97 | owner | internal handle kinds at host boundary: cells, promises, fibers, scopes refused | prevents leaking internal runtime capabilities across boundary (E4-HOST-CE-007) |
| translation-simulation | 138 | owner | non-empty host tables in M7: M7 is stated strictly on M7Fragment with root.table = [] | table-aware agreement is deferred to R6 (DI-57) |
| translation-simulation | 95 | owner | host answers on decision tapes: M6 and M7 quantify over answer-free tapes | reference machine has no host table and refuses every answer (emptyTable_refuses_every_answer) |
| translation-simulation | 117 | owner | open requirement rows: M7Fragment enforces rootTy.requires = empty | rc.112 runs closed rows (Effect.ts:17494-17497) |