diff --git a/current/CHECKPOINT-REIFY.md b/current/CHECKPOINT-REIFY.md
index a94b4612..b7e7004d 100644
--- a/current/CHECKPOINT-REIFY.md
+++ b/current/CHECKPOINT-REIFY.md
@@ -120,6 +120,38 @@ Then F2 (reify→sx + general comptime-Type-decl eval, delete `reifyType`), F3 (
 body eval, delete `findReturnReifyCall`, re-green 0615/0617), F4 (make_enum in sx),
 F5 (validation). `type_info` (old 2.2) stays orthogonal/pending.
 
+**END STATE IS NON-NEGOTIABLE: ZERO `reify` in the compiler.** `reifyType`, the
+`E :: reify(...)` decl hook (`decl.zig` ~660), and `findReturnReifyCall` routing
+(`generic.zig`) must ALL be deleted by the end of the floor work — `reify` lives only
+in `meta.sx`. The compiler keeps only `declare`/`define` (+ the generic comptime
+Type-expr evaluation that runs them). Removal can't precede the floor (the reify
+examples would have no path), so the floor + removal land together; the suite must
+never be left red across a session boundary.
+
+### F1 investigation findings (verified 2026-06-16 — don't re-derive)
+- **Pass order** (`decl.zig:lowerRoot`): Pass 1 `scanDecls` (line 441 — registers all
+  types; the old reify hook mints here) → Pass 1f `UnknownTypeChecker` → Pass 2
+  `lowerMainAndComptime` (1320 — force-lowers `main` via `lazyLowerFunction`, which
+  transitively lowers bodies; also *creates* `#run` comptime fns). `#run` side-effects
+  EXECUTE only at emit time (`emit_llvm.zig:runComptimeSideEffects`).
+- **`define` timing:** must run AFTER scanDecls (needs all types) but BEFORE body
+  lowering (match/construct resolve variant indices at lower-time, Pass 2). Neither
+  existing hook fits → add a **new Pass 1g** (after `scanDecls`, before
+  `lowerMainAndComptime`) that executes recorded `declare`/`define` pairs via the
+  interp. Self-ref works because `declare` binds the name in Pass 1, so `*List` in the
+  `define` body resolves.
+- **Parse constraint:** a bare top-level `define(List, ...)` does NOT parse
+  (`expected '::' / ':=' / ':' after identifier`). So `define` is invoked either via a
+  recognized top-level form or `#run define(...)` whose comptime fn Pass 1g executes
+  early (instead of waiting for emit). Decide the surface in F1.
+- **Builtin dispatch:** `resolveBuiltin` (`call.zig:1297`) is a tiny name→`BuiltinId`
+  table; `reify`/`type_info`/`field_type` are NOT there — they're recognized
+  syntactically (decl hook / `tryLowerReflectionCall` at `call.zig:1679`). `declare`/
+  `define` need their own dispatch (likely comptime interp builtins, since they mutate
+  the type table at comptime).
+- **Salvage:** the reverted eval-decode (`reifyEnumFromVariantsValue` +
+  `decodeVariantElements`, commit `4d6c463` in reflog) IS `define`'s decode core.
+
 ### (superseded) earlier Next step — `type_info` value construction Reflect a type into a `TypeInfo`
 *value* — the inverse of reify. Two sub-pieces, both non-trivial: (a) widen the
 `meta.sx` `TypeInfo` data model beyond `` `enum `` (struct / tuple variants); (b)