diff --git a/fjs/bnf/todo/bigint-symbols.md b/fjs/bnf/todo/bigint-symbols.md
index 9415772c6c..d4bd2219b5 100644
--- a/fjs/bnf/todo/bigint-symbols.md
+++ b/fjs/bnf/todo/bigint-symbols.md
@@ -1,135 +1,61 @@
 ## Use 256-bit bigint BNF symbols
 
 **Priority:** P3
-**Status:** blocked
-**Blocked by:** [Bigint-aware JSON parse/serialize](../../media/json/todo/bigint-parse-serialize.md), [Separate alphabet-specific BNF helpers](./unicode-rules.md), [Investigate TerminalRange representation](./terminal-range-representation.md)
+**Status:** open
 
 ### Problem
 
-BNF symbols are currently limited to 24 bits so two range endpoints can be packed
-into one safe JavaScript `number`. This keeps `TerminalRange` compact, but it also
-makes the symbol alphabet an implementation limit of the parser.
+BNF ordinary symbols are currently limited to 24 bits because `TerminalRange`
+packs two endpoint codes into one safe JavaScript `number`.
 
-Layered parsing needs a much larger symbol space. A tokenizer should be able to
-emit a token symbol that the next BNF parser consumes directly, including symbols
-derived from descriptive token names or, later, cryptographic hashes.
+After moving semantic EOF to `-1`, the current domain is:
 
-Changing BNF data from `number` to `bigint` also means the data representation can
-no longer round-trip through native `JSON.parse` / `JSON.stringify`. The bigint-
-precise JSON parse/serialize task provides the JSON-compatible representation this
-change needs.
-
-The generic BNF core should also be separated from alphabet-specific rule
-construction first, so changing the symbol representation does not preserve or
-reinforce the current assumption that BNF symbols are Unicode code points.
+```text
+EOF              = -1
+ordinary symbols = 0 .. 2^24 - 2
+```
 
-The current terminal-range encoding also depends on the 24-bit symbol width. A
-naive uint256 version would shift the first endpoint by 256 bits, making even
-small ranges serialize as very large integers. The representation of
-`TerminalRange` therefore needs a separate design decision before this migration.
+Layered parsing needs a much larger ordinary-symbol space so tokenizer output can
+be consumed directly by another BNF layer.
 
 ### Proposal
 
-Use one fixed 256-bit unsigned symbol representation backed by `bigint`:
+Use bigint ordinary symbols over the full uint256 domain:
 
 ```ts
 type Symbol = bigint
 ```
 
-with the invariant:
-
-```text
-0 <= symbol < 2^256
-```
-
-Reserve the maximal value for EOF:
-
 ```text
-EOF = 2^256 - 1
+EOF              = -1n
+ordinary symbols = 0n .. 2^256 - 1n
 ```
 
-Ordinary input symbols occupy `0 .. EOF - 1`. EOF is represented as a normal
-BNF symbol/range value rather than as a separate terminal kind. This keeps one
-representation throughout the parser stack: scanners, parsers, recognizers,
-serialized BNF data, and range operations do not need a second EOF case in their
-APIs.
-
-Do **not** decide the `TerminalRange` representation in this task. Resolve
-[Investigate TerminalRange representation](./terminal-range-representation.md)
-first. The investigation includes fixed-width bigint packing, bit-interleaved
-bigint packing, other variable-width bigint encodings, and structural
-representations. If the chosen representation is not a primitive bigint, the BNF
-rule/data format may need a broader redesign so terminal ranges remain
-unambiguous from sequences and variants.
-
-Regardless of the chosen representation, define `fullRange` over ordinary input
-symbols only, `0 .. EOF - 1`, while `eof` represents the singleton `EOF .. EOF`.
-Complements over ordinary symbols therefore do not include EOF, while grammars can
-still refer to EOF through the normal terminal-range abstraction.
-
-#### EOF in parser input
-
-Alphabet adapters and callers provide only physical input symbols. They do **not**
-append the reserved EOF value or invent metadata for it. Every parser backend
-instead synthesizes exactly one logical EOF symbol immediately after the last
-physical input symbol.
-
-Keep the public parser position in the physical input domain:
-
-```text
-0 <= idx <= input.length
-```
-
-The parser's internal state must separately record whether the synthesized EOF has
-already been consumed. Conceptually:
-
-```text
-idx < input.length
-    -> match the physical input symbol
-idx == input.length && !eofConsumed
-    -> match the synthesized EOF symbol
-idx == input.length && eofConsumed
-    -> no symbol remains
-```
+No uint256 value is reserved for EOF. Physical parser input contains ordinary
+symbols only; parser backends preserve the logical one-time EOF behavior defined
+by the EOF task.
 
-Matching EOF marks that logical symbol as consumed but does **not** expose a
-physical position beyond the input. Indexed parser results such as
-`DescentMatchResult.idx` therefore report `input.length` after a successful EOF
-match, not `input.length + 1`. Remainder-based public results likewise continue to
-report the empty physical remainder. The extra EOF-consumed state is internal to
-the parser and exists only to prevent a second EOF match.
+`fullRange` covers `0n .. 2^256 - 1n`; `eof` is the singleton `-1n` range.
 
-This preserves the meaning of existing public parser positions and callers that
-check complete consumption with `idx === input.length`, including the DJS
-tokenizer. Parser implementations may choose any internal representation for the
-EOF-consumed bit/state, but must normalize public positions and remainders back to
-the physical input domain.
+This change expands the semantic terminal domain from `2^24` values to
+`2^256 + 1` values, so the current 24-bit `TerminalRange` representation cannot
+be reused. Use the representation selected by the TerminalRange investigation.
 
-The synthesized EOF has no physical source element and therefore contributes no
-ordinary symbol/metadata leaf to the AST. Diagnostics that reject a terminal at
-EOF still point at the physical end position (`input.length`). This avoids
-requiring a generic metadata type `T` to manufacture EOF metadata while keeping
-EOF itself in the same `Symbol` / terminal-range abstraction as every other
-terminal.
+BNF data also needs bigint-precise JSON serialization. Keep that concern in the
+existing bigint JSON work rather than inventing a BNF-specific encoding.
 
-This is parser end-of-stream semantics, not a second EOF type. Alphabet adapters
-must never produce the reserved EOF value as ordinary input; mappings whose
-natural output can reach it must reject or remap it at their boundary.
+Keep this TODO `open` rather than encoding task scheduling in `blocked` metadata.
+The implementation order is still explicit: land the `EOF = -1` semantics first,
+choose the bigint `TerminalRange` representation, and use the bigint-aware JSON
+representation when serialized BNF data is updated.
 
 #### Bigint range infrastructure
 
-BNF terminal containment can compare decoded bigint endpoints directly, but the
-LL(1) backend also needs the existing range-map merge/lookup algorithm. Do not
-copy that algorithm into a BNF-local module. Instead, parameterize the existing
-`fjs/types/range_map` implementation by its ordered boundary type so both number
-and bigint users share the same splitting, ordering, and merge invariants.
-
-The range-map algorithm currently has only two boundary-specific operations:
-
-- comparison/order, used by merge and lookup;
-- predecessor, currently written as `a - 1` by `fromRange`.
+BNF containment can compare bigint semantic endpoints directly.
 
-Factor those into boundary properties, conceptually:
+The LL(1) backend also uses `fjs/types/range_map`; parameterize that shared
+algorithm by boundary type instead of copying it into BNF. The generic boundary
+operations need comparison and predecessor, conceptually:
 
 ```ts
 type BoundaryOps<B> = {
@@ -138,135 +64,46 @@ type BoundaryOps<B> = {
 }
 ```
 
-Then make the core range-map entries/ranges generic over `B`, and route **all**
-boundary ordering and predecessor arithmetic through those operations. The exact
-factory/type names should follow local conventions, but the architecture should
-be equivalent to:
-
-```ts
-rangeMapBy(boundaryOps)(valueOps)
-```
-
-Preserve the existing number-oriented `rangeMap(valueOps)` API as a thin
-instantiation/wrapper using number comparison and `value => value - 1`, so current
-callers do not need an unrelated migration.
-
-For BNF, instantiate the shared range-map boundary type as raw `bigint`, not the
-semantic `Symbol` domain. A range-map entry stores an **upper cut point**, and
-`fromRange` may need a cut point immediately below the first valid symbol. Thus a
-BNF range beginning at `0n` legitimately produces the internal cut point `-1n`:
-
-```text
-[0n, b] -> [[default, -1n], [value, b]]
-```
-
-`-1n` is not a BNF symbol and must never be accepted from an alphabet adapter or
-terminal range. It exists only inside the range-map representation. The `Symbol`
-invariant applies to parser input and terminal endpoints, not to these internal
-cut points. LL(1) lookup still receives a valid `Symbol`; because `Symbol` is
-backed by `bigint`, it can be passed to the bigint range-map lookup without
-converting it to `number`.
-
-This distinction avoids making predecessor fallible and avoids inventing a fake
-BNF symbol below zero. It also matches the existing number range-map semantics,
-where `fromRange([0, b])` already creates an internal `-1` cut point even when the
-consumer's meaningful input domain starts at zero.
-
-The parameterized core should accept a generic inclusive boundary pair
-`readonly [B, B]` rather than depending internally on the existing number-only
-`fjs/types/range.Range`. The current public number wrapper can continue to accept
-that existing `Range` type. This keeps `fjs/types/range` itself number-specific
-while avoiding duplication in `range_map`.
-
-Generic BNF terminal containment does not need a range map and should simply use
-bigint endpoint comparisons (`start <= symbol && symbol <= end`) after obtaining
-the endpoints from the chosen `TerminalRange` representation. No BNF symbol/range
-endpoint should ever be converted to `number` merely to reuse an existing utility.
-
-Unicode code points and bytes are possible symbol alphabets supplied through
-alphabet-specific helpers; the generic BNF core itself should know neither
-Unicode nor byte-stream semantics. Those adapters convert their values into the
-new bigint symbol domain. Metadata carried alongside physical symbols is
-unchanged.
-
-A 256-bit symbol also leaves a natural path for token mappings whose input may be
-arbitrarily large and whose output is a cryptographic hash. Such mappings must
-avoid the single reserved EOF value. That constraint belongs to the mapping
-boundary, not to BNF parsers.
+Preserve the existing number-oriented `rangeMap(...)` API as a thin wrapper.
+For BNF, use raw bigint boundaries. `-1n` may be both semantic EOF and the cut
+point immediately below ordinary `0n`; use `-2n` when a cut point below EOF is
+needed.
 
 ### Tasks
 
-- [ ] Introduce a BNF `Symbol` type backed by `bigint` with the 256-bit invariant.
-- [ ] Reserve `2^256 - 1` as EOF; ordinary symbols are smaller values.
-- [ ] Adopt the `TerminalRange` representation selected by
-      [the representation investigation](./terminal-range-representation.md);
-      do not assume fixed-width `(start << 256n) | end` packing here.
-- [ ] Define `fullRange` over ordinary symbols only and `eof` as the singleton
-      maximal-symbol range using the selected terminal-range representation.
-- [ ] Update generic `rangeEncode`, `rangeDecode`, `oneEncode`, complement/range
-      helpers, and their callers for bigint symbols and the selected range format.
-- [ ] Replace BNF use of number-only `fjs/types/range.contains` with direct
-      `Symbol` endpoint comparison; do not convert bigint endpoints to `number`.
-- [ ] Parameterize the core `fjs/types/range_map` algorithm by boundary type and
-      explicit comparison/predecessor operations; make entry/range boundaries and
-      lookup values generic over that boundary type.
-- [ ] Preserve the current number `rangeMap(...)` API as a thin instantiation of
-      the generic core so existing number callers keep their current behavior.
-- [ ] Instantiate the shared range-map core for BNF with raw `bigint` cut-point
-      boundaries, not the semantic `Symbol` domain; allow the internal `-1n` cut
-      point required for a range beginning at the minimum symbol `0n`.
-- [ ] Keep BNF range-map lookup inputs restricted to valid `Symbol` values even
-      though the map's internal bigint cut points may lie outside the symbol
-      domain.
-- [ ] Keep `fjs/types/range` itself number-specific; the parameterized range-map
-      core may use a generic internal `readonly [B, B]` boundary pair while the
-      number wrapper continues accepting `Range`.
-- [ ] Add shared `range_map` proofs showing that the generic implementation
-      preserves existing number behavior and works with bigint boundaries,
-      including a BNF range starting at `0n`, its internal `-1n` cut point, and
-      endpoints above `Number.MAX_SAFE_INTEGER`.
-- [ ] Update every parser/recognizer backend to synthesize exactly one logical EOF
-      after physical input and track whether it has been consumed in internal
-      parser state; do not require callers to append EOF.
-- [ ] Keep public parser positions/remainders in the physical input domain after
-      EOF consumption: indexed results report `input.length`, never
-      `input.length + 1`, and remainder-based results report the empty physical
-      remainder.
-- [ ] Keep synthesized EOF out of ordinary AST metadata leaves; preserve end-of-
-      input diagnostics at the physical end position.
-- [ ] Update BNF data, parsers, recognizers, AST/meta inputs, and proofs to consume
-      bigint symbols without introducing a separate EOF representation.
-- [ ] Update alphabet-specific helpers so their input values are converted to
-      bigint ordinary symbols only at their BNF boundary and never emit reserved
-      EOF; keep source-domain APIs unchanged.
-- [ ] Verify range complement, containment, shared range-map merge/lookup, and
-      ordering semantics over the 256-bit domain, including the boundary
-      immediately below EOF.
-- [ ] Add BNF proof coverage for minimum/maximum ordinary symbols, EOF, singleton
-      ranges, general ranges, complements, bigint dispatch-map lookup/merge,
-      alphabet-adapter boundaries, explicit EOF on empty/non-empty input, failure
-      before physical end, one-time EOF consumption, and public result positions
-      normalized to the physical input length.
+- [ ] Change BNF ordinary `Symbol` values to bigint with invariant
+      `0n <= symbol <= 2^256 - 1n`.
+- [ ] Keep logical EOF at `-1n`; do not reserve any uint256 ordinary value.
+- [ ] Define `fullRange` over the complete uint256 ordinary domain and keep `eof`
+      as the `-1n` singleton.
+- [ ] Adopt the bigint `TerminalRange` representation selected by
+      [Investigate TerminalRange representation](./terminal-range-representation.md).
+- [ ] Update range encode/decode, containment, complement helpers, BNF data,
+      parsers, recognizers, AST/meta inputs, and proofs for bigint terminals.
+- [ ] Parameterize `fjs/types/range_map` by boundary type and comparison /
+      predecessor operations.
+- [ ] Preserve the existing number `rangeMap(...)` API as a wrapper over the
+      generic implementation.
+- [ ] Instantiate the shared range-map implementation for bigint boundaries,
+      including `-2n`, `-1n`, `0n`, and values above `Number.MAX_SAFE_INTEGER`.
+- [ ] Keep Unicode/byte/token adapters responsible for mapping their source values
+      into the ordinary uint256 symbol domain.
+- [ ] Use bigint-aware JSON parse/serialize for serialized BNF data.
+- [ ] Add proofs for EOF, ordinary minimum/maximum values, ranges, complements,
+      range-map lookup/merge, and one-time logical EOF behavior.
 - [ ] `npx tsc`, `fjs test`.
 
 ### Related
 
-- [Bigint-aware JSON parse/serialize](../../media/json/todo/bigint-parse-serialize.md)
-  — exact JSON-compatible parse/serialize support required by bigint-valued BNF
-  data.
-- [Separate alphabet-specific BNF helpers](./unicode-rules.md) — makes the core
-  BNF symbol algebra independent of Unicode and byte-stream semantics before its
-  representation changes.
+- [Use `-1` as the BNF EOF symbol](./eof-minus-one.md) — establishes the EOF
+  semantics used by this migration.
 - [Investigate TerminalRange representation](./terminal-range-representation.md)
-  — chooses how bigint range endpoints are represented without assuming a
-  fixed-width 512-bit packed integer.
-- [UTF-8 token symbols](./utf8-token-symbols.md) — replace registered 24-bit token
-  IDs with deterministic token-name-derived symbols after this task lands.
+  — selects a representation for the expanded bigint terminal domain.
+- [Bigint-aware JSON parse/serialize](../../media/json/todo/bigint-parse-serialize.md)
+  — provides exact serialization for bigint-valued BNF data.
+- [Separate alphabet-specific BNF helpers](./unicode-rules.md) — keeps core BNF
+  independent from Unicode and byte-specific authoring helpers.
+- [UTF-8 token symbols](./utf8-token-symbols.md) — uses the full uint256 ordinary
+  symbol space for deterministic token mappings.
 - [Layered parser](./layered-parser.md) — tokenizer output becomes input symbols to
   the next BNF layer.
-- [`fjs/bnf/module.f.mjs`](../module.f.mjs) — current 24-bit symbol/range encoding.
-- [`fjs/types/range/module.f.mjs`](../../types/range/module.f.mjs) — remains the
-  existing number-boundary helper used by current number callers.
-- [`fjs/types/range_map/module.f.mjs`](../../types/range_map/module.f.mjs) — shared
-  range-map algorithm to parameterize for number and bigint boundaries instead of
-  duplicating it in BNF.
diff --git a/fjs/bnf/todo/eof-minus-one.md b/fjs/bnf/todo/eof-minus-one.md
new file mode 100644
index 0000000000..caba586256
--- /dev/null
+++ b/fjs/bnf/todo/eof-minus-one.md
@@ -0,0 +1,168 @@
+## Use `-1` as the BNF EOF symbol
+
+**Priority:** P3
+**Status:** open
+
+### Problem
+
+BNF currently uses one 24-bit terminal value for EOF. The current terminal space is:
+
+```text
+ordinary symbols = 0 .. 2^24 - 2
+EOF              = 2^24 - 1
+```
+
+This makes EOF depend on the physical symbol width. We want EOF to be a logical
+symbol outside the non-negative physical-symbol domain.
+
+### Proposal
+
+Move EOF from the top of the current 24-bit domain to `-1`:
+
+```text
+before:
+ordinary symbols = 0 .. 2^24 - 2
+EOF              = 2^24 - 1
+
+after:
+EOF              = -1
+ordinary symbols = 0 .. 2^24 - 2
+```
+
+This does **not** expand the current terminal space. There are exactly `2^24`
+terminal values both before and after the change.
+
+The later bigint-symbol migration is a separate change. It may expand ordinary
+symbols to the full uint256 domain:
+
+```text
+EOF              = -1
+ordinary symbols = 0 .. 2^256 - 1
+```
+
+That later expansion is where a larger/final `TerminalRange` representation is
+needed.
+
+#### Keep the current 24-bit stored representation
+
+The current packed `TerminalRange` can remain two 24-bit stored endpoints.
+Encode a semantic terminal into its stored 24-bit value with:
+
+```js
+const terminalSize = 2 ** 24
+const terminalMask = terminalSize - 1
+
+const encodeTerminal = value =>
+    (value + terminalSize) & terminalMask
+```
+
+For the current semantic domain this gives:
+
+```text
+-1            -> 2^24 - 1
+0             -> 0
+1             -> 1
+...
+2^24 - 2      -> 2^24 - 2
+```
+
+The inverse is also branchless:
+
+```js
+const decodeTerminal = value =>
+    ((value + 1) & terminalMask) - 1
+```
+
+The stored endpoint **codes and width** stay unchanged: EOF still uses stored code
+`2^24 - 1`, and every ordinary symbol keeps its existing stored code.
+
+This does not mean every existing serialized range has unchanged semantics.
+Ranges whose old endpoint was EOF must be regenerated under the new semantic
+ordering. In particular, the old `fullRange = [0, 2^24 - 1]` becomes the ordinary
+range `[0, 2^24 - 2]`; decoding the old upper endpoint now means EOF (`-1`).
+
+Treat this as a breaking semantic change to BNF range data. We do not need a
+compatibility/versioning layer for old serialized grammars; update in-repo data
+and generated ranges to the new semantics instead.
+
+The stored codes are an implementation representation, not semantic terminal
+ordering. Range operations that care about semantic ordering must compare decoded
+terminal values.
+
+`eof` is the singleton semantic range `[-1, -1]`. `fullRange` contains only
+ordinary physical symbols: `[0, 2^24 - 2]`. Complements over `fullRange` do not
+include EOF.
+
+#### Logical EOF in parser input
+
+Callers and alphabet adapters provide physical ordinary symbols only. They do not
+append `-1`. Parser/recognizer backends synthesize exactly one logical EOF after
+the physical input.
+
+Keep public parser positions physical:
+
+```text
+0 <= idx <= input.length
+```
+
+Internally, parser progress must include EOF consumption:
+
+```text
+cursor = (idx, eofConsumed)
+```
+
+At physical end:
+
+```text
+(input.length, false) --EOF--> (input.length, true)
+```
+
+Consuming EOF is parser progress even though public `idx` does not move.
+Sequencing, alternatives, repetition, backtracking, and failure high-water
+tracking must therefore use the complete cursor rather than `idx` alone.
+Backtracking restores both fields.
+
+For diagnostics, `(idx, true)` is farther than `(idx, false)`. Merge expected
+terminals only for failures at the same complete cursor, then report the physical
+`idx` publicly.
+
+The synthesized EOF has no physical source element and contributes no ordinary
+metadata leaf to the AST. EOF diagnostics point at `input.length`.
+
+### Tasks
+
+- [ ] Change semantic EOF from `2^24 - 1` to `-1`.
+- [ ] Keep the current ordinary domain `0 .. 2^24 - 2` unchanged.
+- [ ] Keep `TerminalRange` packed as two 24-bit stored endpoints.
+- [ ] Encode/decode semantic terminals with the branchless 24-bit formulas above,
+      preserving the existing stored EOF code and all ordinary stored codes.
+- [ ] Regenerate/update ranges whose old endpoint was EOF, including `fullRange`;
+      do not add compatibility/versioning for old serialized grammar data.
+- [ ] Update range containment, validation, keys, and proofs to distinguish
+      semantic terminal values from stored endpoint codes.
+- [ ] Define `eof` as semantic `[-1, -1]` and `fullRange` as
+      `[0, 2^24 - 2]`.
+- [ ] Synthesize logical EOF exactly once in parser/recognizer backends; callers
+      must not append EOF.
+- [ ] Track parser cursor as `(idx, eofConsumed)` and use the complete cursor for
+      progress, alternatives, repetition, backtracking, and diagnostic ordering.
+- [ ] Keep public positions/remainders physical and keep synthesized EOF out of
+      ordinary AST metadata.
+- [ ] Update callers/proofs that assume semantic EOF is `2^24 - 1`.
+- [ ] Add proofs for empty/non-empty input, one-time EOF consumption, EOF in
+      alternatives/repetition, backtracking, diagnostic ordering, ordinary
+      minimum/maximum values, and range encode/decode round trips.
+- [ ] Add a `CHANGELOG.md` breaking-change entry if this changes published BNF
+      range semantics.
+- [ ] `npx tsc`, `fjs test`.
+
+### Related
+
+- [Investigate TerminalRange representation](./terminal-range-representation.md)
+  — chooses the representation needed when the later bigint migration expands
+  the terminal domain.
+- [256-bit bigint BNF symbols](./bigint-symbols.md) — later expands ordinary
+  symbols to the full uint256 domain while keeping `EOF = -1`.
+- [`fjs/bnf/module.f.mjs`](../module.f.mjs) — current 24-bit range codec and EOF
+  definition.
+- [`fjs/bnf/types.ts`](../types.ts) — current packed-number `TerminalRange` type.
diff --git a/fjs/bnf/todo/recognizer-backend.md b/fjs/bnf/todo/recognizer-backend.md
index ef4f2a0e44..cfb96c8e7d 100644
--- a/fjs/bnf/todo/recognizer-backend.md
+++ b/fjs/bnf/todo/recognizer-backend.md
@@ -2,7 +2,7 @@
 
 **Priority:** P3
 **Status:** blocked
-**Blocked by:** [Separate alphabet-specific BNF helpers](./unicode-rules.md)
+**Blocked by:** [Use `-1` as the BNF EOF symbol](./eof-minus-one.md), [Separate alphabet-specific BNF helpers](./unicode-rules.md)
 
 ### Problem
 
@@ -34,6 +34,11 @@ alphabet split first so the recognizer can consume those helpers instead of
 creating a second byte-helper API or restoring alphabet-specific syntax in core
 BNF.
 
+The recognizer must also preserve the logical EOF contract from
+[Use `-1` as the BNF EOF symbol](./eof-minus-one.md). Incremental chunk boundaries
+are not end-of-input; EOF is synthesized only when the complete stream is
+explicitly finalized.
+
 ### Proposal
 
 Treat **BNF as the single source, with a family of backends** that share one
@@ -47,10 +52,12 @@ type StateScan<I, S, O> = (input: I, prior: S) => readonly[O, S]    // Mealy ste
 type Scan<I, O>         = (input: I) => readonly[O, Scan<I, O>]     // state-hidden form; stateScanToScan unifies
 ```
 
-- A **recognizer** is the output-less case: `Fold<Symbol, State>` for `δ`, plus
-  a separate `λ: (State) => Verdict` on the final state. Driven by `foldScan`
-  (stream of states) / `fold` (final state) — exactly what `fjs/fsm`'s
-  `run = foldScan(runOp)` already does.
+- A **recognizer** uses `Fold<Symbol, State>` for its per-physical-symbol `δ`,
+  plus an explicit finalization operation that provides exactly one logical EOF
+  transition opportunity while preserving acceptance already established at the
+  physical end of input. Driven by `foldScan` (stream of states) / `fold` (state
+  after physical input) — exactly what `fjs/fsm`'s `run = foldScan(runOp)`
+  already does.
 - A **transducer** is `StateScan<Symbol, State, Out>` (the Mealy step that emits
   output), driven by `stateScan(op)(init): List<Out>`.
 
@@ -58,6 +65,66 @@ type Scan<I, O>         = (input: I) => readonly[O, Scan<I, O>]     // state-hid
 incremental input, including the effectful CAS chunk stream) and lets callers
 **short-circuit** once the state reaches an absorbing sink.
 
+#### Logical EOF finalization
+
+The ordinary streaming step consumes physical symbols only. It must never inject
+EOF merely because one array/chunk ended. State is carried unchanged across chunk
+boundaries until the caller knows the complete input stream has ended.
+
+At true end-of-stream, use one explicit finalization operation. Conceptually:
+
+```text
+state = fold(physicalSymbols, init)
+verdict = finish(state)
+```
+
+Logical EOF is available exactly once at finalization, but existing whole-input
+grammars must not be forced to add an explicit `eof` terminal. A grammar that is
+already accepting after the complete physical stream remains accepted; a grammar
+that requires `eof` may instead become accepting after consuming the synthesized
+EOF.
+
+If the backend exposes an internal terminal transition `δTerminal` and an
+accepting-state classifier `λ`, the observable semantics are equivalent to:
+
+```text
+beforeEOF = λ(state)
+afterEOF  = λ(δTerminal(EOF, state))
+finish(state) = beforeEOF || afterEOF
+```
+
+The EOF transition is therefore not allowed to erase acceptance that was already
+established at the physical end. For example, if an ordinary grammar reaches an
+accepting state after its last physical symbol and the EOF transition would move
+that state to a rejecting sink, `finish` still returns true. Conversely, a
+grammar whose final rule explicitly requires `eof` can return false before EOF
+and true after the one synthesized transition.
+
+A backend may encode the same behavior by compiling an optional final EOF path
+rather than literally evaluating both states, but the semantics must be
+identical. The exact internal representation may differ by backend; the contract
+is about the accepted language and one-time EOF availability.
+
+The finalization semantics are fixed:
+
+- physical folds/chunks never contain or synthesize EOF;
+- chunk boundaries do not invoke finalization;
+- finalization provides exactly one logical EOF transition opportunity;
+- acceptance at the physical end is preserved even if the EOF transition would
+  reject;
+- a grammar that explicitly requires EOF may accept through the synthesized EOF
+  transition;
+- rejection means neither the pre-EOF nor post-EOF state is accepting;
+- empty input is handled by the same rule from the initial state;
+- callers do not append `-1` and do not manufacture EOF metadata;
+- repeated chunking of the same physical stream must produce the same finalized
+  verdict as processing it as one chunk.
+
+This finalization rule applies to the DFA recognizer and the AST-less LL(1)
+recognizer. It preserves the existing "recognized and consumed the complete
+physical input" contract while also making the EOF terminal available to grammars
+that use it explicitly.
+
 #### Build from the data representation, not the functional one
 
 BNF has two representations and the automata builders consume the **second**:
@@ -199,10 +266,22 @@ Bigger automata are built from BNF pieces in two complementary ways:
       IR; new backends land as sibling modules (`fjs/bnf/recognizer`,
       `fjs/bnf/dfa`)
 - [ ] Use the existing `Scan` family as the streaming contract (no new type):
-      `Fold<I, S>` for a recognizer + a separate `λ: (S) => Verdict`,
+      `Fold<I, S>` for the physical-symbol recognizer step and
       `StateScan<I, S, O>` for a transducer; drivers `foldScan` / `stateScan` /
       `scan`. Keep it parametric in the symbol space over the same generic
       `RuleSet`. (`fjs/fsm`'s `run = foldScan(runOp)` is precedent.)
+- [ ] Add explicit end-of-stream finalization for DFA and AST-less LL(1)
+      recognizers: ordinary/chunk folds consume only physical symbols; `finish`
+      preserves an accepting pre-EOF state and also evaluates the one synthesized
+      EOF transition so grammars that explicitly require `eof` can accept.
+- [ ] Prove both finalization acceptance paths: an existing whole-input grammar
+      without `eof` remains accepted at physical end, and a grammar that requires
+      `eof` becomes accepted only after the synthesized transition. Also prove a
+      grammar rejecting both states remains rejected.
+- [ ] Prove finalization on empty/non-empty inputs and chunking independence:
+      splitting the same physical input into different chunk boundaries must not
+      change the finalized verdict or create additional EOF transition
+      opportunities.
 - [ ] Tokenizer stage needs maximal munch (emit at the longest accepting
       prefix, then restart) — a mechanism over plain recognition
 - [ ] DFA backend: `RuleSet` (regular subset) → finite DFA, built as a sibling
@@ -222,6 +301,8 @@ Bigger automata are built from BNF pieces in two complementary ways:
 
 ### Related
 
+- [Use `-1` as the BNF EOF symbol](./eof-minus-one.md) — defines the logical EOF
+  finalization semantics that every recognizer backend must preserve.
 - [Separate alphabet-specific BNF helpers](./unicode-rules.md) — owns Unicode and
   byte authoring helpers; this recognizer work consumes the generic rules they
   produce.
diff --git a/fjs/bnf/todo/terminal-range-representation.md b/fjs/bnf/todo/terminal-range-representation.md
index 8316b40568..ff89de8f9c 100644
--- a/fjs/bnf/todo/terminal-range-representation.md
+++ b/fjs/bnf/todo/terminal-range-representation.md
@@ -5,97 +5,70 @@
 
 ### Problem
 
-The current BNF `TerminalRange` packs two 24-bit endpoints into one JavaScript
-`number`:
+The current BNF `TerminalRange` packs two 24-bit endpoint codes into one
+JavaScript `number`:
 
 ```text
 range = start * 2^24 + end
 ```
 
-If BNF symbols move to a 256-bit `bigint` domain, directly preserving this layout
-would become:
+Moving semantic EOF from `2^24 - 1` to `-1` does not require changing this
+representation. The same 24-bit stored EOF code can continue to represent EOF,
+and ordinary symbols remain `0 .. 2^24 - 2`.
+
+The representation question becomes necessary when BNF ordinary symbols later
+expand to the full uint256 domain:
 
 ```text
-range = start * 2^256 + end
+EOF              = -1
+ordinary symbols = 0 .. 2^256 - 1
 ```
 
-That representation is simple and fixed-width, but even a range with very small
-endpoints becomes a very large integer. The current compact-number motivation for
-packing the pair therefore no longer obviously applies.
+That domain has `2^256 + 1` semantic terminal values, so a single 256-bit unsigned
+endpoint code cannot represent all terminals.
+
+### Alternatives to investigate
 
-This is not only a runtime-performance question. `TerminalRange` is part of the
-serializable BNF rule representation, so choosing the fixed-width layout during
-the uint256 migration would also choose the persistent representation emitted by
-JSON/DJS and stored or hashed as BNF data. Changing that representation later may
-therefore be a format migration rather than a local optimization.
+Use a simple deterministic representation. Candidates include:
 
-The fixed-width form is the **baseline** because it is the simplest continuation
-of the current encoding. The investigation should compare other representations
-against that baseline and choose only if they provide a meaningful enough benefit
-to justify extra complexity. Do not assume in advance that a more compact scheme
-wins, but also do not commit the serialized format before making this small design
-comparison.
+- an order-preserving non-negative encoding:
 
-Before the bigint symbol migration chooses a `TerminalRange` representation,
-investigate whether the range should remain one `bigint` or become a different
-rule representation.
+  ```text
+  encodeTerminal(value) = value + 1
+  decodeTerminal(value) = value - 1
+  ```
 
-### Alternatives to investigate
+  giving encoded endpoints `0 .. 2^256`; a fixed-width form therefore needs
+  257 bits per endpoint;
+- a structural range storing signed semantic endpoints directly;
+- a canonical variable-width bigint encoding;
+- other simple representations that preserve the same semantic domain.
+
+A structural representation may require changing the surrounding BNF rule/data
+representation so terminal ranges remain unambiguous from sequences and variants.
+
+`TerminalRange` is serialized BNF data and may be content-addressed, so the chosen
+representation must be canonical and stable rather than an incidental runtime
+optimization.
+
+### Tasks
 
-At minimum, compare:
-
-- fixed-width bigint packing, equivalent to `(start << 256n) | end`; this is the
-  simplest baseline and should be preferred unless another representation has a
-  clear advantage;
-- bigint bit interleaving, for example storing bits from one endpoint in even bit
-  positions and bits from the other endpoint in odd bit positions, so small
-  endpoints remain small;
-- another self-delimiting / variable-width bigint encoding whose size follows the
-  actual endpoint sizes rather than the full 256-bit symbol width;
-- a non-bigint structural representation for a range.
-
-Do not choose one of these representations in this investigation TODO yet.
-Additional simple representations may be considered if they make the rule model
-clearer.
-
-A structural range representation has a wider consequence: today primitive
-numeric values distinguish terminal ranges from arrays/sequences and
-objects/variants. If `TerminalRange` stops being a primitive bigint, the other BNF
-rule representations may also need to change so every rule kind remains
-unambiguous and serializable. Treat that as part of the comparison rather than
-assuming that only `TerminalRange` changes.
-
-### Evaluation criteria
-
-- [ ] Use fixed-width `(start << 256n) | end` as the baseline and compare actual
-      encoded/serialized sizes before choosing a more complex representation.
-- [ ] Compare encoded size for common small ranges such as bytes, ASCII, and
-      Unicode code-point ranges, as well as ranges near the uint256 boundary.
-- [ ] Require a deterministic, canonical, lossless representation with simple
-      encode/decode semantics.
-- [ ] Compare containment/range-operation cost; avoid conversions through
-      JavaScript `number`.
-- [ ] Consider JSON/DJS serialization size and debuggability. The current packed
-      range is already not meaningfully human-readable, so readability alone is
-      not a reason to preserve primitive packing.
-- [ ] Treat representation stability as part of the decision because serialized
-      BNF data may be persisted/content-addressed; avoid knowingly choosing a
-      temporary wire representation merely to defer the comparison.
-- [ ] Preserve the reserved EOF symbol and `fullRange` semantics from the bigint
-      symbol design.
-- [ ] If considering a structural representation, specify how `Rule`, `DataRule`,
-      sequences, variants, lazy rules, and serialized BNF data remain
-      unambiguous.
-- [ ] Consider migration complexity for BNF core, data conversion, descent/LL(1)
-      parsers, and proofs.
-- [ ] Choose the representation before implementing the uint256 BNF-symbol
-      migration.
+- [ ] Use the bigint terminal domain `[-1] | [0, 2^256 - 1]` as the required
+      semantic domain.
+- [ ] Compare fixed-width 257-bit endpoint encoding with simpler structural or
+      variable-width alternatives.
+- [ ] Require deterministic, canonical, lossless encode/decode semantics.
+- [ ] Compare serialized size and containment/range-operation cost for EOF,
+      bytes, Unicode, token symbols, and values near `2^256 - 1`.
+- [ ] If using a structural representation, specify how `Rule` / `DataRule`
+      remain unambiguous and serializable.
+- [ ] Choose one representation for the bigint-symbol migration and document any
+      serialized/public format migration it requires.
 
 ### Related
 
-- [256-bit bigint BNF symbols](./bigint-symbols.md) — blocked on this representation
-  decision.
-- [Separate alphabet-specific BNF helpers](./unicode-rules.md) — keeps the range
-  representation independent from Unicode-specific syntax.
-- [`fjs/bnf/module.f.mjs`](../module.f.mjs) — current 24-bit packed range encoding and
-  rule representation.
+- [Use `-1` as the BNF EOF symbol](./eof-minus-one.md) — keeps the existing
+  24-bit stored representation while changing EOF's semantic value.
+- [256-bit bigint BNF symbols](./bigint-symbols.md) — expands the terminal domain
+  and consumes the representation selected here.
+- [`fjs/bnf/module.f.mjs`](../module.f.mjs) — current 24-bit packed range codec.
diff --git a/fjs/bnf/todo/unicode-rules.md b/fjs/bnf/todo/unicode-rules.md
index 2eef1d2b0a..fb95f6374b 100644
--- a/fjs/bnf/todo/unicode-rules.md
+++ b/fjs/bnf/todo/unicode-rules.md
@@ -60,9 +60,11 @@ constructing `','` as a string rule), change its core form to accept rules or
 symbols. A Unicode convenience wrapper may live in `fjs/bnf/unicode` if useful.
 
 EOF remains a generic BNF symbol convention rather than an alphabet-specific
-helper. The bigint-symbol task reserves the maximal 256-bit symbol value for EOF,
-so Unicode, byte, token, and future alphabets all use the same parser-level EOF
-representation without defining their own sentinel.
+helper. [The EOF task](./eof-minus-one.md) defines `EOF = -1`, outside the
+non-negative physical-symbol domain. Unicode, byte, token, and future alphabet
+adapters therefore produce only ordinary non-negative symbols and never need to
+reserve one value from their own alphabet. After the bigint migration the full
+uint256 range `0 .. 2^256 - 1` remains available for ordinary symbols.
 
 The result should allow the same core BNF API to describe grammars over any
 symbol alphabet without importing or depending on Unicode or byte-stream support.
@@ -125,6 +127,9 @@ new module boundary and final rule discriminants before implementation starts.
       `fjs/bnf/unicode/module.f.ts`.
 - [ ] Update grammars and imports to construct text terminals through the Unicode
       helpers instead of relying on raw strings as generic rules.
+- [ ] Keep EOF generic and width-independent: use `EOF = -1` from
+      [the EOF task](./eof-minus-one.md), and keep all alphabet adapters restricted
+      to ordinary non-negative symbols without reserving the maximal value.
 - [ ] Update/block `fjs/media/json/todo/bnf-grammar-single-owner.md` so its JSON
       grammar design imports Unicode helpers from `fjs/bnf/unicode/module.f.ts`
       and does not depend on raw string rules in core BNF.
@@ -156,8 +161,11 @@ new module boundary and final rule discriminants before implementation starts.
 
 ### Related
 
+- [Use `-1` as BNF EOF](./eof-minus-one.md) — defines EOF outside every physical
+  alphabet so adapters do not reserve a width-dependent value.
 - [256-bit bigint BNF symbols](./bigint-symbols.md) — after this split, the core
-  symbol-domain migration can stay independent of alphabet semantics.
+  symbol-domain migration can stay independent of alphabet semantics and retain
+  the full uint256 ordinary-symbol range.
 - [Layered parser](./layered-parser.md) — each parser layer can use the same BNF
   machinery with a different symbol alphabet.
 - [UTF-8 token symbols](./utf8-token-symbols.md) — tokenizer-output symbols are
diff --git a/fjs/bnf/todo/utf8-token-symbols.md b/fjs/bnf/todo/utf8-token-symbols.md
index 5cdb070313..d86bccc9af 100644
--- a/fjs/bnf/todo/utf8-token-symbols.md
+++ b/fjs/bnf/todo/utf8-token-symbols.md
@@ -76,7 +76,7 @@ const tryTokenSymbol = (name: string): Nullable<Symbol> => {
     if (vec === null) { return null }
     const encoded = tryToSentinel(vec)
     if (encoded === null) { return null }
-    return 0n <= encoded && encoded < eofSymbol ? encoded : null
+    return 0n <= encoded && encoded < (1n << 256n) ? encoded : null
 }
 ```
 
@@ -87,15 +87,15 @@ limit is a valid `Vec`, but its positive sentinel form is not representable on a
 supported runtimes. The `tryTokenSymbol` contract must return `null` for both
 cases, as well as for any candidate outside the ordinary BNF symbol domain.
 
-`eofSymbol` is the maximal 256-bit value reserved by BNF. Thus a successful
-direct mapping is always an ordinary BNF symbol and can never collide with EOF.
-The final validation is against the complete actual symbol-domain invariant,
-`0n <= encoded && encoded < eofSymbol`, not merely against the exact EOF value or
-an estimated/precomputed source size.
+BNF EOF is `-1`, outside the non-negative uint256 input-symbol domain. Therefore a
+successful direct mapping can use the complete ordinary-symbol range
+`0 .. 2^256 - 1` and cannot collide with EOF. The final validation is against the
+complete actual symbol-domain invariant, `0n <= encoded && encoded < 2^256`, not
+against a reserved maximal value or an estimated/precomputed source size.
 
 For the current UTF-8 sentinel encoding, the 31-byte boundary remains a useful
 derived property rather than a preflight rule: byte-aligned names up to 31 UTF-8
-bytes produce values below the ordinary-symbol limit, while a 32-byte name puts
+bytes produce values inside the uint256 symbol domain, while a 32-byte name puts
 the sentinel at bit 256 and therefore returns `null` at the BNF-domain check.
 Proofs should cover that boundary, but implementation should branch on the actual
 `tryUtf8`, `tryToSentinel`, and symbol-domain results.
@@ -113,10 +113,11 @@ global injectivity, so construction/configuration of a layer that uses such a
 mapping must map its complete finite set of token names and reject the
 configuration if two distinct names produce the same symbol, if any mapping
 returns `null`, or if any produced bigint is outside the ordinary symbol domain
-`0n <= symbol && symbol < eofSymbol`. This rejects negative values, values wider
-than the 256-bit domain, and reserved EOF uniformly. Producer and consumer may
-still compute symbols independently after that alphabet has been validated; no
-ordered registration ID is introduced.
+`0n <= symbol && symbol < 2^256`. This rejects negative values and values wider
+than the 256-bit domain uniformly. Because EOF is `-1`, restricting mappings to
+that non-negative domain also excludes EOF automatically. Producer and consumer
+may still compute symbols independently after that alphabet has been validated;
+no ordered registration ID is introduced.
 
 Different parser layers have different symbol alphabets, so the same numeric
 symbol does not need a global meaning across byte, code-point, token, and later
@@ -153,7 +154,7 @@ tokens or calls `token_symbol.encoding()` for multi-character names.
       produced value against the ordinary BNF symbol domain.
 - [ ] Return `null` when UTF-8/bit-vector encoding fails, sentinel conversion
       fails, or the encoded candidate does not satisfy
-      `0n <= encoded && encoded < eofSymbol`; do not use a UTF-8 length preflight
+      `0n <= encoded && encoded < 2^256`; do not use a UTF-8 length preflight
       check.
 - [ ] Prove injectivity for every successful direct encoding, including
       preservation of leading zero bytes/bits.
@@ -164,10 +165,11 @@ tokens or calls `token_symbol.encoding()` for multi-character names.
 - [ ] Require every token mapping to be injective over the concrete token alphabet
       used by a parser layer. For mappings without a mathematical injectivity
       guarantee, validate the complete configured token-name set and reject
-      duplicate symbols, `null`, negative/out-of-width bigints, and reserved EOF
-      before the layer is used.
-- [ ] Reserve `2^256 - 1` for EOF in every token-symbol mapping; every successful
-      mapping result must be in `0 .. EOF - 1`.
+      duplicate symbols, `null`, negative/out-of-width bigints, and other values
+      outside `0 .. 2^256 - 1` before the layer is used.
+- [ ] Treat EOF as `-1`; token mappings produce only non-negative uint256 symbols,
+      so the full `0 .. 2^256 - 1` domain is available and EOF is excluded
+      automatically.
 - [ ] Keep dependent parser designs, including [new-parser](./new-parser.md),
       blocked until their token-name alphabets use this fallible `Symbol` mapping
       instead of `token_symbol.encoding()` or raw 24-bit/ASCII identities.
@@ -187,8 +189,10 @@ tokens or calls `token_symbol.encoding()` for multi-character names.
 
 ### Related
 
-- [256-bit bigint BNF symbols](./bigint-symbols.md) — provides the symbol space
-  used by this mapping.
+- [256-bit bigint BNF symbols](./bigint-symbols.md) — provides the full uint256
+  ordinary-symbol space used by this mapping; BNF EOF remains `-1`.
+- [Use `-1` as BNF EOF](./eof-minus-one.md) — defines EOF outside the physical
+  symbol domain.
 - [New parser](./new-parser.md) — consumes a validated finite token-name alphabet
   through this mapping rather than the current 24-bit registration API.
 - [Layered parser](./layered-parser.md) — tokenizer output feeds the next BNF