diff --git a/CHANGELOG.md b/CHANGELOG.md
index f87c25bfa..d5397979a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -20,6 +20,48 @@ history.
 
 ## Unreleased
 
+- **BREAKING CHANGES:** `fjs/djs/examples/input.f.ts` and
+  `fjs/djs/examples/m.f.ts` migrate to `.f.mjs`. Being `.mjs` they now
+  ship in the tarball, which `.f.ts` did not
+  [#1505](https://github.com/functionalscript/functionalscript/pull/1505)
+- **BREAKING CHANGES:** `fjs/types/nominal/proof.f.ts` migrates to
+  `.f.mjs`. Its two `unique symbol` brands move to `types.ts`, exported
+  as `_SymbolKeyBranded` and `_SymbolIntersectionBranded`
+  [#1505](https://github.com/functionalscript/functionalscript/pull/1505)
+- **BREAKING CHANGES:** `fjs/types/ts/proof.f.ts` migrates to `.f.mjs`.
+  Its `declare const` index-signature block moves to `types.ts`,
+  non-exported, so no public type changes
+  [#1505](https://github.com/functionalscript/functionalscript/pull/1505)
+- **BREAKING CHANGES:** `fjs/emergent_testing/example.f.ts` migrates
+  from authored TypeScript to JSDoc-typed JavaScript (`.f.mjs`) — the
+  four typed consts become JSDoc `@type` annotations
+  [#1505](https://github.com/functionalscript/functionalscript/pull/1505)
+- **BREAKING CHANGES:** `fjs/types/rtti/validate/proof.f.ts` migrates to
+  `.f.mjs` — 23 compile-time round-trips stay function-local as JSDoc
+  `@typedef`s and are not emitted
+  [#1505](https://github.com/functionalscript/functionalscript/pull/1505)
+- **BREAKING CHANGES:** `fjs/types/rtti/parse/proof.f.ts` migrates to
+  `.f.mjs` — compile-time round-trips stay function-local as JSDoc
+  `@typedef`s and are not emitted
+  [#1505](https://github.com/functionalscript/functionalscript/pull/1505)
+- **BREAKING CHANGES:** `fjs/emergent_testing/proof.f.ts` migrates to
+  `.f.mjs`. Six module-local types become `_`-prefixed `@typedef`s, as a
+  JSDoc `@typedef` has no non-exported form
+  [#1505](https://github.com/functionalscript/functionalscript/pull/1505)
+- **BREAKING CHANGES:** `fjs/effects/node/proof.f.ts` migrates to
+  `.f.mjs` — explicit generic instantiations become checked `@type`
+  declarations, as JSDoc has no call-site form
+  [#1505](https://github.com/functionalscript/functionalscript/pull/1505)
+- **BREAKING CHANGES:** `fjs/js/tokenizer/proof.f.ts` migrates to
+  `.f.mjs` — typed consts become JSDoc `@type` annotations
+  [#1505](https://github.com/functionalscript/functionalscript/pull/1505)
+- **BREAKING CHANGES:** `fjs/media/json/parser/proof.f.ts` migrates to
+  `.f.mjs` — the typed const becomes a JSDoc `@type` annotation
+  [#1505](https://github.com/functionalscript/functionalscript/pull/1505)
+- **BREAKING CHANGES:** `todo/proof.f.ts` migrates to `.f.mjs`. The
+  `TemplateType` alias is renamed `_TemplateType`: it was never exported,
+  but a JSDoc `@typedef` has no non-exported form
+  [#1505](https://github.com/functionalscript/functionalscript/pull/1505)
 - **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
diff --git a/fjs/djs/README.md b/fjs/djs/README.md
index 69dcfd923..0d63f3c83 100644
--- a/fjs/djs/README.md
+++ b/fjs/djs/README.md
@@ -19,7 +19,7 @@ holding the same reference must yield the same object, not two equal copies —
 so the AST keeps the constants addressable and refers to them by index
 instead of inlining them. That is also what makes serialization a real
 choice: a value referenced more than once is emitted as a `const` and reused.
-See [examples/input.f.ts](./examples/input.f.ts).
+See [examples/input.f.mjs](./examples/input.f.mjs).
 
 ## Next steps
 
diff --git a/fjs/djs/examples/input.f.ts b/fjs/djs/examples/input.f.mjs
similarity index 67%
rename from fjs/djs/examples/input.f.ts
rename to fjs/djs/examples/input.f.mjs
index e081d9f28..5ec9fdd8b 100644
--- a/fjs/djs/examples/input.f.ts
+++ b/fjs/djs/examples/input.f.mjs
@@ -1,4 +1,4 @@
-import c from "./m.f.ts"
+import c from "./m.f.mjs"
 const a = 1
 const b = 2
 export default [a, a, b, c, c]
\ No newline at end of file
diff --git a/fjs/djs/examples/m.f.ts b/fjs/djs/examples/m.f.mjs
similarity index 100%
rename from fjs/djs/examples/m.f.ts
rename to fjs/djs/examples/m.f.mjs
diff --git a/fjs/djs/todo/66e-parser-container-stack-bookkeeping.md b/fjs/djs/todo/66e-parser-container-stack-bookkeeping.md
index f8b94d183..96e64ac05 100644
--- a/fjs/djs/todo/66e-parser-container-stack-bookkeeping.md
+++ b/fjs/djs/todo/66e-parser-container-stack-bookkeeping.md
@@ -165,7 +165,7 @@ one and can land independently of 157.
 - [ ] Apply the same shape to `fjs/djs/parser/module.f.mjs`, preserving the
       `{ ...state }` spread and the `endArray` non-array fallback inside the
       `build` callback.
-- [ ] Run `npx tsc` and `fjs t`; confirm `fjs/media/json/parser/proof.f.ts` and
+- [ ] Run `npx tsc` and `fjs t`; confirm `fjs/media/json/parser/proof.f.mjs` and
       `fjs/djs/parser/proof.f.mjs` still pass with full line/branch coverage
       (behaviour is unchanged — this is a pure refactor).
 
diff --git a/fjs/effects/node/proof.f.ts b/fjs/effects/node/proof.f.mjs
similarity index 92%
rename from fjs/effects/node/proof.f.ts
rename to fjs/effects/node/proof.f.mjs
index 73e3f2a63..e73c687dd 100644
--- a/fjs/effects/node/proof.f.ts
+++ b/fjs/effects/node/proof.f.mjs
@@ -1,25 +1,33 @@
-import type { Vec } from "../../types/bit_vec/types.ts"
+/**
+ * @import { Vec } from "../../types/bit_vec/types.ts"
+ * @import { IoResult, ReadFile } from "./types.ts"
+ * @import { Dir } from "./virtual/types.ts"
+ * @import { List } from "../list/types.ts"
+ * @import { OperationMap } from "../types.ts"
+ */
+
 import { empty, isVec, uint, vec, vec8 } from "../../types/bit_vec/module.f.mjs"
 import { utf8, utf8ToString } from "../../text/module.f.mjs"
 import { match, pure, step } from "../module.f.mjs"
 import { both, fetch, mkdir, now, readdir, readFile, readUtf8File, rm, sandbox, writeFile, writeUtf8File, rename, readBytes, randomInt, writeFromStream, usesInlineTestContext, versionLessThan } from "./module.f.mjs"
-import type { IoResult, ReadFile } from "./types.ts"
 import { create as memCreate, read as memRead, write as memWrite } from "../memory/module.f.mjs"
 import { empty as listEmpty, nonEmpty as listNonEmpty } from "../list/module.f.mjs"
 import { emptyState, virtual } from "./virtual/module.f.mjs"
-import type { Dir } from "./virtual/types.ts"
 import { assert, assertEq, assertNotNullish } from '../../asserts/module.f.mjs'
 import { ok } from '../../types/result/module.f.mjs'
 
 // Answers the one command the `map` proof below drives. Routing the loop
 // through `match` keeps the `Pure`/`Do` layout out of this module: the map key
 // is the command assertion, and `MatchResult` types the continuation.
-const readHello = match<ReadFile, IoResult<Vec>>({
+/** @type {OperationMap<ReadFile, IoResult<Vec>>} */
+const readHelloMap = {
     readFile: path => {
         assertEq(path, 'hello')
         return ok(vec8(0x15n))
     },
-})
+}
+
+const readHello = match(readHelloMap)
 
 export const proof = {
     externalTestContext: () => {
@@ -74,7 +82,7 @@ export const proof = {
             assert(t === 'ok', result)
             const tmp = state.root.tmp
             assert(!(typeof tmp !== 'object' || Array.isArray(tmp)), state.root)
-            const cache = (tmp as Dir).cache
+            const cache = (/** @type {Dir} */ (tmp)).cache
             assert(!(typeof cache !== 'object' || Array.isArray(cache)), tmp)
         },
         nonRec: () => {
@@ -114,7 +122,7 @@ export const proof = {
         nestedPath: () => {
             const [_, [t, result]] = virtual(emptyState)(readFile('tmp/cache'))
             assert(t === 'error', result)
-            if ((result as { code?: unknown }).code !== 'ENOENT') { throw result }
+            if ((/** @type {{ code?: unknown }} */ (result)).code !== 'ENOENT') { throw result }
         },
         withinLimit: () => {
             // Test with a small file well within the 131,072 byte limit
@@ -265,7 +273,7 @@ export const proof = {
             assert(t === 'ok', result)
             const tmp = state.root.tmp
             assert(!(typeof tmp !== 'object' || Array.isArray(tmp)), state.root)
-            assertEq((tmp as Dir).cache, undefined, tmp)
+            assertEq((/** @type {Dir} */ (tmp)).cache, undefined, tmp)
         },
         noSuchFile: () => {
             const [_, [t, result]] = virtual(emptyState)(rm('hello'))
@@ -305,7 +313,7 @@ export const proof = {
         // (and `duration`) instead of the runner measuring.
         ok: () => {
             const [_, { result, duration }] = virtual(emptyState)(
-                sandbox(() => ({ result: ['ok', 42], duration: 0 }) as never))
+                sandbox(() => /** @type {never} */ ({ result: ['ok', 42], duration: 0 })))
             assert(result[0] === 'ok', result)
             assertEq(result[1], 42)
             assertEq(duration, 0)
@@ -313,7 +321,7 @@ export const proof = {
         error: () => {
             const err = new Error('fail')
             const [_, { result }] = virtual(emptyState)(
-                sandbox(() => ({ result: ['error', err], duration: 0 }) as never))
+                sandbox(() => /** @type {never} */ ({ result: ['error', err], duration: 0 })))
             assert(result[0] === 'error', result)
             assertEq(result[1], err)
         },
@@ -343,7 +351,7 @@ export const proof = {
             assert(t === 'ok', result)
             assertEq(state.root.src, undefined, state.root)
             assert(Array.isArray(state.root.dst), state.root)
-            assertEq(uint((state.root.dst as readonly Vec[])[0]), 0x2An, state.root)
+            assertEq(uint((/** @type {readonly Vec[]} */ (state.root.dst))[0]), 0x2An, state.root)
         },
         nestedRename: () => {
             const [state, [t, result]] = virtual({
@@ -353,7 +361,7 @@ export const proof = {
             assert(t === 'ok', result)
             const tmp = state.root.tmp
             assert(!(typeof tmp !== 'object' || Array.isArray(tmp)), state.root)
-            assertEq((tmp as Dir).src, undefined, tmp)
+            assertEq((/** @type {Dir} */ (tmp)).src, undefined, tmp)
         },
         dirOverFile: () => {
             const [state, [t, result]] = virtual({
@@ -411,10 +419,12 @@ export const proof = {
         createExclusiveFails: () => {
             // The destination already exists, so `createExclusive` fails (EEXIST) and
             // the error propagates without ever touching `writeBytes`.
+            /** @type {List<never, IoResult<Vec>>} */
+            const chunks = listEmpty()
             const [state, [t, result]] = virtual({
                 ...emptyState,
                 root: { hello: [vec8(0x2An)] },
-            })(writeFromStream('hello', listEmpty<never, IoResult<Vec>>()))
+            })(writeFromStream('hello', chunks))
             assert(t === 'error', result)
             const file = state.root.hello
             assert(!(!Array.isArray(file) || uint(file[0]) !== 0x2An), file)
@@ -422,8 +432,10 @@ export const proof = {
         invalidBufferSize: () => {
             // A chunk whose bit length isn't a multiple of 8 trips the
             // byte-alignment guard before `writeBytes` is ever called.
+            /** @type {List<never, IoResult<Vec>>} */
+            const chunks = listNonEmpty(['ok', vec(4n)(0b1010n)], listEmpty())
             const [_, [t, result]] = virtual(emptyState)(
-                writeFromStream('hello', listNonEmpty<never, IoResult<Vec>>(['ok', vec(4n)(0b1010n)], listEmpty()))
+                writeFromStream('hello', chunks)
             )
             assert(t === 'error', result)
             assertEq(result, 'invalid buffer size')
diff --git a/fjs/effects/node/todo/ornotfound-combinator.md b/fjs/effects/node/todo/ornotfound-combinator.md
index 0d971a113..4ea5a625b 100644
--- a/fjs/effects/node/todo/ornotfound-combinator.md
+++ b/fjs/effects/node/todo/ornotfound-combinator.md
@@ -49,7 +49,7 @@ list: () => access(storePrefix).step(orNotFound<readonly Vec[]>([])(() =>
 - [ ] Add `orNotFound` beside `isNotFound` in `fjs/effects/node/module.f.mjs`
       (once a second consumer exists).
 - [ ] Rewrite `list` in `fjs/cas/module.f.ts` on top of it.
-- [ ] Cover all three branches (`ok`, `ENOENT`, non-`ENOENT` throw) in `fjs/effects/node/proof.f.ts`.
+- [ ] Cover all three branches (`ok`, `ENOENT`, non-`ENOENT` throw) in `fjs/effects/node/proof.f.mjs`.
 
 ### Related
 
diff --git a/fjs/emergent_testing/example.f.ts b/fjs/emergent_testing/example.f.mjs
similarity index 62%
rename from fjs/emergent_testing/example.f.ts
rename to fjs/emergent_testing/example.f.mjs
index 0d680af0a..cdd9b9664 100644
--- a/fjs/emergent_testing/example.f.ts
+++ b/fjs/emergent_testing/example.f.mjs
@@ -1,12 +1,16 @@
-export const add = (a: number, b: number): number => a + b
+/** @type {(a: number, b: number) => number} */
+export const add = (a, b) => a + b
 
-export const mul = (a: number, b: number): number => a * b
+/** @type {(a: number, b: number) => number} */
+export const mul = (a, b) => a * b
 
-export const sqr = (a: number) => mul(a, a)
+/** @type {(a: number) => number} */
+export const sqr = a => mul(a, a)
 
 export const todo = () => { throw "not implemented" }
 
-const checkMul = (a: number, b: number, r: number) => {
+/** @type {(a: number, b: number, r: number) => void} */
+const checkMul = (a, b, r) => {
     if (mul(a, b) !== r) { throw `mul(${a}, ${b}) !== ${r}` } 
 }
 
diff --git a/fjs/emergent_testing/proof.f.ts b/fjs/emergent_testing/proof.f.mjs
similarity index 81%
rename from fjs/emergent_testing/proof.f.ts
rename to fjs/emergent_testing/proof.f.mjs
index e5e388d2b..a6ba5979a 100644
--- a/fjs/emergent_testing/proof.f.ts
+++ b/fjs/emergent_testing/proof.f.mjs
@@ -1,22 +1,25 @@
-import type { Effect } from '../effects/types.ts'
+/**
+ * @import { Effect } from '../effects/types.ts'
+ * @import { NodeProgramOptions, Sandbox, Write } from '../effects/node/types.ts'
+ * @import { JsModule } from '../effects/node/virtual/types.ts'
+ * @import { Reporter } from './types.ts'
+ * @import { All, Await, Test, TestContext } from '../effects/node/types.ts'
+ * @import { Ts } from '../types/rtti/ts/types.ts'
+ */
+
 import { log } from '../effects/node/module.f.mjs'
-import type { NodeProgramOptions, Sandbox, Write } from '../effects/node/types.ts'
 import { defaultNodeProgramOptions, emptyState, virtual } from '../effects/node/virtual/module.f.mjs'
-import type { JsModule } from '../effects/node/virtual/types.ts'
 import { assert, assertEq } from '../asserts/module.f.mjs'
 import {
     testAll, defaultReporter, fmtPath, fmtTerm, fmtImport, ghEscape, isInteger, isIdentifier,
     registerModule, parseTestSet,
     defaultTest,
 } from './module.f.mjs'
-import type { Reporter } from './types.ts'
 import { run as mockRun } from '../effects/mock/module.f.mjs'
-import type { All, Await, Test, TestContext } from '../effects/node/types.ts'
 import { shouldLoad } from '../dev/module.f.mjs'
 import { parse as parseJson } from '../media/json/module.f.mjs'
 import { array, number as rttiNumber, or, string as rttiString } from '../types/rtti/module.f.mjs'
 import { parse as rttiParse } from '../types/rtti/parse/module.f.mjs'
-import type { Ts } from '../types/rtti/ts/types.ts'
 import { unwrap } from '../types/result/module.f.mjs'
 
 /**
@@ -30,38 +33,46 @@ import { unwrap } from '../types/result/module.f.mjs'
  * JSON representation to round-trip through anyway.
  */
 const event = or(
-    ['result', rttiString, array(or(rttiString, null))] as const,
-    ['summary', rttiNumber, rttiNumber, rttiNumber] as const,
+    /** @type {const} */ (['result', rttiString, array(or(rttiString, null))]),
+    /** @type {const} */ (['summary', rttiNumber, rttiNumber, rttiNumber]),
 )
 
-type Event = Ts<typeof event>
+/** @typedef {Ts<typeof event>} _Event */
 
 const parseEvent = rttiParse(event)
 
-type TestReporter = Reporter<Sandbox | Write>
+/** @typedef {Reporter<Sandbox | Write>} _TestReporter */
 
-const writeEvent = (e: Event) => log(JSON.stringify(e))
+/** @type {(e: _Event) => ReturnType<typeof log>} */
+const writeEvent = e => log(JSON.stringify(e))
 
-const parseEvents = (stdout: string): readonly Event[] =>
+/** @type {(stdout: string) => readonly _Event[]} */
+const parseEvents = stdout =>
     stdout === '' ? [] : stdout.trimEnd().split('\n')
         .map(line => unwrap(parseEvent(unwrap(parseJson(line)))))
 
-const makeReporter = (): TestReporter => ({
+/** @type {() => _TestReporter} */
+const makeReporter = () => ({
     result: (file, path, _r, _throws) => writeEvent(['result', file, [...path]]),
     summary: (pass, fail, time) => writeEvent(['summary', pass, fail, time]),
     test: defaultTest,
 })
 
-const options = (initCwd: string, github = false): NodeProgramOptions => ({
+/** @type {(initCwd: string, github?: boolean) => NodeProgramOptions} */
+const options = (initCwd, github = false) => ({
     ...defaultNodeProgramOptions,
     env: { INIT_CWD: initCwd, ...(github ? { GITHUB_ACTIONS: 'true' } : {}) },
 })
 
-const ok0 = (): unknown => ({ result: ['ok', undefined] as const, duration: 0 })
-const fail0 = (): unknown => ({ result: ['error', 'oops'] as const, duration: 0 })
-const ok1 = (): unknown => ({ result: ['ok', undefined] as const, duration: 1 })
+/** @type {() => unknown} */
+const ok0 = () => ({ result: /** @type {const} */ (['ok', undefined]), duration: 0 })
+/** @type {() => unknown} */
+const fail0 = () => ({ result: /** @type {const} */ (['error', 'oops']), duration: 0 })
+/** @type {() => unknown} */
+const ok1 = () => ({ result: /** @type {const} */ (['ok', undefined]), duration: 1 })
 
-const run = (dir: Record<string, JsModule>, initCwd = '.'): readonly [readonly Event[], number] => {
+/** @type {(dir: Record<string, JsModule>, initCwd?: string) => readonly [readonly _Event[], number]} */
+const run = (dir, initCwd = '.') => {
     const reporter = makeReporter()
     const state = { ...emptyState, root: dir }
     const [finalState, exitCode] = virtual(state)(testAll(reporter)(options(initCwd)))
@@ -70,7 +81,8 @@ const run = (dir: Record<string, JsModule>, initCwd = '.'): readonly [readonly E
 
 // Runs the real `defaultReporter` and returns its captured stdout/stderr so the
 // terminal and GitHub output formats can be asserted directly.
-const runMain = (dir: Record<string, JsModule>, github = false): readonly [string, string, number] => {
+/** @type {(dir: Record<string, JsModule>, github?: boolean) => readonly [string, string, number]} */
+const runMain = (dir, github = false) => {
     const state = { ...emptyState, root: dir }
     const opts = options('.', github)
     const [finalState, exitCode] = virtual(state)(testAll(defaultReporter(opts))(opts))
@@ -149,14 +161,15 @@ export const mixedPassFail = () => {
 
 // return-value sub-tree: passing test's return value is walked
 export const returnValueSubTree = () => {
-    const inner: () => unknown = () => ({ result: ['ok', undefined] as const, duration: 0 })
+    /** @type {() => unknown} */
+    const inner = () => ({ result: /** @type {const} */ (['ok', undefined]), duration: 0 })
     const [events, exit] = run({
         'r.proof.f.ts': () => ({
             proof: {
-                outer: (): unknown => ({
-                    result: ['ok', { inner }] as const,
+                outer: /** @type {() => unknown} */ (() => ({
+                    result: /** @type {const} */ (['ok', { inner }]),
                     duration: 0,
-                }),
+                })),
             }
         }),
     })
@@ -286,55 +299,61 @@ export const githubReporterOutput = () => {
     )
 }
 
-type RegisterMockState = readonly string[]
+/** @typedef {readonly string[]} _RegisterMockState */
 
-type RegisterMockOps = Test | All | Await
+/** @typedef {Test | All | Await} _RegisterMockOps */
 
-type RegisterRunner =
-    (s: RegisterMockState) => <T>(e: Effect<RegisterMockOps, T>) => readonly [RegisterMockState, T]
+/**
+ * @typedef {(s: _RegisterMockState) => <T>(e: Effect<_RegisterMockOps, T>) => readonly [_RegisterMockState, T]} _RegisterRunner
+ */
 
-/** The `test` op body for a `registerModule` mock; `runner` is threaded in explicitly (rather than closed over) so it can recurse into sub-effects returned by `fn`. */
-type RegisterTestOp = (
-    runner: RegisterRunner,
-    ctx: TestContext,
-    name: string,
-    expectFailure: boolean,
-    fn: (t: TestContext) => Effect<RegisterMockOps, void>,
-) => (s: RegisterMockState) => readonly [RegisterMockState, void]
+/**
+ * The `test` op body for a `registerModule` mock; `runner` is threaded in explicitly (rather than closed over) so it can recurse into sub-effects returned by `fn`.
+ * @typedef {(
+ *     runner: _RegisterRunner,
+ *     ctx: TestContext,
+ *     name: string,
+ *     expectFailure: boolean,
+ *     fn: (t: TestContext) => Effect<_RegisterMockOps, void>,
+ * ) => (s: _RegisterMockState) => readonly [_RegisterMockState, void]} _RegisterTestOp
+ */
 
-const registerNoopCtx: TestContext = { test: (_n, _o, _f) => Promise.resolve() }
+/** @type {TestContext} */
+const registerNoopCtx = { test: (_n, _o, _f) => Promise.resolve() }
 
 /**
  * Builds a synchronous mock runner for `registerModule`'s `Test`/`All`/`Await`
  * effect operations. Only the `test` op varies between call sites (whether it
  * invokes the registered callback), so `all`/`await` are shared here.
  */
-const makeRegisterRunner = (testOp: RegisterTestOp): RegisterRunner => {
-    let runner!: RegisterRunner
-    runner = mockRun<RegisterMockOps, RegisterMockState>({
+/** @type {(testOp: _RegisterTestOp) => _RegisterRunner} */
+const makeRegisterRunner = testOp => {
+    /** @type {_RegisterRunner} */
+    let runner
+    runner = mockRun(/** @type {Parameters<typeof mockRun<_RegisterMockOps, _RegisterMockState>>[0]} */ ({
         test: (ctx, name, xf, fn) => testOp(runner, ctx, name, xf, fn),
-        all: (...effects: readonly Effect<RegisterMockOps, unknown>[]) => (s: RegisterMockState) =>
+        all: (...effects) => s =>
             effects.reduce(
-                ([st, rs]: readonly [RegisterMockState, readonly unknown[]], e) => {
+                ([st, rs], e) => {
                     const [ns, r] = runner(st)(e)
-                    return [ns, [...rs, r]] as const
+                    return /** @type {readonly [_RegisterMockState, readonly unknown[]]} */ ([ns, [...rs, r]])
                 },
-                [s, []] as readonly [RegisterMockState, readonly unknown[]],
+                /** @type {readonly [_RegisterMockState, readonly unknown[]]} */ ([s, []]),
             ),
-        await: (p: unknown) => (s: RegisterMockState) => [s, [p]] as const,
-    } as Parameters<typeof mockRun<RegisterMockOps, RegisterMockState>>[0])
+        await: p => s => /** @type {const} */ ([s, [p]]),
+    }))
     return runner
 }
 
 // registerModule appends ' ...' for inline runners (Bun).
 // This mock never invokes the registered callback; it only records names.
 export const registerSuffixes = () => {
-    const runner = makeRegisterRunner((_runner, _ctx, name, _xf, _fn) => (s: RegisterMockState) => [[...s, name], undefined])
+    const runner = makeRegisterRunner((_runner, _ctx, name, _xf, _fn) => s => [[...s, name], undefined])
 
-    const proof = {
+    const proof = /** @type {const} */ ({
         ok: () => {},
         throw: { a: () => { throw 'expected' } },
-    } as const
+    })
 
     // Node (star = ''): no suffixes
     const [nodeNames] = runner([])(registerModule(registerNoopCtx, './a.f.ts', proof, ''))
@@ -359,14 +378,14 @@ export const registerThrowsWithoutThrowing = () => {
     // Unlike registerSuffixes' mock, this one actually invokes the registered
     // callback so registerOne's inner `.step` body runs, and asserts the
     // callback is registered with `expectFailure: true`.
-    const runner = makeRegisterRunner((runner, ctx, name, xf, fn) => (s: RegisterMockState) => {
+    const runner = makeRegisterRunner((runner, ctx, name, xf, fn) => s => {
         assert(xf)
         const [ns] = runner(s)(fn(ctx))
         return [[...ns, name], undefined]
     })
 
     // Returns a sub-tree that would register more tests if it were walked.
-    const proof = { throw: { a: () => ({ sub: () => {} }) } } as const
+    const proof = /** @type {const} */ ({ throw: { a: () => ({ sub: () => {} }) } })
 
     const [names] = runner([])(registerModule(registerNoopCtx, './a.f.ts', proof, ''))
     // Only the throw-test itself is registered; `sub` is never reached.
@@ -377,7 +396,7 @@ export const registerThrowsWithoutThrowing = () => {
 // registerModule with an empty proof object registers zero tests and
 // returns without invoking the mock's `test` op at all.
 export const registerEmptyProof = () => {
-    const runner = makeRegisterRunner((_runner, _ctx, name, _xf, _fn) => (s: RegisterMockState) => [[...s, name], undefined])
+    const runner = makeRegisterRunner((_runner, _ctx, name, _xf, _fn) => s => [[...s, name], undefined])
     const [names] = runner([])(registerModule(registerNoopCtx, './a.f.ts', {}, ''))
     assertEq(names.length, 0)
 }
@@ -454,12 +473,12 @@ export const helpers = {
         nullReturnsEmpty: () => {
             const result = parseTestSet(false, null)
             assertEq(Array.isArray(result), true)
-            assertEq((result as unknown[]).length, 0)
+            assertEq((/** @type {unknown[]} */ (result)).length, 0)
         },
         functionWithParamsReturnsEmpty: () => {
-            const result = parseTestSet(false, (_x: number) => _x)
+            const result = parseTestSet(false, (/** @type {number} */ _x) => _x)
             assertEq(Array.isArray(result), true)
-            assertEq((result as unknown[]).length, 0)
+            assertEq((/** @type {unknown[]} */ (result)).length, 0)
         },
     },
 }
diff --git a/fjs/emergent_testing/todo/skip-property.md b/fjs/emergent_testing/todo/skip-property.md
index 122175037..7578993ce 100644
--- a/fjs/emergent_testing/todo/skip-property.md
+++ b/fjs/emergent_testing/todo/skip-property.md
@@ -157,7 +157,7 @@ Playwright execution obtains skip results from the shared browser application.
       browser-side runner, independently of the Playwright Test adapter.
 - [ ] Print `# SKIP` per leaf and `pass / fail / todo / skip` in
       `defaultReporter` (`fjs t`).
-- [ ] Add proofs in `fjs/emergent_testing/proof.f.ts`: skipped leaf not
+- [ ] Add proofs in `fjs/emergent_testing/proof.f.mjs`: skipped leaf not
       executed, skipped subtree collected as individual paths, skipped
       generator reported as one leaf, `skip` dominating `throw`/`todo`,
       counters unaffected by skips.
diff --git a/fjs/emergent_testing/todo/todo-property.md b/fjs/emergent_testing/todo/todo-property.md
index 2af8b41a6..fa2b9f4d1 100644
--- a/fjs/emergent_testing/todo/todo-property.md
+++ b/fjs/emergent_testing/todo/todo-property.md
@@ -197,7 +197,7 @@ docs, mirroring the existing `throws` plumbing:
 
 ### Migration
 
-This rule reinterprets existing `fjs/emergent_testing/example.f.ts`:
+This rule reinterprets existing `fjs/emergent_testing/example.f.mjs`:
 
 ```ts
 export const todo = () => { throw "not implemented" }
@@ -231,8 +231,8 @@ out from under `throw`) as part of landing this change.
 - [ ] Add a `todo` counter to `TestState`/`Reporter.summary` and print
       `pass / fail / todo` in `defaultReporter` (`fjs t` only; `register`
       unchanged).
-- [ ] Migrate `fjs/emergent_testing/example.f.ts` off `throw: { todo }`.
-- [ ] Add proofs in `fjs/emergent_testing/proof.f.ts` for: `todo` green on throw,
+- [ ] Migrate `fjs/emergent_testing/example.f.mjs` off `throw: { todo }`.
+- [ ] Add proofs in `fjs/emergent_testing/proof.f.mjs` for: `todo` green on throw,
       `todo` red when it returns, `throw.todo` green on return / red on throw, the
       never-walk-subtests rule, and the static guard rejecting a non-function
       `todo`.
diff --git a/fjs/js/identifier/todo/lift-js-lexical-predicates-out-of-emergent-testing.md b/fjs/js/identifier/todo/lift-js-lexical-predicates-out-of-emergent-testing.md
index 6c6f5c520..92ad2c17e 100644
--- a/fjs/js/identifier/todo/lift-js-lexical-predicates-out-of-emergent-testing.md
+++ b/fjs/js/identifier/todo/lift-js-lexical-predicates-out-of-emergent-testing.md
@@ -28,9 +28,9 @@ A future consumer: the DJS serializer currently quotes every object key; with `i
 ### Tasks
 
 - [ ] Create `fjs/js/identifier/module.f.ts` with the two exports.
-- [ ] Add co-located `proof.f.ts` with 100% coverage (reuse cases from `fjs/emergent_testing/proof.f.ts:313-328`).
+- [ ] Add co-located `proof.f.ts` with 100% coverage (reuse cases from `fjs/emergent_testing/proof.f.mjs:406-421`).
 - [ ] Register in `deno.json` `exports` map.
-- [ ] Remove the four definitions from `fjs/emergent_testing/module.f.mjs`; repoint `emergent_testing/proof.f.ts` at the new module.
+- [ ] Remove the four definitions from `fjs/emergent_testing/module.f.mjs`; repoint `emergent_testing/proof.f.mjs` at the new module.
 - [ ] Run `npx tsc` and `fjs t`.
 
 ### Related
diff --git a/fjs/js/tokenizer/proof.f.ts b/fjs/js/tokenizer/proof.f.mjs
similarity index 98%
rename from fjs/js/tokenizer/proof.f.ts
rename to fjs/js/tokenizer/proof.f.mjs
index 7bd89ed16..b6c823e88 100644
--- a/fjs/js/tokenizer/proof.f.ts
+++ b/fjs/js/tokenizer/proof.f.mjs
@@ -1,23 +1,23 @@
+/**
+ * @import { JsToken, JsTokenWithMetadata } from './types.ts'
+ */
+
 import { tokenize } from './module.f.mjs'
-import type { JsToken, JsTokenWithMetadata } from './types.ts'
 import { map, 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 JsToken[]
-    = s => toArray(map(withoutMetada)(tokenize(stringToList(s))('')))
+/** @type {(s: string) => readonly JsToken[]} */
+const tokenizeString = s => toArray(map(withoutMetada)(tokenize(stringToList(s))('')))
 
-const tokenizeStringWithMetadata
-    : (s: string) => readonly JsTokenWithMetadata[]
-    = s => toArray(tokenize(stringToList(s))(''))
+/** @type {(s: string) => readonly JsTokenWithMetadata[]} */
+const tokenizeStringWithMetadata = s => toArray(tokenize(stringToList(s))(''))
 
 const stringify = stringifyAsTree(sort)
 
-const withoutMetada
-    : (tokenWithMetada: JsTokenWithMetadata) => JsToken
-    = tokenWithMetada => tokenWithMetada.token
+/** @type {(tokenWithMetada: JsTokenWithMetadata) => JsToken} */
+const withoutMetada = tokenWithMetada => tokenWithMetada.token
 
 export const proof = {
     djs: [
diff --git a/fjs/media/json/parser/proof.f.ts b/fjs/media/json/parser/proof.f.mjs
similarity index 97%
rename from fjs/media/json/parser/proof.f.ts
rename to fjs/media/json/parser/proof.f.mjs
index 4b54839ac..396c0d664 100644
--- a/fjs/media/json/parser/proof.f.ts
+++ b/fjs/media/json/parser/proof.f.mjs
@@ -1,15 +1,17 @@
+/**
+ * @import { JsonToken } from '../tokenizer/types.ts'
+ */
+
 import { parse } from './module.f.mjs'
 import { tokenize } from '../tokenizer/module.f.mjs'
-import type { JsonToken } from '../tokenizer/types.ts'
 import { toArray } from '../../../types/list/module.f.mjs'
 import { stringify as jsonStringify } from '../module.f.mjs'
 import { sort } from '../../../types/object/module.f.mjs'
 import { stringToList } from '../../../text/utf16/module.f.mjs'
 import { assertEq } from '../../../asserts/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 = jsonStringify(sort)
 
@@ -278,7 +280,7 @@ export const proof = {
     // unforced thunk per closed container. The chain was forced only at the end,
     // costing a call-stack frame per container and overflowing at roughly 5000 of
     // them — nested or flat siblings alike — while primitives were unbounded,
-    // since they never push or pop. `popStack` in `module.f.ts` forces the pop
+    // since they never push or pop. `popStack` in `module.f.mjs` forces the pop
     // instead, which is why these sizes are safe now.
     siblingContainers: [
         () => {
diff --git a/fjs/media/json/todo/remove-native-json.md b/fjs/media/json/todo/remove-native-json.md
index eca781c57..69e2f072e 100644
--- a/fjs/media/json/todo/remove-native-json.md
+++ b/fjs/media/json/todo/remove-native-json.md
@@ -42,7 +42,7 @@ Three reasons to finish the job:
 | Expected-output comparison | 73 | `fjs/bnf/ll1/proof.f.ts` (27), `fjs/bnf/descent/proof.f.ts` (22), `fjs/media/json/serializer/proof.f.mjs` (10), `fjs/djs/tokenizer/proof.f.mjs:886-921` (8), `fjs/bnf/data/proof.f.ts` (4), `fjs/media/revision/proof.f.mjs:177`, `fjs/cas/evo/proof.f.mjs:68` | `stringify(identity)` |
 | Assertion messages | 33 | `fjs/djs/tokenizer/proof.f.mjs` (31), `fjs/types/rtti/ts/proof.f.mjs:8,12` (2) | pass the value, or `fjs/djs`'s `stringify` |
 | Source-text quoting | 5 | `fjs/emergent_testing/module.f.mjs:282,303,318`, `fjs/types/ts/module.f.mjs:36,48` | `stringSerialize` — already designed in `66c-emit-literals-via-owner-modules.md` |
-| JSON line framing | 2 | `fjs/emergent_testing/proof.f.ts:42`, `fjs/mcp/proof.f.mjs:128` | `stringify(identity)` |
+| JSON line framing | 2 | `fjs/emergent_testing/proof.f.mjs:47`, `fjs/mcp/proof.f.mjs:128` | `stringify(identity)` |
 | Pretty-printed file output | 1 | `fjs/ci/module.f.mjs:83` | needs indentation support, which `serialize` does not have |
 
 Three semantic differences to respect while migrating, none of them blocking:
@@ -140,7 +140,7 @@ Consider a guard so it does not come back — the cheapest is a proof in
 
 - [`fjs/media/json/serializer/module.f.mjs`](../serializer/module.f.mjs) — the
   leaf `JSON.stringify` phases 1 and 2 replace; only `numberSerialize` is left.
-- [`fjs/text/utf16/module.f.ts`](../../../text/utf16/module.f.ts) — where the
+- [`fjs/text/utf16/module.f.mjs`](../../../text/utf16/module.f.mjs) — where the
   escaping reads code points, and where phase 1 added `codePointToString`.
 - [`fjs/fsc/todo/66c-emit-literals-via-owner-modules.md`](../../../fsc/todo/66c-emit-literals-via-owner-modules.md)
   — already owns the source-text-quoting sites (`fjs/types/ts`,
diff --git a/fjs/media/json/todo/stringify-sorted-canonical.md b/fjs/media/json/todo/stringify-sorted-canonical.md
index a0ac2689c..6a417e7ee 100644
--- a/fjs/media/json/todo/stringify-sorted-canonical.md
+++ b/fjs/media/json/todo/stringify-sorted-canonical.md
@@ -24,7 +24,7 @@ Proof files (each binds its own alias: `jsonStr`, `str`, `stringify`,
   `fjs/types/sorted_set/proof.f.mjs:12`, `fjs/types/list/proof.f.mjs:11`
 - `fjs/text/ascii/proof.f.mjs:6`, `fjs/text/utf8/proof.f.mjs:8`,
   `fjs/text/utf16/proof.f.mjs:18`
-- `fjs/media/json/parser/proof.f.ts:13`, `fjs/protocol/mcp/stdio/proof.f.mjs:20`
+- `fjs/media/json/parser/proof.f.mjs:16`, `fjs/protocol/mcp/stdio/proof.f.mjs:20`
 - `fjs/bnf/data/proof.f.ts` (10 inline calls), `fjs/djs/parser/proof.f.mjs:309`,
   `fjs/djs/serializer/proof.f.mjs:47`
 
diff --git a/fjs/types/nominal/proof.f.mjs b/fjs/types/nominal/proof.f.mjs
new file mode 100644
index 000000000..3a303a2a5
--- /dev/null
+++ b/fjs/types/nominal/proof.f.mjs
@@ -0,0 +1,79 @@
+/**
+ * @import { Nominal, _SymbolKeyBranded, _SymbolIntersectionBranded } from "./types.ts"
+ */
+
+import { asBase, asNominal } from "./module.f.mjs"
+import { assert } from '../../asserts/module.f.mjs'
+
+export const proof = {
+    pre: () => {
+        /** @typedef {Nominal<'utf8', 'v0', bigint>} _Str */
+        /** @type {_Str} */
+        const strA = asNominal(0b1_11000010_10100010_11000010_10100011n) // "¢£"
+        /** @type {_Str} */
+        const strB = asNominal(0b1_11000010_10100010_11000010_10100100n) // "¢¤"
+        assert(strA !== strB, [strA, strB])
+        // // TypeScript compilation error.
+        // const x1 = strA > strB
+
+        //
+        {
+            /**
+             * @template {object} [T=object]
+             * @typedef {T & { __noCompare__: never }} _ForbiddenCompare
+             */
+            /** @typedef {_ForbiddenCompare<{ value: number }>} _IntersectionSafeId */
+            const a = /** @type {_IntersectionSafeId} */ ({ value: 1 })
+            const b = /** @type {_IntersectionSafeId} */ ({ value: 2 })
+
+            // No Compile-time error
+            if (a < b) { }
+        }
+
+        {
+            /** @typedef {{ _brand: 'NoCompare' }} _StringKeyBranded */
+            /** @type {_StringKeyBranded} */
+            const x = { _brand: 'NoCompare' }
+            // No Error
+            if (x < x) { }
+        }
+        {
+            const a = /** @type {_SymbolKeyBranded} */ ({})
+            const b = /** @type {_SymbolKeyBranded} */ ({})
+
+            // No Error
+            a < b
+        }
+        {
+
+            const a = /** @type {_SymbolIntersectionBranded} */ (/** @type {any} */ (undefined))
+            const b = /** @type {_SymbolIntersectionBranded} */ (/** @type {any} */ (undefined))
+
+            // a < b; // TS2469: Operator '<' cannot be applied to type 'symbol'.
+        }
+    },
+    nominal: () => {
+        /** @typedef {Nominal<'UserId', '1', number>} _UserId */
+        /** @typedef {Nominal<'UserId', '2', number>} _UserId2 */
+        /** @type {_UserId} */
+        const userIdA = asNominal(123)
+        /** @type {_UserId} */
+        const userIdB = asNominal(456)
+        assert(userIdA !== userIdB, [userIdA, userIdB])
+        /** @type {(_: _UserId) => number} */
+        const to = asBase
+        /** @type {(_: _UserId2) => number} */
+        const to2 = asBase
+        /** @type {_UserId2} */
+        const userId2A = asNominal(123)
+        /** @type {_UserId2} */
+        const userId2B = asNominal(456)
+        assert(userId2A !== userId2B, [userId2A, userId2B])
+        // assert(userIdA !== userId2A, [userIdA, userId2A]) // compilation error
+        /** @type {number} */
+        const n1 = to(userIdA)
+        /** @type {number} */
+        const n2 = to2(userId2A)
+        // const x = to(userId2A) // compilation error
+    }
+}
diff --git a/fjs/types/nominal/proof.f.ts b/fjs/types/nominal/proof.f.ts
deleted file mode 100644
index ed35f2982..000000000
--- a/fjs/types/nominal/proof.f.ts
+++ /dev/null
@@ -1,73 +0,0 @@
-import type { Nominal } from "./types.ts"
-import { asBase, asNominal } from "./module.f.mjs"
-import { assert } from '../../asserts/module.f.mjs'
-
-declare const noCompareBrand: unique symbol
-
-declare const brand: unique symbol
-
-export const proof = {
-    pre: () => {
-        type Str = Nominal<'utf8', 'v0', bigint>
-        const strA: Str = asNominal(0b1_11000010_10100010_11000010_10100011n) // "¢£"
-        const strB: Str = asNominal(0b1_11000010_10100010_11000010_10100100n) // "¢¤"
-        assert(strA !== strB, [strA, strB])
-        // // TypeScript compilation error.
-        // const x1 = strA > strB
-
-        //
-        {
-            type ForbiddenCompare<T extends object = object> = T & { __noCompare__: never }
-
-            type SafeId = ForbiddenCompare<{ value: number }>
-
-            const a: SafeId = { value: 1 } as SafeId
-            const b: SafeId = { value: 2 } as SafeId
-
-            // No Compile-time error
-            if (a < b) { }
-        }
-
-        {
-            interface NoCompare { _brand: 'NoCompare' }
-
-            const x: NoCompare = { _brand: 'NoCompare' }
-            // No Error
-            if (x < x) { }
-        }
-        {
-            type NoCompare = { [noCompareBrand]: void }
-
-            const a = {} as NoCompare
-            const b = {} as NoCompare
-
-            // No Error
-            a < b
-        }
-        {
-
-            type SafeId = symbol & { [brand]: 'SafeId' }
-
-            const a = undefined as any as SafeId
-            const b = undefined as any as SafeId
-
-            // a < b; // TS2469: Operator '<' cannot be applied to type 'symbol'.
-        }
-    },
-    nominal: () => {
-        type UserId = Nominal<'UserId', '1', number>
-        type UserId2 = Nominal<'UserId', '2', number>
-        const userIdA: UserId = asNominal(123)
-        const userIdB: UserId = asNominal(456)
-        assert(userIdA !== userIdB, [userIdA, userIdB])
-        const to: (_: UserId) => number = asBase
-        const to2: (_: UserId2) => number = asBase
-        const userId2A: UserId2 = asNominal(123)
-        const userId2B: UserId2 = asNominal(456)
-        assert(userId2A !== userId2B, [userId2A, userId2B])
-        // assert(userIdA !== userId2A, [userIdA, userId2A]) // compilation error
-        const n1: number = to(userIdA)
-        const n2: number = to2(userId2A)
-        // const x = to(userId2A) // compilation error
-    }
-}
diff --git a/fjs/types/nominal/types.ts b/fjs/types/nominal/types.ts
index 8e335e462..53bd6813d 100644
--- a/fjs/types/nominal/types.ts
+++ b/fjs/types/nominal/types.ts
@@ -12,3 +12,18 @@
  */
 export type Nominal<N extends string, R extends string, B> =
     symbol & { [k in N]: readonly [R, B] }
+
+// Brand carriers for the comparison experiments in `proof.f.mjs`. They live
+// here because `declare const` / `unique symbol` have no JavaScript form; the
+// proof imports the two types below and keeps the expressions that demonstrate
+// what TypeScript does or does not reject. `_`-prefixed: private by contract.
+
+declare const noCompareBrand: unique symbol
+
+declare const brand: unique symbol
+
+/** A unique-symbol-keyed brand. TypeScript still permits `<` between two of these. */
+export type _SymbolKeyBranded = { [noCompareBrand]: void }
+
+/** A `symbol` intersection brand. `<` on this is TS2469, so the proof only comments it. */
+export type _SymbolIntersectionBranded = symbol & { [brand]: 'SafeId' }
diff --git a/fjs/types/object/todo/structurally-same.md b/fjs/types/object/todo/structurally-same.md
index b7915d2ea..93af90e6e 100644
--- a/fjs/types/object/todo/structurally-same.md
+++ b/fjs/types/object/todo/structurally-same.md
@@ -5,7 +5,7 @@
 
 ## Problem
 
-`fjs/types/rtti/parse/proof.f.ts` contains a private `assertDeepEqual` helper for
+`fjs/types/rtti/parse/proof.f.mjs` contains a private `assertDeepEqual` helper for
 checking parsed FunctionalScript data. It recursively compares arrays and plain
 records, but it is ad hoc and cannot be reused by other proofs:
 
@@ -164,7 +164,7 @@ These cases can be added later when a concrete consumer requires them.
 - [ ] Verify that the change does not introduce the
       `asserts -> object -> nullable -> asserts` import cycle.
 - [ ] Replace the private `assertDeepEqual` in
-      `fjs/types/rtti/parse/proof.f.ts` with `assertStructurallySame`.
+      `fjs/types/rtti/parse/proof.f.mjs` with `assertStructurallySame`.
 - [ ] Update `fjs/types/rtti/todo/proof-shared-asserts.md` when removing
       `assertDeepEqual`: remove or mark that subtask complete while preserving
       its remaining result-helper and shared-suite work.
@@ -196,7 +196,7 @@ These cases can be added later when a concrete consumer requires them.
 - [`fjs/types/nullable/module.f.mjs`](../../nullable/module.f.mjs) — imports the
   assertion module, which makes importing the public object module from assertions
   cyclic.
-- [`fjs/types/rtti/parse/proof.f.ts`](../../rtti/parse/proof.f.ts) — contains the
+- [`fjs/types/rtti/parse/proof.f.mjs`](../../rtti/parse/proof.f.mjs) — contains the
   private `assertDeepEqual` that is the first direct consumer.
 - [`fjs/cas/evo/proof.f.mjs`](../../../cas/evo/proof.f.mjs) — compares independently
   constructed cache values through `JSON.stringify`.
diff --git a/fjs/types/rtti/parse/proof.f.ts b/fjs/types/rtti/parse/proof.f.mjs
similarity index 63%
rename from fjs/types/rtti/parse/proof.f.ts
rename to fjs/types/rtti/parse/proof.f.mjs
index 2b18ab987..8129bb148 100644
--- a/fjs/types/rtti/parse/proof.f.ts
+++ b/fjs/types/rtti/parse/proof.f.mjs
@@ -1,31 +1,44 @@
+/**
+ * @import { ValidationError } from '../common/types.ts'
+ * @import { Equal } from '../../ts/types.ts'
+ * @import { Ts } from '../ts/types.ts'
+ * @import { Unknown as DjsUnknown } from '../../../djs/types.ts'
+ * @import { Assert } from '../../../asserts/types.ts'
+ */
+
 import { parse } from './module.f.mjs'
-import type { ValidationError } from '../common/types.ts'
 import { boolean, number, string, bigint, unknown, array, record, or, option } from '../module.f.mjs'
-import type { Equal } from '../../ts/types.ts'
-import type { Ts } from '../ts/types.ts'
-import type { Unknown as DjsUnknown } from '../../../djs/types.ts'
-import type { Assert } from '../../../asserts/types.ts'
 import { assert, assertEq } from '../../../asserts/module.f.mjs'
 
-const assertOk = ([k]: readonly [string, unknown]) => { assertEq(k, 'ok', 'expected ok') }
-const assertError = ([k]: readonly [string, unknown]) => { assertEq(k, 'error', 'expected error') }
+/** @type {(r: readonly [string, unknown]) => void} */
+const assertOk = ([k]) => { assertEq(k, 'ok', 'expected ok') }
+
+/** @type {(r: readonly [string, unknown]) => void} */
+const assertError = ([k]) => { assertEq(k, 'error', 'expected error') }
 
-const unwrap = <T>(r: readonly [string, unknown]): T => {
+/**
+ * @template T
+ * @param {readonly [string, unknown]} r
+ * @returns {T}
+ */
+const unwrap = r => {
     assert(r[0] === 'ok', 'expected ok')
-    return r[1] as T
+    return /** @type {T} */ (r[1])
 }
 
-const assertErrorPath = (expected: readonly string[]) =>
-    (r: readonly [string, unknown]) => {
+/** @type {(expected: readonly string[]) => (r: readonly [string, unknown]) => void} */
+const assertErrorPath = expected =>
+    r => {
         assert(r[0] === 'error', 'expected error')
-        const e = r[1] as ValidationError
+        const e = /** @type {ValidationError} */ (r[1])
         if (e.path.length !== expected.length) { throw `path length ${e.path.length} != ${expected.length}` }
         for (let i = 0; i < expected.length; i++) {
             if (e.path[i] !== expected[i]) { throw `path[${i}] ${e.path[i]} != ${expected[i]}` }
         }
     }
 
-const assertDeepEqual = (a: unknown, b: unknown): void => {
+/** @type {(a: unknown, b: unknown) => void} */
+const assertDeepEqual = (a, b) => {
     if (a === b) { return }
     if (a instanceof Array && b instanceof Array) {
         if (a.length !== b.length) { throw `array length ${a.length} != ${b.length}` }
@@ -38,7 +51,7 @@ const assertDeepEqual = (a: unknown, b: unknown): void => {
         if (ka.length !== kb.length) { throw `key count ${ka.length} != ${kb.length}` }
         for (let i = 0; i < ka.length; i++) {
             if (ka[i] !== kb[i]) { throw `key ${ka[i]} != ${kb[i]}` }
-            assertDeepEqual((a as any)[ka[i]], (b as any)[kb[i]])
+            assertDeepEqual((/** @type {any} */ (a))[ka[i]], (/** @type {any} */ (b))[kb[i]])
         }
         return
     }
@@ -48,7 +61,7 @@ const assertDeepEqual = (a: unknown, b: unknown): void => {
 export const proof = {
     boolean: {
         ok: () => {
-            type _ = Assert<Equal<Ts<typeof boolean>, boolean>>
+            /** @typedef {Assert<Equal<Ts<typeof boolean>, boolean>>} _RoundTrip */
             assertOk(parse(boolean)(true))
             assertOk(parse(boolean)(false))
         },
@@ -60,7 +73,7 @@ export const proof = {
     },
     number: {
         ok: () => {
-            type _ = Assert<Equal<Ts<typeof number>, number>>
+            /** @typedef {Assert<Equal<Ts<typeof number>, number>>} _RoundTrip */
             assertOk(parse(number)(42))
         },
         error: () => {
@@ -70,7 +83,7 @@ export const proof = {
     },
     string: {
         ok: () => {
-            type _ = Assert<Equal<Ts<typeof string>, string>>
+            /** @typedef {Assert<Equal<Ts<typeof string>, string>>} _RoundTrip */
             assertOk(parse(string)('hello'))
         },
         error: () => {
@@ -80,7 +93,7 @@ export const proof = {
     },
     bigint: {
         ok: () => {
-            type _ = Assert<Equal<Ts<typeof bigint>, bigint>>
+            /** @typedef {Assert<Equal<Ts<typeof bigint>, bigint>>} _RoundTrip */
             assertOk(parse(bigint)(4n))
         },
         error: () => {
@@ -90,7 +103,7 @@ export const proof = {
     },
     unknown: {
         ok: () => {
-            type _ = Assert<Equal<Ts<typeof unknown>, DjsUnknown>>
+            /** @typedef {Assert<Equal<Ts<typeof unknown>, DjsUnknown>>} _RoundTrip */
             assertOk(parse(unknown)(null))
             assertOk(parse(unknown)(42))
             assertOk(parse(unknown)('hello'))
@@ -112,80 +125,80 @@ export const proof = {
             error: () => assertError(parse(undefined)(null)),
         },
         number: {
-            ok: () => assertOk(parse(42 as const)(42)),
-            error: () => assertError(parse(42 as const)(43)),
+            ok: () => assertOk(parse(/** @type {const} */ (42))(42)),
+            error: () => assertError(parse(/** @type {const} */ (42))(43)),
         },
         nan: {
-            ok: () => assertOk(parse(NaN as number)(NaN)),
+            ok: () => assertOk(parse(/** @type {number} */ (NaN))(NaN)),
             error: () => {
-                assertError(parse(NaN as number)(0))
-                assertError(parse(0 as const)(NaN))
-                assertError(parse(42 as const)(NaN))
+                assertError(parse(/** @type {number} */ (NaN))(0))
+                assertError(parse(/** @type {const} */ (0))(NaN))
+                assertError(parse(/** @type {const} */ (42))(NaN))
             },
         },
         infinity: {
             ok: () => {
-                assertOk(parse(Infinity as number)(Infinity))
-                assertOk(parse(-Infinity as number)(-Infinity))
+                assertOk(parse(/** @type {number} */ (Infinity))(Infinity))
+                assertOk(parse(/** @type {number} */ (-Infinity))(-Infinity))
             },
             error: () => {
-                assertError(parse(Infinity as number)(-Infinity))
-                assertError(parse(Infinity as number)(0))
+                assertError(parse(/** @type {number} */ (Infinity))(-Infinity))
+                assertError(parse(/** @type {number} */ (Infinity))(0))
             },
         },
         signedZero: {
             // `Object.is` distinguishes +0 and -0; `===` treats them equal.
             distinct: () => {
-                assertError(parse(0 as const)(-0))
-                assertError(parse(-0 as number)(0))
+                assertError(parse(/** @type {const} */ (0))(-0))
+                assertError(parse(/** @type {number} */ (-0))(0))
             },
             self: () => {
-                assertOk(parse(0 as const)(0))
-                assertOk(parse(-0 as number)(-0))
+                assertOk(parse(/** @type {const} */ (0))(0))
+                assertOk(parse(/** @type {number} */ (-0))(-0))
             },
         },
         string: {
-            ok: () => assertOk(parse('hello' as const)('hello')),
-            error: () => assertError(parse('hello' as const)('world')),
+            ok: () => assertOk(parse(/** @type {const} */ ('hello'))('hello')),
+            error: () => assertError(parse(/** @type {const} */ ('hello'))('world')),
         },
         bigint: {
-            ok: () => assertOk(parse(7n as const)(7n)),
-            error: () => assertError(parse(7n as const)(8n)),
+            ok: () => assertOk(parse(/** @type {const} */ (7n))(7n)),
+            error: () => assertError(parse(/** @type {const} */ (7n))(8n)),
         },
         boolean: {
-            ok: () => assertOk(parse(true as const)(true)),
-            error: () => assertError(parse(true as const)(false)),
+            ok: () => assertOk(parse(/** @type {const} */ (true))(true)),
+            error: () => assertError(parse(/** @type {const} */ (true))(false)),
         },
         tuple: {
             ok: () => {
-                const t = [42, 'hello'] as const
+                const t = /** @type {const} */ ([42, 'hello'])
                 const r = parse(t)([42, 'hello'])
                 assertDeepEqual(unwrap(r), [42, 'hello'])
             },
             // The key behavior change vs `validate`: extra tuple elements are dropped.
             extraItemsDropped: () => {
-                const r = parse([42] as const)([42, 'extra'])
+                const r = parse(/** @type {const} */ ([42]))([42, 'extra'])
                 assertDeepEqual(unwrap(r), [42])
             },
             error: () => {
-                assertError(parse([42] as const)([99]))
-                assertError(parse([42] as const)({}))
+                assertError(parse(/** @type {const} */ ([42]))([99]))
+                assertError(parse(/** @type {const} */ ([42]))({}))
             },
         },
         struct: {
             ok: () => {
-                const t = { a: 42, b: 'hello' } as const
+                const t = /** @type {const} */ ({ a: 42, b: 'hello' })
                 const r = parse(t)({ a: 42, b: 'hello' })
                 assertDeepEqual(unwrap(r), { a: 42, b: 'hello' })
             },
             // Undeclared properties are dropped from the constructed value.
             extraKeysDropped: () => {
-                const r = parse({ a: 42 as const } as const)({ a: 42, b: 'extra' })
+                const r = parse(/** @type {const} */ ({ a: /** @type {const} */ (42) }))({ a: 42, b: 'extra' })
                 assertDeepEqual(unwrap(r), { a: 42 })
             },
             error: () => {
-                assertError(parse({ a: 42 } as const)({ a: 99 }))
-                assertError(parse({ a: 42 } as const)([]))
+                assertError(parse(/** @type {const} */ ({ a: 42 }))({ a: 99 }))
+                assertError(parse(/** @type {const} */ ({ a: 42 }))([]))
             },
         },
     },
@@ -201,8 +214,9 @@ export const proof = {
         // `parse` always constructs a new array, even when the inner type is a primitive.
         freshArray: () => {
             const input = [1, 2, 3]
-            const out = unwrap<readonly number[]>(parse(array(number))(input))
-            assert(out !== input as unknown, 'expected a fresh array')
+            /** @type {readonly number[]} */
+            const out = unwrap(parse(array(number))(input))
+            assert(out !== /** @type {unknown} */ (input), 'expected a fresh array')
             assertDeepEqual(out, [1, 2, 3])
         },
         error: () => {
@@ -228,8 +242,9 @@ export const proof = {
         // `parse` always constructs a new record.
         freshRecord: () => {
             const input = { a: 1, b: 2 }
-            const out = unwrap<Record<string, number>>(parse(record(number))(input))
-            assert(out !== input as unknown, 'expected a fresh record')
+            /** @type {Record<string, number>} */
+            const out = unwrap(parse(record(number))(input))
+            assert(out !== /** @type {unknown} */ (input), 'expected a fresh record')
             assertDeepEqual(out, { a: 1, b: 2 })
         },
         error: () => {
@@ -240,7 +255,7 @@ export const proof = {
     },
     constThunk: {
         primitive: () => {
-            const t = () => ['const', 7n] as const
+            const t = () => /** @type {const} */ (['const', 7n])
             assertOk(parse(t)(7n))
             assertError(parse(t)(8n))
         },
@@ -248,13 +263,13 @@ export const proof = {
     or: {
         consts: {
             ok: () => {
-                const t = or(...[false, 42, 'hello'] as const)
+                const t = or(.../** @type {const} */ ([false, 42, 'hello']))
                 assertOk(parse(t)(false))
                 assertOk(parse(t)(42))
                 assertOk(parse(t)('hello'))
             },
             error: () => {
-                const t = or(...[false, 42, 'hello'] as const)
+                const t = or(.../** @type {const} */ ([false, 42, 'hello']))
                 assertError(parse(t)(true))
                 assertError(parse(t)(43))
                 assertError(parse(t)('world'))
@@ -275,8 +290,9 @@ export const proof = {
         },
         // First matching variant wins; the freshly-constructed value comes from that variant.
         firstMatchWins: () => {
-            const t = or([number] as const, array(number))
-            const out = unwrap<readonly number[]>(parse(t)([1, 2, 3]))
+            const t = or(/** @type {const} */ ([number]), array(number))
+            /** @type {readonly number[]} */
+            const out = unwrap(parse(t)([1, 2, 3]))
             // The const tuple `[number]` matches first and returns a length-1 result.
             assertDeepEqual(out, [1])
         },
@@ -304,29 +320,29 @@ export const proof = {
             parse(array(array(number)))([[1, 'x'], [2, 3]])
         ),
         tupleIndex: () => assertErrorPath(['1'])(
-            parse([number, number] as const)([1, 'two'])
+            parse(/** @type {const} */ ([number, number]))([1, 'two'])
         ),
         structKey: () => assertErrorPath(['b'])(
-            parse({ a: number, b: number } as const)({ a: 1, b: 'two' })
+            parse(/** @type {const} */ ({ a: number, b: number }))({ a: 1, b: 'two' })
         ),
         deepStruct: () => {
-            const schema = { user: { name: string, age: number } } as const
+            const schema = /** @type {const} */ ({ user: { name: string, age: number } })
             const r = parse(schema)({ user: { name: 'A', age: 'old' } })
             assertErrorPath(['user', 'age'])(r)
         },
         recursiveSchema: () => {
-            type A = readonly A[]
-            const list = () => ['array', list] as const
-            const r = parse(list)([[[42]] as unknown as A])
+            /** @typedef {readonly _A[]} _A */
+            const list = () => /** @type {const} */ (['array', list])
+            const r = parse(list)([/** @type {_A} */ (/** @type {unknown} */ ([[42]]))])
             assertErrorPath(['0', '0', '0'])(r)
         },
         orRoot: () => assertErrorPath([])(parse(or(number, string))(true)),
     },
     recursive: {
         arrayOfArrays: () => {
-            type A = readonly A[]
-            const list = () => ['array', list] as const
-            type _A = Assert<Equal<A, Ts<typeof list>>>
+            /** @typedef {readonly _A[]} _A */
+            const list = () => /** @type {const} */ (['array', list])
+            /** @typedef {Assert<Equal<_A, Ts<typeof list>>>} _ListRoundTrip */
             const v = parse(list)
             assertOk(v([]))
             assertOk(v([[], []]))
@@ -335,9 +351,9 @@ export const proof = {
             assertError(v(null))
         },
         recordOfRecords: () => {
-            const tree = () => ['record', tree] as const
-            type A = { readonly[K in string]?: A }
-            type _ = Assert<Equal<A, Ts<typeof tree>>>
+            const tree = () => /** @type {const} */ (['record', tree])
+            /** @typedef {{ readonly[K in string]?: _A }} _A */
+            /** @typedef {Assert<Equal<_A, Ts<typeof tree>>>} _TreeRoundTrip */
             const v = parse(tree)
             assertOk(v({}))
             assertOk(v({ a: {}, b: { c: {} } }))
diff --git a/fjs/types/rtti/todo/proof-shared-asserts.md b/fjs/types/rtti/todo/proof-shared-asserts.md
index cc4a11eff..594041b74 100644
--- a/fjs/types/rtti/todo/proof-shared-asserts.md
+++ b/fjs/types/rtti/todo/proof-shared-asserts.md
@@ -5,8 +5,8 @@
 
 ## Problem
 
-`fjs/types/rtti/validate/proof.f.ts:9-20` and
-`fjs/types/rtti/parse/proof.f.ts:9-25` define byte-identical helpers:
+`fjs/types/rtti/validate/proof.f.mjs:13-29` and
+`fjs/types/rtti/parse/proof.f.mjs:13-38` define byte-identical helpers:
 
 ```ts
 const assertOk = ([k]: readonly [string, unknown]) => { assertEq(k, 'ok', 'expected ok') }
@@ -20,18 +20,18 @@ const assertErrorPath = (expected: readonly string[]) =>
     }
 ```
 
-In addition, `parse/proof.f.ts:12-15` hand-rolls an `unwrap` that duplicates
+In addition, `parse/proof.f.mjs:19-27` hand-rolls an `unwrap` that duplicates
 `unwrap` from `fjs/types/result/module.f.mjs:59` (assert `'ok'`, return the
 payload), and `assertErrorPath`/`assertDeepEqual`
-(`parse/proof.f.ts:17-45`) still use raw `if`/`throw` instead of
+(`parse/proof.f.mjs:29-59`) still use raw `if`/`throw` instead of
 `assert`/`assertEq`, contrary to the proof-assertion rule in `AGENTS.md`
 (each local `if`/`throw` is a permanently-uncovered branch).
 
 Beyond the helpers, roughly 80% of the two proof trees are copy-pasted
 verbatim modulo the checker name (`validate` vs `parse`): the `boolean` /
 `number` / `string` / `bigint` / `unknown` / `const` / `or` / `option` /
-`path` / `recursive` suites (`validate/proof.f.ts:22-75,273-326` vs
-`parse/proof.f.ts:47-100,295-345`). Only the container *success* cases
+`path` / `recursive` suites (`validate/proof.f.mjs:29-83,280-334` vs
+`parse/proof.f.mjs:60-113,311-362`). Only the container *success* cases
 legitimately differ (validate asserts identity of the returned value; parse
 asserts fresh construction and dropped extras via `assertDeepEqual`).
 
@@ -45,14 +45,14 @@ Two steps; the first is the high-confidence part:
      `fjs/asserts/module.f.mjs` (type-only import of `Result` from
      `fjs/types/result`, or structural `readonly [string, unknown]` to keep
      `fjs/asserts` dependency-free).
-   - Replace `parse/proof.f.ts`'s local `unwrap` with `unwrap` from
+   - Replace `parse/proof.f.mjs`'s local `unwrap` with `unwrap` from
      `fjs/types/result/module.f.mjs`.
    - Rewrite `assertErrorPath` with `assertEq` (compare `e.path.length` and
      each element, or compare the joined path string), export it from one
      place both proofs can import — since `ValidationError` is owned by
      `validate` (parse already reuses it per `AGENTS.md`), exporting the
      helper from a small shared rtti proof-helper module (or from
-     `validate/proof.f.ts`) keeps it next to the type it inspects.
+     `validate/proof.f.mjs`) keeps it next to the type it inspects.
 
 2. **Suite factory (optional, larger).** Extract a
    `commonSuite(check: <T>(rtti: T) => (input: unknown) => Result<…>)`
diff --git a/fjs/types/rtti/validate/proof.f.ts b/fjs/types/rtti/validate/proof.f.mjs
similarity index 54%
rename from fjs/types/rtti/validate/proof.f.ts
rename to fjs/types/rtti/validate/proof.f.mjs
index ee86601d1..bd189d7fa 100644
--- a/fjs/types/rtti/validate/proof.f.ts
+++ b/fjs/types/rtti/validate/proof.f.mjs
@@ -1,19 +1,26 @@
+/**
+ * @import { ValidationError } from '../common/types.ts'
+ * @import { Equal } from '../../ts/types.ts'
+ * @import { Ts } from '../ts/types.ts'
+ * @import { Unknown as DjsUnknown } from '../../../djs/types.ts'
+ * @import { Assert } from '../../../asserts/types.ts'
+ */
+
 import { validate } from './module.f.mjs'
-import type { ValidationError } from '../common/types.ts'
 import { boolean, number, string, bigint, unknown, array, record, or, option } from '../module.f.mjs'
-import type { Equal } from '../../ts/types.ts'
-import type { Ts } from '../ts/types.ts'
-import type { Unknown as DjsUnknown } from '../../../djs/types.ts'
-import type { Assert } from '../../../asserts/types.ts'
 import { assert, assertEq } from '../../../asserts/module.f.mjs'
 
-const assertOk = ([k]: readonly [string, unknown]) => { assertEq(k, 'ok', 'expected ok') }
-const assertError = ([k]: readonly [string, unknown]) => { assertEq(k, 'error', 'expected error') }
+/** @type {(r: readonly [string, unknown]) => void} */
+const assertOk = ([k]) => { assertEq(k, 'ok', 'expected ok') }
+
+/** @type {(r: readonly [string, unknown]) => void} */
+const assertError = ([k]) => { assertEq(k, 'error', 'expected error') }
 
-const assertErrorPath = (expected: readonly string[]) =>
-    (r: readonly [string, unknown]) => {
+/** @type {(expected: readonly string[]) => (r: readonly [string, unknown]) => void} */
+const assertErrorPath = expected =>
+    r => {
         assert(r[0] === 'error', 'expected error')
-        const e = r[1] as ValidationError
+        const e = /** @type {ValidationError} */ (r[1])
         if (e.path.length !== expected.length) { throw `path length ${e.path.length} != ${expected.length}` }
         for (let i = 0; i < expected.length; i++) {
             if (e.path[i] !== expected[i]) { throw `path[${i}] ${e.path[i]} != ${expected[i]}` }
@@ -23,7 +30,7 @@ const assertErrorPath = (expected: readonly string[]) =>
 export const proof = {
     boolean: {
         ok: () => {
-            type _ = Assert<Equal<Ts<typeof boolean>, boolean>>
+            /** @typedef {Assert<Equal<Ts<typeof boolean>, boolean>>} _RoundTrip */
             assertOk(validate(boolean)(true))
             assertOk(validate(boolean)(false))
         },
@@ -35,7 +42,7 @@ export const proof = {
     },
     number: {
         ok: () => {
-            type _ = Assert<Equal<Ts<typeof number>, number>>
+            /** @typedef {Assert<Equal<Ts<typeof number>, number>>} _RoundTrip */
             assertOk(validate(number)(42))
         },
         error: () => {
@@ -45,7 +52,7 @@ export const proof = {
     },
     string: {
         ok: () => {
-            type _ = Assert<Equal<Ts<typeof string>, string>>
+            /** @typedef {Assert<Equal<Ts<typeof string>, string>>} _RoundTrip */
             assertOk(validate(string)('hello'))
         },
         error: () => {
@@ -55,7 +62,7 @@ export const proof = {
     },
     bigint: {
         ok: () => {
-            type _ = Assert<Equal<Ts<typeof bigint>, bigint>>
+            /** @typedef {Assert<Equal<Ts<typeof bigint>, bigint>>} _RoundTrip */
             assertOk(validate(bigint)(4n))
         },
         error: () => {
@@ -65,7 +72,7 @@ export const proof = {
     },
     unknown: {
         ok: () => {
-            type _ = Assert<Equal<Ts<typeof unknown>, DjsUnknown>>
+            /** @typedef {Assert<Equal<Ts<typeof unknown>, DjsUnknown>>} _RoundTrip */
             assertOk(validate(unknown)(null))
             assertOk(validate(unknown)(42))
             assertOk(validate(unknown)('hello'))
@@ -77,7 +84,7 @@ export const proof = {
     const: {
         null: {
             ok: () => {
-                type _ = Assert<Equal<Ts<null>, null>>
+                /** @typedef {Assert<Equal<Ts<null>, null>>} _RoundTrip */
                 assertOk(validate(null)(null))
             },
             error: () => {
@@ -87,90 +94,90 @@ export const proof = {
         },
         undefined: {
             ok: () => {
-                type _ = Assert<Equal<Ts<undefined>, undefined>>
+                /** @typedef {Assert<Equal<Ts<undefined>, undefined>>} _RoundTrip */
                 assertOk(validate(undefined)(undefined))
             },
             error: () => assertError(validate(undefined)(null)),
         },
         number: {
             ok: () => {
-                type _ = Assert<Equal<Ts<42>, 42>>
-                assertOk(validate(42 as const)(42))
+                /** @typedef {Assert<Equal<Ts<42>, 42>>} _RoundTrip */
+                assertOk(validate(/** @type {const} */ (42))(42))
             },
-            error: () => assertError(validate(42 as const)(43)),
+            error: () => assertError(validate(/** @type {const} */ (42))(43)),
         },
         nan: {
-            ok: () => assertOk(validate(NaN as number)(NaN)),
+            ok: () => assertOk(validate(/** @type {number} */ (NaN))(NaN)),
             error: () => {
-                assertError(validate(NaN as number)(0))
-                assertError(validate(0 as const)(NaN))
-                assertError(validate(42 as const)(NaN))
+                assertError(validate(/** @type {number} */ (NaN))(0))
+                assertError(validate(/** @type {const} */ (0))(NaN))
+                assertError(validate(/** @type {const} */ (42))(NaN))
             },
         },
         infinity: {
             ok: () => {
-                assertOk(validate(Infinity as number)(Infinity))
-                assertOk(validate(-Infinity as number)(-Infinity))
+                assertOk(validate(/** @type {number} */ (Infinity))(Infinity))
+                assertOk(validate(/** @type {number} */ (-Infinity))(-Infinity))
             },
             error: () => {
-                assertError(validate(Infinity as number)(-Infinity))
-                assertError(validate(Infinity as number)(0))
+                assertError(validate(/** @type {number} */ (Infinity))(-Infinity))
+                assertError(validate(/** @type {number} */ (Infinity))(0))
             },
         },
         signedZero: {
             // `Object.is` distinguishes +0 and -0; `===` treats them equal.
             distinct: () => {
-                assertError(validate(0 as const)(-0))
-                assertError(validate(-0 as number)(0))
+                assertError(validate(/** @type {const} */ (0))(-0))
+                assertError(validate(/** @type {number} */ (-0))(0))
             },
             self: () => {
-                assertOk(validate(0 as const)(0))
-                assertOk(validate(-0 as number)(-0))
+                assertOk(validate(/** @type {const} */ (0))(0))
+                assertOk(validate(/** @type {number} */ (-0))(-0))
             },
         },
         string: {
             ok: () => {
-                type _ = Assert<Equal<Ts<'hello'>, 'hello'>>
-                assertOk(validate('hello' as const)('hello'))
+                /** @typedef {Assert<Equal<Ts<'hello'>, 'hello'>>} _RoundTrip */
+                assertOk(validate(/** @type {const} */ ('hello'))('hello'))
             },
-            error: () => assertError(validate('hello' as const)('world')),
+            error: () => assertError(validate(/** @type {const} */ ('hello'))('world')),
         },
         bigint: {
             ok: () => {
-                type _ = Assert<Equal<Ts<7n>, 7n>>
-                assertOk(validate(7n as const)(7n))
+                /** @typedef {Assert<Equal<Ts<7n>, 7n>>} _RoundTrip */
+                assertOk(validate(/** @type {const} */ (7n))(7n))
             },
-            error: () => assertError(validate(7n as const)(8n)),
+            error: () => assertError(validate(/** @type {const} */ (7n))(8n)),
         },
         boolean: {
             ok: () => {
-                type _ = Assert<Equal<Ts<true>, true>>
-                assertOk(validate(true as const)(true))
+                /** @typedef {Assert<Equal<Ts<true>, true>>} _RoundTrip */
+                assertOk(validate(/** @type {const} */ (true))(true))
             },
-            error: () => assertError(validate(true as const)(false)),
+            error: () => assertError(validate(/** @type {const} */ (true))(false)),
         },
         tuple: {
             ok: () => {
-                const t = [42, 'hello'] as const
-                type _ = Assert<Equal<Ts<typeof t>, readonly[42, 'hello']>>
+                const t = /** @type {const} */ ([42, 'hello'])
+                /** @typedef {Assert<Equal<Ts<typeof t>, readonly[42, 'hello']>>} _RoundTrip */
                 assertOk(validate(t)([42, 'hello']))
             },
-            extraItems: () => assertOk(validate([42] as const)([42, 'extra'])),
+            extraItems: () => assertOk(validate(/** @type {const} */ ([42]))([42, 'extra'])),
             error: () => {
-                assertError(validate([42] as const)([99]))
-                assertError(validate([42] as const)({}))
+                assertError(validate(/** @type {const} */ ([42]))([99]))
+                assertError(validate(/** @type {const} */ ([42]))({}))
             },
         },
         struct: {
             ok: () => {
-                const t = { a: 42, b: 'hello' } as const
-                type _ = Assert<Equal<Ts<typeof t>, { readonly a: 42, readonly b: 'hello' }>>
+                const t = /** @type {const} */ ({ a: 42, b: 'hello' })
+                /** @typedef {Assert<Equal<Ts<typeof t>, { readonly a: 42, readonly b: 'hello' }>>} _RoundTrip */
                 assertOk(validate(t)({ a: 42, b: 'hello' }))
             },
-            extraKeys: () => assertOk(validate({ a: 42 as const } as const)({ a: 42, b: 'extra' })),
+            extraKeys: () => assertOk(validate(/** @type {const} */ ({ a: /** @type {const} */ (42) }))({ a: 42, b: 'extra' })),
             error: () => {
-                assertError(validate({ a: 42 } as const)({ a: 99 }))
-                assertError(validate({ a: 42 } as const)([]))
+                assertError(validate(/** @type {const} */ ({ a: 42 }))({ a: 99 }))
+                assertError(validate(/** @type {const} */ ({ a: 42 }))([]))
             },
         },
     },
@@ -178,7 +185,7 @@ export const proof = {
         empty: () => assertOk(validate(array(number))([])),
         ok: () => {
             const t = array(number)
-            type _ = Assert<Equal<Ts<typeof t>, readonly number[]>>
+            /** @typedef {Assert<Equal<Ts<typeof t>, readonly number[]>>} _RoundTrip */
             assertOk(validate(array(number))([1, 2, 3]))
         },
         error: () => {
@@ -188,7 +195,7 @@ export const proof = {
         },
         nested: () => {
             const t = array(array(boolean))
-            type _ = Assert<Equal<Ts<typeof t>, readonly (readonly boolean[])[]>>
+            /** @typedef {Assert<Equal<Ts<typeof t>, readonly (readonly boolean[])[]>>} _RoundTrip */
             assertOk(validate(array(array(boolean)))([[true, false], [false]]))
             assertError(validate(array(array(boolean)))([[true, 42]]))
         },
@@ -197,7 +204,7 @@ export const proof = {
         empty: () => assertOk(validate(record(number))({})),
         ok: () => {
             const t = record(string)
-            type _ = Assert<Equal<Ts<typeof t>, { readonly[K in string]?: string }>>
+            /** @typedef {Assert<Equal<Ts<typeof t>, { readonly[K in string]?: string }>>} _RoundTrip */
             assertOk(validate(t)({ a: 'hello', b: 'world' }))
         },
         error: () => {
@@ -208,8 +215,8 @@ export const proof = {
     },
     constThunk: {
         primitive: () => {
-            const t = () => ['const', 7n] as const
-            type _ = Assert<Equal<Ts<typeof t>, 7n>>
+            const t = () => /** @type {const} */ (['const', 7n])
+            /** @typedef {Assert<Equal<Ts<typeof t>, 7n>>} _RoundTrip */
             assertOk(validate(t)(7n))
             assertError(validate(t)(8n))
         },
@@ -217,14 +224,14 @@ export const proof = {
     or: {
         consts: {
             ok: () => {
-                const t = or(...[false,42, 'hello'] as const)
-                type _ = Assert<Equal<Ts<typeof t>, false | 42 | 'hello'>>
+                const t = or(.../** @type {const} */ ([false,42, 'hello']))
+                /** @typedef {Assert<Equal<Ts<typeof t>, false | 42 | 'hello'>>} _RoundTrip */
                 assertOk(validate(t)(false))
                 assertOk(validate(t)(42))
                 assertOk(validate(t)('hello'))
             },
             error: () => {
-                const t = or(...[false, 42, 'hello'] as const)
+                const t = or(.../** @type {const} */ ([false, 42, 'hello']))
                 assertError(validate(t)(true))
                 assertError(validate(t)(43))
                 assertError(validate(t)('world'))
@@ -234,7 +241,7 @@ export const proof = {
         thunks: {
             ok: () => {
                 const t = or(number, string)
-                type _ = Assert<Equal<Ts<typeof t>, number | string>>
+                /** @typedef {Assert<Equal<Ts<typeof t>, number | string>>} _RoundTrip */
                 assertOk(validate(t)(42))
                 assertOk(validate(t)('hello'))
             },
@@ -246,13 +253,13 @@ export const proof = {
         },
         mixed: {
             ok: () => {
-                const t = or(42 as const, string)
-                type _ = Assert<Equal<Ts<typeof t>, 42 | string>>
+                const t = or(/** @type {const} */ (42), string)
+                /** @typedef {Assert<Equal<Ts<typeof t>, 42 | string>>} _RoundTrip */
                 assertOk(validate(t)(42))
                 assertOk(validate(t)('hello'))
             },
             error: () => {
-                const t = or(42 as const, string)
+                const t = or(/** @type {const} */ (42), string)
                 assertError(validate(t)(43))
                 assertError(validate(t)(null))
             },
@@ -261,7 +268,7 @@ export const proof = {
     option: {
         ok: () => {
             const t = option(number)
-            type _ = Assert<Equal<Ts<typeof t>, number | undefined>>
+            /** @typedef {Assert<Equal<Ts<typeof t>, number | undefined>>} _RoundTrip */
             assertOk(validate(t)(42))
             assertOk(validate(t)(undefined))
         },
@@ -283,31 +290,31 @@ export const proof = {
             validate(array(array(number)))([[1, 'x'], [2, 3]])
         ),
         tupleIndex: () => assertErrorPath(['1'])(
-            validate([number, number] as const)([1, 'two'])
+            validate(/** @type {const} */ ([number, number]))([1, 'two'])
         ),
         structKey: () => assertErrorPath(['b'])(
-            validate({ a: number, b: number } as const)({ a: 1, b: 'two' })
+            validate(/** @type {const} */ ({ a: number, b: number }))({ a: 1, b: 'two' })
         ),
         deepStruct: () => {
-            const schema = { user: { name: string, age: number } } as const
+            const schema = /** @type {const} */ ({ user: { name: string, age: number } })
             const r = validate(schema)({ user: { name: 'A', age: 'old' } })
             assertErrorPath(['user', 'age'])(r)
         },
         recursiveSchema: () => {
-            type A = readonly A[]
-            const list = () => ['array', list] as const
+            /** @typedef {readonly _A[]} _A */
+            const list = () => /** @type {const} */ (['array', list])
             // [[[42]]] — innermost element 42 is a number, not an array
-            const r = validate(list)([[[42]] as unknown as A])
+            const r = validate(list)([/** @type {_A} */ (/** @type {unknown} */ ([[42]]))])
             assertErrorPath(['0', '0', '0'])(r)
         },
         orRoot: () => assertErrorPath([])(validate(or(number, string))(true)),
     },
     recursive: {
         arrayOfArrays: () => {
-            type A = readonly A[]
+            /** @typedef {readonly _A[]} _A */
             // self-referential schema: an array whose elements are also arrays of the same type
-            const list = () => ['array', list] as const
-            type _A = Assert<Equal<A, Ts<typeof list>>>
+            const list = () => /** @type {const} */ (['array', list])
+            /** @typedef {Assert<Equal<_A, Ts<typeof list>>>} _RoundTripA */
             const v = validate(list)
             assertOk(v([]))
             assertOk(v([[], []]))
@@ -316,9 +323,9 @@ export const proof = {
             assertError(v(null))
         },
         recordOfRecords: () => {
-            const tree = () => ['record', tree] as const
-            type A = { readonly[K in string]?: A }
-            type _ = Assert<Equal<A, Ts<typeof tree>>>
+            const tree = () => /** @type {const} */ (['record', tree])
+            /** @typedef {{ readonly[K in string]?: _A }} _A */
+            /** @typedef {Assert<Equal<_A, Ts<typeof tree>>>} _RoundTrip */
             const v = validate(tree)
             assertOk(v({}))
             assertOk(v({ a: {}, b: { c: {} } }))
@@ -326,22 +333,28 @@ export const proof = {
         },
     },
     funcParam: () => {
-        const paramSet0 = ['hello', bigint] as const
-        const paramSet1 = ['goodbye', string, 43] as const
+        const paramSet0 = /** @type {const} */ (['hello', bigint])
+        const paramSet1 = /** @type {const} */ (['goodbye', string, 43])
 
         const paramSet01 = or(paramSet0, paramSet1)
 
-        type Param0 = Ts<typeof paramSet0>
-        type Param1 = Ts<typeof paramSet1>
-        type Param01 = Ts<typeof paramSet01>
+        /** @typedef {Ts<typeof paramSet0>} _Param0 */
+        /** @typedef {Ts<typeof paramSet1>} _Param1 */
+        /** @typedef {Ts<typeof paramSet01>} _Param01 */
 
         const v0 = validate(paramSet0)
         const v1 = validate(paramSet1)
 
-        type F0<T> = (...args: Param0) => T
-        type F1<T> = (...args: Param1) => T
+        /** @template T @typedef {(...args: _Param0) => T} _F0 */
+        /** @template T @typedef {(...args: _Param1) => T} _F1 */
 
-        const func = <T>(f0: F0<T>, f1: F1<T>) => (...args: Param01): T => {
+        /**
+         * @template T
+         * @param {_F0<T>} f0
+         * @param {_F1<T>} f1
+         * @returns {(...args: _Param01) => T}
+         */
+        const func = (f0, f1) => (...args) => {
             {
                 const [t, r] = v0(args)
                 if (t === 'ok') {
@@ -357,10 +370,13 @@ export const proof = {
             throw 'unreachable: args did not match any parameter set'
         }
 
-        const f0 = (a: 'hello', b: bigint): number => 42
-        const f1 = (a: 'goodbye', b: string, c: 43): number => 13
+        /** @type {(a: 'hello', b: bigint) => number} */
+        const f0 = (a, b) => 42
+        /** @type {(a: 'goodbye', b: string, c: 43) => number} */
+        const f1 = (a, b, c) => 13
 
-        const x: (...args: Param01) => number = func(f0, f1)
+        /** @type {(...args: _Param01) => number} */
+        const x = func(f0, f1)
 
         return () => {
             assertEq(x('hello', 42n), 42)
@@ -373,17 +389,23 @@ export const proof = {
 
         const param01 = or(param0, param1)
 
-        type Param0 = Ts<typeof param0>
-        type Param1 = Ts<typeof param1>
-        type Param01 = Ts<typeof param01>
+        /** @typedef {Ts<typeof param0>} _Param0 */
+        /** @typedef {Ts<typeof param1>} _Param1 */
+        /** @typedef {Ts<typeof param01>} _Param01 */
 
         const v0 = validate(param0)
         const v1 = validate(param1)
 
-        type F0<T> = (args: Param0) => T
-        type F1<T> = (args: Param1) => T
+        /** @template T @typedef {(args: _Param0) => T} _F0 */
+        /** @template T @typedef {(args: _Param1) => T} _F1 */
 
-        const func = <T>(f0: F0<T>, f1: F1<T>) => (args: Param01): T => {
+        /**
+         * @template T
+         * @param {_F0<T>} f0
+         * @param {_F1<T>} f1
+         * @returns {(args: _Param01) => T}
+         */
+        const func = (f0, f1) => args => {
             {
                 const [t, r] = v0(args)
                 if (t === 'ok') {
@@ -399,10 +421,13 @@ export const proof = {
             throw 'unreachable: args did not match any parameter set'
         }
 
-        const f0 = (args: Param0): number => Number(args.b) + args.a.length
-        const f1 = (args: Param1): number => args.c
+        /** @type {(args: _Param0) => number} */
+        const f0 = args => Number(args.b) + args.a.length
+        /** @type {(args: _Param1) => number} */
+        const f1 = args => args.c
 
-        const x: (args: Param01) => number = func(f0, f1)
+        /** @type {(args: _Param01) => number} */
+        const x = func(f0, f1)
 
         return () => {
             assertEq(x({ a: 'hello', b: 42n }), 47)
diff --git a/fjs/types/todo/66d-ts-printer-tuple-readonly-fold.md b/fjs/types/todo/66d-ts-printer-tuple-readonly-fold.md
index bd94479ee..cb3fa8701 100644
--- a/fjs/types/todo/66d-ts-printer-tuple-readonly-fold.md
+++ b/fjs/types/todo/66d-ts-printer-tuple-readonly-fold.md
@@ -51,7 +51,7 @@ touched anyway, not on its own.
 ### Tasks
 
 - [ ] Replace the `tuple` ternary with `complex(\`${ro}[\`, ']')`.
-- [ ] Confirm `fjs/types/ts/proof.f.ts` still passes (`fjs t`) with both the
+- [ ] Confirm `fjs/types/ts/proof.f.mjs` still passes (`fjs t`) with both the
       mutable and readonly tuple paths covered and `npx tsc` is clean.
 
 ### Related
diff --git a/fjs/types/ts/proof.f.ts b/fjs/types/ts/proof.f.mjs
similarity index 79%
rename from fjs/types/ts/proof.f.ts
rename to fjs/types/ts/proof.f.mjs
index 9269da2b9..6203784a1 100644
--- a/fjs/types/ts/proof.f.ts
+++ b/fjs/types/ts/proof.f.mjs
@@ -1,5 +1,3 @@
-import type { Assert } from '../../asserts/types.ts'
-import type { Equal } from './types.ts'
 import { printer, primitive, union } from './module.f.mjs'
 import { assertEq } from '../../asserts/module.f.mjs'
 
@@ -97,37 +95,3 @@ export const printerMutableRecord = () => {
 }
 
 export const proof = { primitiveNull,primitiveBigint,primitiveString,primitiveNumberFinite,primitiveNumberInfinite,primitiveUndefined,primitiveBoolean,unionEmpty,unionSingle,unionMulti,printerReadonlyTuple,printerReadonlyStruct,printerReadonlyArray,printerReadonlyRecord,printerMutableTuple,printerMutableStruct,printerMutableArray,printerMutableRecord }
-
-// Don't use!
-
-type T0 = {[k:string]: bigint}
-
-declare const x0: T0
-
-type X0 = Assert<Equal<typeof x0['hello'], bigint>>
-
-// Use for finite sets
-
-type T1 = {[k in 'hello']: bigint}
-
-declare const x1: T1
-
-type X1 = Assert<Equal<typeof x1['hello'], bigint>>
-
-// Don't use it
-
-type T2 = {[k in string]: bigint}
-
-declare const x2: T2
-
-type X2 = Assert<Equal<typeof x2['hello'], bigint>>
-
-// Use it for infinite sets
-
-type T3 = {[k in string]?: bigint}
-
-declare const x3: T3
-
-type X3 = Assert<Equal<typeof x3['hello'], bigint | undefined>>
-
-// type T4 = {[k:string]?: bigint} //< compilation error.
diff --git a/fjs/types/ts/types.ts b/fjs/types/ts/types.ts
index 82407c8fd..cb94c611d 100644
--- a/fjs/types/ts/types.ts
+++ b/fjs/types/ts/types.ts
@@ -5,6 +5,8 @@
  * @module
  */
 
+import type { Assert } from '../../asserts/types.ts'
+
 export type Equal<A, B> =
     (<T>() => T extends A ? 1 : 2) extends (<T>() => T extends B ? 1 : 2)
         ? true
@@ -19,3 +21,42 @@ export type Printer = {
     readonly array: (type: string) => string
     readonly record: (type: string) => string
 }
+
+// Index-signature guidance, checked at compile time. Moved here from
+// `proof.f.ts` when that file migrated to `.f.mjs`: `declare const` has no
+// JavaScript form, and these aliases are type-level only. Non-exported, so
+// they add nothing to the emitted declaration.
+
+// Don't use!
+
+type _T0 = {[k:string]: bigint}
+
+declare const x0: _T0
+
+type _X0 = Assert<Equal<typeof x0['hello'], bigint>>
+
+// Use for finite sets
+
+type _T1 = {[k in 'hello']: bigint}
+
+declare const x1: _T1
+
+type _X1 = Assert<Equal<typeof x1['hello'], bigint>>
+
+// Don't use it
+
+type _T2 = {[k in string]: bigint}
+
+declare const x2: _T2
+
+type _X2 = Assert<Equal<typeof x2['hello'], bigint>>
+
+// Use it for infinite sets
+
+type _T3 = {[k in string]?: bigint}
+
+declare const x3: _T3
+
+type _X3 = Assert<Equal<typeof x3['hello'], bigint | undefined>>
+
+// type T4 = {[k:string]?: bigint} //< compilation error.
diff --git a/todo/proof.f.ts b/todo/proof.f.mjs
similarity index 79%
rename from todo/proof.f.ts
rename to todo/proof.f.mjs
index 2402e5b36..311694345 100644
--- a/todo/proof.f.ts
+++ b/todo/proof.f.mjs
@@ -1,15 +1,16 @@
-const at
-: (a: unknown) => (i: any) =>unknown
-= a => i => Object.getOwnPropertyDescriptor(a, i)?.value
+/** @typedef {`<html>${string}</html>`} _TemplateType */
 
-const utf8 = (...x: [readonly string[]]) => x
+/** @type {(a: unknown) => (i: any) => unknown} */
+const at = a => i => Object.getOwnPropertyDescriptor(a, i)?.value
 
-type TemplateType = `<html>${string}</html>`
+/** @type {(...x: [readonly string[]]) => [readonly string[]]} */
+const utf8 = (...x) => x
 
 export const proof = {
     literal: () => {
         const x = utf8`17`
-        const m: TemplateType = '<html>Hello</html>'
+        /** @type {_TemplateType} */
+        const m = '<html>Hello</html>'
     },
     ownProperty: {
         null: {