diff --git a/AGENTS.md b/AGENTS.md
index bcebdea550..cceb568c37 100644
--- a/AGENTS.md
+++ b/AGENTS.md
@@ -258,8 +258,13 @@ normally the part of the contract that matters.
 ## 4. Documentation
 
 Use JSDoc for module documentation in both TypeScript and JavaScript source.
-Every implementation module starts with one module JSDoc block, followed by one
-blank line before the first source-level import or declaration.
+The `@module` tag belongs only to a package's entry-point file — `module.f.ts` /
+`module.f.mjs` / `module.ts` / `module.mjs` — not to `proof.f.ts` / `proof.f.mjs`,
+`types.ts`, or any other file. A `module.*` file starts with one module JSDoc
+block carrying `@module`, followed by one blank line before the first
+source-level import or declaration. A `proof.*` or other non-`module.*` file has
+no `@module` tag and no required leading documentation block; one is still
+needed if the file has `@import` tags to hold, per below.
 
 For TypeScript, put type-only imports first, external or built-in runtime imports
 second, then repository-owned relative runtime imports: already-migrated
@@ -286,10 +291,14 @@ import ... from '...ts'
 import ... from '...ts'
 ```
 
-For JavaScript, put all module-level `@import` tags in the same leading JSDoc
-block as `@module`, then put one blank line before runtime imports. External or
-built-in runtime imports come first, followed by repository-owned relative
-`.mjs` runtime imports:
+For JavaScript, group all module-level `@import` tags into one leading JSDoc
+comment block — the same block as `@module` in a `module.*` file, or a
+standalone block at the top of the file otherwise — then put one blank line
+before runtime imports. Do not scatter `@import` tags as separate comments
+between or after individual `import` statements. External or built-in runtime
+imports come first, followed by repository-owned relative `.mjs` runtime
+imports, matching the TypeScript order of type imports, then `.mjs` imports,
+then remaining `.ts` imports:
 
 ```js
 /**
@@ -308,15 +317,31 @@ import ... from '...mjs'
 import ... from '...mjs'
 ```
 
-Do not put module-level `@import` tags in separate JSDoc comments. The `.mjs` /
-`.ts` grouping and the Stage 1 migration restriction apply to repository-owned
-relative runtime imports, not to external or built-in modules. During Stage 1, a
-migrated JavaScript module has no remaining relative runtime `.ts` / `.f.ts`
-import group: migrated JavaScript may depend at runtime on external modules and
-migrated repository JavaScript, but not on remaining authored TypeScript
-implementations. The blank line after the module JSDoc block is required even
-when the module has no `@import` tags; it keeps the header detached from the first
-import/declaration and preserves it through declaration emit.
+A non-`module.*` file (e.g. `proof.f.mjs`) with `@import` tags but no `@module`
+uses the same grouping without the tag:
+
+```js
+/**
+ * @import ...
+ * @import ...
+ */
+
+import ... from 'node:...'
+import ... from 'package'
+
+import ... from '...mjs'
+import ... from '...mjs'
+```
+
+The `.mjs` / `.ts` grouping and the Stage 1 migration restriction apply to
+repository-owned relative runtime imports, not to external or built-in modules.
+During Stage 1, a migrated JavaScript module has no remaining relative runtime
+`.ts` / `.f.ts` import group: migrated JavaScript may depend at runtime on
+external modules and migrated repository JavaScript, but not on remaining
+authored TypeScript implementations. In a `module.*` file, the blank line after
+the leading JSDoc block is required even when the module has no `@import` tags;
+it keeps the `@module` header detached from the first import/declaration and
+preserves it through declaration emit.
 
 Where each kind of documentation belongs:
 
diff --git a/CHANGELOG.md b/CHANGELOG.md
index c0f7f47538..f87c25bfa5 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -20,6 +20,15 @@ history.
 
 ## Unreleased
 
+- **BREAKING CHANGES:** `fjs/media/json/tokenizer/proof.f.ts` migrates
+  from authored TypeScript to JSDoc-typed JavaScript (`.f.mjs`) — the
+  typed `tokenizeString` const becomes a JSDoc `@type` annotation, and
+  the `JsonToken` type import becomes an `@import`
+  [#1504](https://github.com/functionalscript/functionalscript/pull/1504)
+- **BREAKING CHANGES:** `fjs/media/json/proof.f.ts` migrates from
+  authored TypeScript to JSDoc-typed JavaScript (`.f.mjs`) — two nested
+  `as unknown as null` double-casts become nested inline `@type` casts
+  [#1504](https://github.com/functionalscript/functionalscript/pull/1504)
 - **BREAKING CHANGES:** `fjs/effects/proof.f.ts` and
   `fjs/effects/eff/proof.f.ts` migrate from authored TypeScript to
   JSDoc-typed JavaScript (`.f.mjs`) — explicit generic instantiations
diff --git a/fjs/media/json/proof.f.ts b/fjs/media/json/proof.f.mjs
similarity index 96%
rename from fjs/media/json/proof.f.ts
rename to fjs/media/json/proof.f.mjs
index 2f0b133026..3ed325fc62 100644
--- a/fjs/media/json/proof.f.ts
+++ b/fjs/media/json/proof.f.mjs
@@ -15,12 +15,12 @@ export const proof = {
         },
         () => {
             // typeof src !== 'object': primitive src treated as empty object
-            const x = stringify(sort)(setProperty("Hello")(['a'])(42 as unknown as null))
+            const x = stringify(sort)(setProperty("Hello")(['a'])(/** @type {null} */ (/** @type {unknown} */ (42))))
             if (x !== '{"a":"Hello"}') { throw x }
         },
         () => {
             // src instanceof Array: array src treated as empty object
-            const x = stringify(sort)(setProperty("Hello")(['a'])([1, 2] as unknown as null))
+            const x = stringify(sort)(setProperty("Hello")(['a'])(/** @type {null} */ (/** @type {unknown} */ ([1, 2]))))
             if (x !== '{"a":"Hello"}') { throw x }
         },
     ],
diff --git a/fjs/media/json/todo/stringify-sorted-canonical.md b/fjs/media/json/todo/stringify-sorted-canonical.md
index e195d769c7..a0ac2689c9 100644
--- a/fjs/media/json/todo/stringify-sorted-canonical.md
+++ b/fjs/media/json/todo/stringify-sorted-canonical.md
@@ -55,7 +55,7 @@ applications once.
 ## Tasks
 
 - [ ] Add `stringifySorted` to `fjs/media/json/module.f.mjs` with proof
-      coverage in `fjs/media/json/proof.f.ts` (which itself calls
+      coverage in `fjs/media/json/proof.f.mjs` (which itself calls
       `stringify(sort)` seven times today).
 - [ ] Migrate the two source-module sites (`fjs/protocol/mcp/stdio/module.f.mjs`,
       `fjs/djs/module.f.mjs`), then the proof files.
diff --git a/fjs/media/json/tokenizer/proof.f.ts b/fjs/media/json/tokenizer/proof.f.mjs
similarity index 98%
rename from fjs/media/json/tokenizer/proof.f.ts
rename to fjs/media/json/tokenizer/proof.f.mjs
index 5d78ae787f..0404e657ae 100644
--- a/fjs/media/json/tokenizer/proof.f.ts
+++ b/fjs/media/json/tokenizer/proof.f.mjs
@@ -1,13 +1,15 @@
+/**
+ * @import { JsonToken } from './types.ts'
+ */
+
 import { tokenize } from './module.f.mjs'
-import type { JsonToken } from './types.ts'
 import { toArray } from '../../../types/list/module.f.mjs'
 import { stringifyAsTree } from '../../../djs/serializer/module.f.mjs'
 import { sort } from '../../../types/object/module.f.mjs'
 import { stringToList } from '../../../text/utf16/module.f.mjs'
 
-const tokenizeString
-    : (s: string) => readonly JsonToken[]
-    = s => toArray(tokenize(stringToList(s)))
+/** @type {(s: string) => readonly JsonToken[]} */
+const tokenizeString = s => toArray(tokenize(stringToList(s)))
 
 const stringify = stringifyAsTree(sort)
 
diff --git a/todo/migrate-typescript-to-mjs.md b/todo/migrate-typescript-to-mjs.md
index 947da3c667..a119509dd5 100644
--- a/todo/migrate-typescript-to-mjs.md
+++ b/todo/migrate-typescript-to-mjs.md
@@ -239,9 +239,10 @@ Use `@template out T`, `@template in T`, or constrained forms such as
 
 A JavaScript implementation must not gain a real JavaScript import just because
 it uses a separately declared type. Use JSDoc `@import` with the same real source
-path used by `import type`. All module-level `@import` tags belong in the leading
-module JSDoc block together with `@module`; do not create separate `@import`
-comment blocks.
+path used by `import type`. All module-level `@import` tags belong in one
+leading JSDoc block — sharing it with `@module` in a `module.*` file, or
+standing alone at the top of a `proof.*` or other non-`module.*` file, which
+does not carry `@module`; do not create separate `@import` comment blocks.
 
 The corresponding TypeScript implementation uses `import type` with the same
 specifier:
@@ -250,7 +251,7 @@ specifier:
 import type { Types } from './types.ts'
 ```
 
-JavaScript uses:
+JavaScript in a `module.*` file uses:
 
 ```js
 /**
@@ -262,6 +263,15 @@ JavaScript uses:
  */
 ```
 
+JavaScript in a `proof.*` file (or any other non-`module.*` file, which has no
+`@module` tag) groups the same `@import` tags without one:
+
+```js
+/**
+ * @import { Types } from './types.ts'
+ */
+```
+
 Do not point migrated JavaScript back at a remaining implementation `.ts` /
 `.f.ts` merely for a type. If that type must survive independently of the
 implementation, move or split it into `types.ts` first. If it is naturally
@@ -379,8 +389,11 @@ rediscovered by each migration.
 
 #### Module header and import ordering
 
-Every implementation module starts with one module JSDoc block. Always put one
-blank line after that block before the first source-level import or declaration.
+The `@module` tag belongs only to a package's entry-point file — `module.f.ts` /
+`module.f.mjs` / `module.ts` / `module.mjs`. It is not required on `proof.f.ts` /
+`proof.f.mjs`, `types.ts`, or any other file. A `module.*` file starts with one
+leading JSDoc block carrying `@module`; always put one blank line after that
+block before the first source-level import or declaration.
 
 For TypeScript, put type-only imports first, external or built-in runtime imports
 second, then repository-owned relative runtime imports: already-migrated
@@ -407,10 +420,14 @@ import ... from '...ts'
 import ... from '...ts'
 ```
 
-For JavaScript, put all module-level `@import` tags in the same leading JSDoc
-block as `@module`, then put one blank line before runtime imports. External or
-built-in runtime imports come first, followed by repository-owned relative
-`.mjs` runtime imports:
+For JavaScript, group all module-level `@import` tags into one leading JSDoc
+block — sharing that block with `@module` in a `module.*` file, or standing
+alone at the top of a `proof.*` or other non-`module.*` file — then put one
+blank line before runtime imports. Never scatter `@import` tags as separate
+comments interleaved with individual `import` statements. External or built-in
+runtime imports come first, followed by repository-owned relative `.mjs`
+runtime imports, matching the same order as TypeScript: type imports, then
+`.mjs` imports, then remaining `.ts` imports:
 
 ```js
 /**
@@ -429,6 +446,22 @@ import ... from '...mjs'
 import ... from '...mjs'
 ```
 
+A `proof.*` or other non-`module.*` file with `@import` tags uses the same
+grouping without a `@module` tag:
+
+```js
+/**
+ * @import ...
+ * @import ...
+ */
+
+import ... from 'node:...'
+import ... from 'package'
+
+import ... from '...mjs'
+import ... from '...mjs'
+```
+
 The `.mjs` / `.ts` grouping and the Stage 1 migration restriction apply only to
 repository-owned relative runtime imports. External or built-in imports are not
 migration edges and may remain where the module design requires them. A migrated
@@ -724,13 +757,15 @@ this rename.
       than by what the `.f.ts` happened to export or by what a pending refactor
       plans to delete. Types intentionally moved to `types.ts` use normal
       TypeScript source visibility instead.
-- [ ] Apply the module-header/import convention: keep module-level JavaScript
-      `@import` tags in the same JSDoc block as `@module`, always put one blank
-      line after that block, group external/built-in runtime imports separately,
-      and order repository-owned relative runtime imports as migrated `.mjs`
-      before remaining `.ts`; fix the modules that already lose their header
-      (`fjs/common/monoid`, `fjs/types/btree/remove`, `fjs/types/btree/set`,
-      `fjs/types/list`, `fjs/types/nullable`).
+- [ ] Apply the module-header/import convention: `@module` belongs only to
+      `module.*` entry-point files, never to `proof.*` or other files; group
+      module-level JavaScript `@import` tags into one leading JSDoc block —
+      sharing it with `@module` in a `module.*` file, standing alone otherwise —
+      always put one blank line after that block, group external/built-in
+      runtime imports separately, and order repository-owned relative runtime
+      imports as migrated `.mjs` before remaining `.ts`; fix the modules that
+      already lose their header (`fjs/common/monoid`, `fjs/types/btree/remove`,
+      `fjs/types/btree/set`, `fjs/types/list`, `fjs/types/nullable`).
 - [ ] File an upstream issue for JSDoc typedef documentation being dropped from
       declaration emit, and keep writing type documentation in the source
       meanwhile; substantial type APIs may instead live directly in `types.ts`
@@ -803,11 +838,13 @@ this rename.
   JSDoc `@typedef` is recorded as a known upstream gap; an intentionally separate
   `types.ts` may preserve declaration documentation through normal TypeScript
   emit.
-- Every implementation module follows the module-header/import convention:
-  JavaScript keeps module-level `@import` tags in the same JSDoc block as
-  `@module`, one blank line follows that block, external/built-in runtime imports
-  form their own group, and repository-owned relative runtime imports are ordered
-  as migrated `.mjs` before remaining `.ts`. The `@module` header survives
+- Every module-level import follows the module-header/import convention:
+  `@module` appears only on `module.*` entry-point files, never on `proof.*` or
+  other files; JavaScript groups module-level `@import` tags into one leading
+  JSDoc block — shared with `@module` where present, standing alone otherwise —
+  one blank line follows that block, external/built-in runtime imports form
+  their own group, and repository-owned relative runtime imports are ordered as
+  migrated `.mjs` before remaining `.ts`. The `@module` header survives
   declaration emit.
 - Every exported function's return type survives into its emitted declaration as
   a named type, not `any` or `/*elided*/`; curried generic exports carry an